Zapato 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 Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year Zapato: Automatic theorem proving for predicate abstraction refinement. Zbl 1103.68604Ball, Thomas; Cook, Byron; Lahiri, Shuvendu K.; Zhang, Lintao 2004 all top 5 Cited by 26 Authors 4 Cimatti, Alessandro 4 Sebastiani, Roberto 3 Bruttomesso, Roberto 2 Bozzano, Marco 2 Griggio, Alberto 2 Junttila, Tommi A. 2 Ranise, Silvio 2 van Rossum, Peter 1 Amjad, Hasan 1 Bagnara, Roberto 1 Ball, Thomas 1 Biere, Armin 1 Conchon, Sylvain 1 Cook, Byron 1 Déharbe, David 1 Franzén, Anders 1 Hill, Patricia M. 1 Kröning, Daniel 1 Krstic, Sava A. 1 Lahiri, Shuvendu Kumar 1 Leino, K. Rustan M. 1 Logozzo, Francesco 1 Schulz, Stephan 1 Vidal, Jorgiano 1 Zaffanella, Enea 1 Zhang, Lintao Cited in 5 Serials 1 Theoretical Computer Science 1 Information and Computation 1 Journal of Automated Reasoning 1 Formal Methods in System Design 1 Annals of Mathematics and Artificial Intelligence Cited in 2 Fields 11 Computer science (68-XX) 1 Mathematical logic and foundations (03-XX) Citations by Year