FSE 2016 All Events

24th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE 2016), November 13–18, 2016, Seattle, WA, USA

Desktop Layout

Session 7: Verification
Research Papers
Emerald 1, Chair: Abhik Roychoudhury
SMT-Based Verification of Parameterized Systems
Arie Gurfinkel, Sharon Shoham, and Yuri Meshman
(Software Engineering Institute, USA; University of Waterloo, Canada; Tel Aviv University, Israel; Technion, Israel)
Publisher's Version
Abstract: It is well known that verification of safety properties of sequential programs is reducible to satisfiability modulo theory of a first-order logic formula, called a verification condition (VC). The reduction is used both in deductive and automated verification, the difference is only in whether the user or the solver provides candidates for inductive invariants. In this paper, we extend the reduction to parameterized systems consisting of arbitrary many copies of a user-specified process, and whose transition relation is definable in first-order logic modulo theory of linear arithmetic and arrays. We show that deciding whether a parameterized system has a universally quantified inductive invariant is reducible to satisfiability of (non-linear) Constraint Horn Clauses (CHC). As a consequence of our reduction, we obtain a new automated procedure for verifying parameterized systems using existing PDR and CHC engines. While the new procedure is applicable to a wide variety of systems, we show that it is a decision procedure for several decidable fragments.

Authors:


Time stamp: 2019-03-19T15:43:29+01:00