Zapato

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.


References in zbMATH (referenced in 11 articles , 1 standard article )

Showing results 1 to 11 of 11.
Sorted by year (citations)

  1. Biere, Armin; Kröning, Daniel: SAT-based model checking (2018)
  2. Bagnara, Roberto; Hill, Patricia M.; Zaffanella, Enea: Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness (2009)
  3. Bruttomesso, Roberto; Cimatti, Alessandro; Franzen, Anders; Griggio, Alberto; Sebastiani, Roberto: Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis (2009)
  4. Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto: Interpolant generation for UTVPI (2009)
  5. Deharbe, David; Ranise, Silvio; Vidal, Jorgiano: Distributing the workload in a lazy theorem-prover (2007)
  6. Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Junttila, Tommi; Ranise, Silvio; Van Rossum, Peter; Sebastiani, Roberto: Efficient theory combination via Boolean search (2006)
  7. Conchon, Sylvain; Krstić, Sava: Strategies for combining decision procedures (2006)
  8. Amjad, Hasan: Shallow lazy proofs (2005)
  9. Bozzano, Marco; Bruttomesso, Roberto; Cimatti, Alessandro; Junttila, Tommi; van Rossum, Peter; Schulz, Stephan; Sebastiani, Roberto: M\textbfathSAT: Tight integration of SAT and mathematical decision procedures (2005)
  10. Leino, K. Rustan M.; Logozzo, Francesco: Loop invariants on demand (2005)
  11. Ball, Thomas; Cook, Byron; Lahiri, Shuvendu K.; Zhang, Lintao: Zapato: Automatic theorem proving for predicate abstraction refinement (2004)