@techreport{ball2005zap,
author = {Ball, Thomas and Lahiri, Shuvendu and Musuvathi, Madanlal and Ball, Thomas and Musuvathi, Madan},
title = {Zap: Automated Theorem Proving for Software Analysis},
series = {LNCS 3835},
year = {2005},
month = {October},
abstract = {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.},
publisher = {Springer Verlag},
url = {http://approjects.co.za/?big=en-us/research/publication/zap-automated-theorem-proving-for-software-analysis/},
pages = {21},
edition = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '05)},
number = {MSR-TR-2005-137},
note = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '05)},
}