Decidability of Inferring Inductive Invariants
Induction is a successful approach for verification of hardware and software systems. A common practice is to model a system using logical formulas, and then use a decision procedure to verify that some logical formula is an inductive safety invariant for the system. A key ingredient in this approach is coming up with the inductive invariant, which is known as invariant inference. This is a major difficulty, and it is often left for humans or addressed by sound but incomplete abstract interpretation. This paper is motivated by the problem of inductive invariants in shape analysis and in distributed protocols.
This paper approaches the general problem of inferring first-order inductive invariants by restricting the language L of candidate invariants. Notice that the problem of invariant inference in a restricted language L differs from the safety problem, since a system may be safe and still not have any inductive invariant in L that proves safety. Clearly, if L is finite (and if testing an inductive invariant is decidable), then inferring invariants in L is decidable. This paper presents some interesting cases when inferring inductive invariants in L is decidable even when L is an infinite language of universal formulas. Decidability is obtained by restricting L and defining a suitable well-quasi-order on the state space. We also present some undecidability results that show that our restrictions are necessary. We further present a framework for systematically constructing infinite languages while keeping the invariant inference problem decidable. We illustrate our approach by showing the decidability of inferring invariants for programs manipulating linked-lists, and for distributed protocols.
Wed 20 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
16:30 - 17:45
Track 2: Decidability and complexityResearch Papers at Grand Bay South
Chair(s): C.-H. Luke Ong University of Oxford, UK
|Decidability of Inferring Inductive Invariants|
Oded Padon Tel Aviv University, Neil Immerman University of Massachusetts, Amherst, Sharon Shoham , Aleksandr Karbyshev Tel Aviv University, Mooly Sagiv Tel Aviv UniversityMedia Attached
|The Hardness of Data Packing|
Rahman Lavaee , Chen Ding University of RochesterMedia Attached
|The Complexity of Interaction|
Stéphane Gimenez University of Innsbruck, Georg Moser University of InnsbruckMedia Attached