Quantified first-order formulas, often with quantifier alternations, are increasingly used in the verification of complex systems. While automated theorem provers for first-order logic are becoming more robust, invariant inference tools that handle quantifiers are currently restricted to purely universal formulas. We define and analyze first-order quantified separators and their application to inferring quantified invariants with alternations. A \emph{separator} for a given set of positively and negatively labeled structures is a formula that is true on positive structures and false on negative structures. We investigate the problem of finding a separator from the class of formulas in prenex normal form with a bounded number of quantifiers and show this problem is NP-complete by reduction to and from SAT. We also give a practical separation algorithm, which we use to demonstrate the first invariant inference procedure able to infer invariants with quantifier alternations.
Fri 19 JunDisplayed time zone: Pacific Time (US & Canada) change
10:40 - 12:00 | Verification IIPLDI Research Papers at PLDI Research Papers live stream Chair(s): Manu Sridharan University of California Riverside | ||
10:40 20mTalk | Scalable Validation of Binary Lifters PLDI Research Papers Sandeep Dasgupta University of Illinois at Urbana-Champaign, USA, Sushant Dinesh University of Illinois at Urbana-Champaign, USA, Deepan Venkatesh University of Illinois at Urbana-Champaign, USA, Vikram S. Adve University of Illinois at Urbana-Champaign, USA, Christopher W. Fletcher University of Illinois at Urbana-Champaign, USA | ||
11:00 20mTalk | Polynomial Invariant Generation for Non-deterministic Recursive Programs PLDI Research Papers Krishnendu Chatterjee IST Austria, Austria, Hongfei Fu Shanghai Jiao Tong University, China, Amir Kafshdar Goharshady IST Austria, Austria, Ehsan Kafshdar Goharshady Ferdowsi University of Mashhad, Iran | ||
11:20 20mTalk | Templates and Recurrences: Better Together PLDI Research Papers Jason Breck University of Wisconsin-Madison, USA, John Cyphert University of Wisconsin-Madison, USA, Zachary Kincaid Princeton University, USA, Thomas Reps University of Wisconsin-Madison, USA | ||
11:40 20mTalk | First-Order Quantified Separators PLDI Research Papers Jason R. Koenig Stanford University, USA, Oded Padon Stanford University, USA, Neil Immerman University of Massachusetts at Amherst, USA, Alex Aiken Stanford University, USA |