Paper Info
Title
Solving existentially quantified horn clauses
Abstract
Temporal verification of universal (i.e., valid for all computation paths) properties of various kinds of programs, e.g., procedural, multi-threaded, or functional, can be reduced to finding solutions for equations in form of universally quantified Horn clauses extended with well-foundedness conditions. Dealing with existential properties (e.g., whether there exists a particular computation path), however, requires solving forall-exists quantified Horn clauses, where the conclusion part of some clauses contains existentially quantified variables. For example, a deductive approach to CTL verification reduces to solving such clauses. In this paper we present a method for solving forall-exists quantified Horn clauses extended with well-foundedness conditions. Our method is based on a counterexample-guided abstraction refinement scheme to discover witnesses for existentially quantified variables. We also present an application of our solving method to automation of CTL verification of software, as well as its experimental evaluation.
Year
DOI
Venue
2013
10.1007/978-3-642-39799-8_61
CAV
Keywords
Field
DocType
horn clause,particular computation path,well-foundedness condition,counterexample-guided abstraction refinement scheme,conclusion part,ctl verification,computation path,temporal verification,existential property,deductive approach
Horn clause,Predicate abstraction,Existential quantification,Computer science,Horn-satisfiability,Algorithm,Automation,Theoretical computer science,Software,Unit propagation,Computation
Conference
Citations 
PageRank 
References 
40
1.10
25
Authors
3
Name
Order
Citations
PageRank
Tewodros A. Beyene1703.74
Corneliu Popeea237418.27
Andrey Rybalchenko3143968.53