Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Zap: Automated Theorem Proving for Software Analysis

Thomas Ball, Shuvendu Lahiri, and Madanlal Musuvathi


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.


Publication typeProceedings
Published inLogic for Programming, Artificial Intelligence, and Reasoning (LPAR '05)
SeriesLNCS 3835
InstitutionMicrosoft Research
PublisherSpringer Verlag
> Publications > Zap: Automated Theorem Proving for Software Analysis