Polynomial Invariant Generation for Non-deterministic Recursive Programs
We consider the classical problem of invariant generation for programs with polynomial assignments and focus on synthesizing invariants that are a conjunction of strict polynomial inequalities. We present a sound and semi-complete method based on positivstellensaetze, i.e. theorems in semi-algebraic geometry that characterize positive polynomials over a semi-algebraic set.
On the theoretical side, the worst-case complexity of our approach is subexponential, whereas the worst-case
complexity of the previous complete method (Kapur, ACA 2004) is doubly-exponential. Even when restricted to linear invariants, the best previous complexity for complete invariant generation is exponential (Colon et al, CAV 2003). On the practical side, we reduce the invariant generation problem to quadratic programming (QCLP), which is a classical optimization problem with many industrial solvers. We demonstrate the applicability of our approach by providing experimental results on several academic benchmarks. To the best of our knowledge, the only previous invariant generation method that provides completeness guarantees for invariants consisting of polynomial inequalities is (Kapur, ACA 2004), which relies on quantifier elimination and cannot even handle toy programs such as our running example.
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 |