000227179 001__ 227179
000227179 005__ 20190317000655.0
000227179 0247_ $$2doi$$a10.1007/978-3-319-09099-3_2
000227179 037__ $$aCONF
000227179 245__ $$aComputing with an SMT Solver
000227179 269__ $$a2014
000227179 260__ $$c2014
000227179 336__ $$aConference Papers
000227179 520__ $$aSatisfiability 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.
000227179 700__ $$0246589$$aAmin, Nada$$g164625
000227179 700__ $$aLeino, Rustan
000227179 700__ $$0243345$$aRompf, Tiark$$g185682
000227179 8564_ $$uhttps://www.microsoft.com/en-us/research/publication/computing-smt-solver$$zURL
000227179 909C0 $$0252187$$pLAMP$$xU10409
000227179 909CO $$ooai:infoscience.tind.io:227179$$pconf$$pIC$$qGLOBAL_SET
000227179 917Z8 $$x164625
000227179 937__ $$aEPFL-CONF-227179
000227179 973__ $$aOTHER$$rREVIEWED$$sPUBLISHED
000227179 980__ $$aCONF