|
Published: 14th July 2016 DOI: 10.4204/EPTCS.219 ISSN: 2075-2180 |
| Preface John P. Gallagher and Philipp Rümmer | |
| Invited Presentation: Transforming Constrained Horn Clauses for Program Verification Maurizio Proietti | |
| Invited Presentation: On Predicate Refinement Heuristics in Program Verification with CEGAR Tachio Terauchi | |
| Efficient CTL Verification via Horn Constraints Solving Tewodros A. Beyene, Corneliu Popeea and Andrey Rybalchenko | 1 |
| Hierarchical State Machines as Modular Horn Clauses Pierre-Loïc Garoche, Temesghen Kahsai and Xavier Thirioux | 15 |
| Challenges in Decomposing Encodings of Verification Problems Peter Schrammel | 29 |
| Solving non-linear Horn clauses using a linear Horn clause solver Bishoksan Kafle, John P. Gallagher and Pierre Ganty | 33 |
| Removing Unnecessary Variables from Horn Clause Verification Conditions Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi and Maurizio Proietti | 49 |
| Horn Binary Serialization Analysis Gabriele Paganelli | 56 |
This volume contains the proceedings of HCVS 2016, the Third Workshop on Horn Clauses for Verification and Synthesis which was held on April 3, 2016 in Eindhoven, The Netherlands as a satellite event of the European Joint Conferences on Theory and Practice of Software (ETAPS 2016).
Many program verification and synthesis problems of interest can be modeled directly using Horn clauses and many recent advances in the CLP and CAV communities have centered around efficiently solving problems presented as Horn clauses. The 3rd Workshop on Horn Clauses for Verification and Synthesis was organised with the aim to bring together researchers working in the two communities of Constraint/Logic Programming and Program Verification on the topic of Horn clause based analysis, verification and synthesis. Horn clauses for verification and synthesis have been advocated by these two communities in different times and from different perspectives, and this workshop is organized to stimulate interaction and a fruitful exchange and integration of experiences.
The workshop featured four regular papers, two extended abstracts and two invited talks by Tachio Terauchi (Japan Advanced Institute of Science and Technology) and Maurizio Proietti (IASI-CNR, Italy).
We are grateful to all the people involved in the organization of HCVS 2016 and ETAPS 2016. We also thank the Program Committee, the authors, the reviewers and all the workshop participants for their contribution to the success of HCVS 2016. Finally, we would like to thank EasyChair for providing us with a tool for handling submissions, and EPTCS for publishing the proceedings of the workshop.
Maurizio Proietti (IASI-CNR, Italy)
Constrained Horn Clauses (CHCs) have been advocated as a lingua franca for verifying program correctness, and a number of solvers for proving the satisfiability of such clauses have been recently developed. However, solving CHC satisfiability problems is a very hard (undecidable, in general) task, and the effectiveness of solvers depends very much on the syntactic form of the clauses. For this reason, recent work has suggested that transformation techniques that change the form of the clauses while preserving their satisfiability may be used to alleviate this problem.
In this talk we present recent and ongoing research on transformation techniques for CHCs that can be used to ease satisfiability proofs, and hence program verification. We first present a very general approach based on transformation rules such as unfolding, folding and constraint rewriting. Then we present the clause specialization and predicate tupling techniques that make use of these rules to improve the effectiveness of CHC solving. Clause specialization can be used for simplifying CHCs by exploiting information about the specific property to be verified and the semantics of the programming language. Predicate tupling consists in deriving new predicates that are equivalent to conjunctions of predicates occurring in a given set of CHCs to be solved. We show that predicate tupling is able to strictly improve the effectiveness of CHC solvers. Indeed, we consider CHC solvers based on Linear Arithmetic (LA-solvers) and we show that there are examples of CHCs that are satisfiable, and yet they cannot be solved by any LA-solver. Then we show that, by predicate tupling, we are able to transform the given CHCs into a new form that can be proved satisfiable by an LA-solver. Finally, we present some applications where complex program properties can be proved by transforming their specifications, using clause specialization and predicate tupling, into CHCs that can be solved by LA-solvers.
Tachio Terauchi (Japan Advanced Institute of Science and Technology)
Many of the modern program verifiers are based on the predicate abstraction with CEGAR method, The method looks for a sufficient inductive invariant to prove the given property of the given program by iteratively accumulating predicates that are obtained by analyzing spurious counterexamples, and predicate refinement heuristics like Craig interpolation are used for this purpose. In this talk, we overview our recent work on predicate refinement heuristics in CEGAR. Specifically, we show that a certain strategy for choosing predicates can guarantee the convergence of CEGAR at a modest cost. We also show that choosing small refinements guarantees fast convergence under certain conditions.