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$$g164625$$aAmin, Nada
000227179 700__ $$aLeino, Rustan
000227179 700__ $$0243345$$g185682$$aRompf, Tiark
000227179 8564_ $$uhttps://www.microsoft.com/en-us/research/publication/computing-smt-solver$$zURL
000227179 909C0 $$xU10409$$0252187$$pLAMP
000227179 909CO $$qGLOBAL_SET$$pconf$$ooai:infoscience.tind.io:227179$$pIC
000227179 917Z8 $$x164625
000227179 937__ $$aEPFL-CONF-227179
000227179 973__ $$rREVIEWED$$sPUBLISHED$$aOTHER
000227179 980__ $$aCONF