Zap: Automated theorem proving for software analysis Automated theorem provers (ATPs) are a key component that many software verification and program analysis tools rely on. However, the basic interface provided by ATPs (validity/satisfiability checking of formulas) has changed little over the years. We believe that program analysis clients would benefit greatly if theorem provers were to provide a richer set of operations. We describe our desiderata for such an interface to an ATP, the logics (theories) that an ATP for program analysis should support, and present how we have incorporated many of these ideas in Zap, an ATP built at Microsoft Research.
References in zbMATH (referenced in 7 articles )
Showing results 1 to 7 of 7.
- Bauer, Andreas; Leucker, Martin; Schallhart, Christian; Tautschnig, Michael: Don’t care in SMT: building flexible yet efficient abstraction/refinement solvers (2010)
- Babić, Domagoj; Hu, Alan J.: Approximating the safely reusable set of learned facts (2009)
- Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto: Efficient interpolant generation in satisfiability modulo theories (2008)
- Moskal, Michal; Lopuszanski, Jakub; Kiniry, Joseph R.: E-matching for fun and profit. (2008)
- Bouillaguet, Charles; Kuncak, Viktor; Wies, Thomas; Zee, Karen; Rinard, Martin: Using first-order theorem provers in the Jahob data structure verification system (2007)
- Chatterjee, Shaunak; Lahiri, Shuvendu K.; Qadeer, Shaz; Rakamarić, Zvonimir: A reachability predicate for analyzing low-level software (2007)
- Ball, Thomas; Lahiri, Shuvendu K.; Musuvathi, Madanlal: Zap: Automated theorem proving for software analysis (2005)