swMATH ID: 25425
Software Authors: Ball, T., Cook, B., Lahiri, S.K., Zhang, L.
Description: zapato: Automatic theorem proving for predicate abstraction refinement. Counterexample-driven abstraction refinement is an automatic process that produces abstract models of finite and infinite-state systems. When this process is applied to software, an automatic theorem prover for quantifier-free first-order logic helps to determine the feasibility of program paths and to refine the abstraction. In this paper we report on a fast, lightweight, and automatic theorem prover called Zapato which we have built specifically to solve the queries produced during the abstraction refinement process.
Homepage: https://link.springer.com/chapter/10.1007/978-3-540-27813-9_36
Related Software: CVC Lite; Chaff; MiniSat; ICS; E Theorem Prover; MathSAT; FOCI; SIMPLIFY; BoogiePL; Spec#; HOL Light; HOL; ML; CVC; Maude; ELAN; Eraser; Bandera; Bogor; veriSoft
Cited in: 11 Publications

Citations by Year