Abstract
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. © Springer-Verlag Berlin Heidelberg 2004.
Cite
CITATION STYLE
Ball, T., Cook, B., Lahiri, S. K., & Zhang, L. (2004). ZAPATO: Automatic theorem proving for predicate abstraction refinement. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3114, 457–461. https://doi.org/10.1007/978-3-540-27813-9_36
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
