Anzeige
Erschienen in:
2014 | OriginalPaper | Buchkapitel
Computing with an SMT Solver
verfasst von : Nada Amin, K. Rustan M. Leino, Tiark Rompf
Erschienen in: Tests and Proofs
Verlag: Springer International Publishing
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Satisfiability modulo theories (SMT) solvers that support quantifier instantiations via matching triggers can be programmed to give practical support for user-defined theories. Care must be taken to avoid so-called matching loops, which may prevent termination of the solver. By design, such avoidance limits the extent to which the SMT solver is able to apply the definitions of user-defined functions. For some inputs to these functions, however, it is instead desireable to allow unadulterated use of the functions; in particular, if it is known that evaluation will terminate.
This paper describes the program verifier Dafny’s SMT encoding of recursive user-defined functions. It then describes a novel encoding that, drawing on ideas from offline partial evaluation systems, lets the SMT solver evaluate “safe” function applications while guarding against matching loops for others.