Write a Blog >>
PLDI 2020
Mon 15 - Fri 19 June 2020
Fri 19 Jun 2020 11:00 - 11:20 at PLDI Research Papers live stream - Verification II Chair(s): Manu Sridharan

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 Jun
Times are displayed in time zone: Pacific Time (US & Canada) change

10:40 - 12:00: Verification IIPLDI Research Papers at PLDI Research Papers live stream
Chair(s): Manu SridharanUniversity of California Riverside

YouTube lightning session video

10:40 - 11:00
PLDI Research Papers
Sandeep DasguptaUniversity of Illinois at Urbana-Champaign, USA, Sushant DineshUniversity of Illinois at Urbana-Champaign, USA, Deepan VenkateshUniversity of Illinois at Urbana-Champaign, USA, Vikram S. AdveUniversity of Illinois at Urbana-Champaign, USA, Christopher W. FletcherUniversity of Illinois at Urbana-Champaign, USA
11:00 - 11:20
PLDI Research Papers
Krishnendu ChatterjeeIST Austria, Austria, Hongfei FuShanghai Jiao Tong University, China, Amir Kafshdar GoharshadyIST Austria, Austria, Ehsan Kafshdar GoharshadyFerdowsi University of Mashhad, Iran
11:20 - 11:40
PLDI Research Papers
Jason BreckUniversity of Wisconsin-Madison, USA, John CyphertUniversity of Wisconsin-Madison, USA, Zachary KincaidPrinceton University, USA, Thomas RepsUniversity of Wisconsin-Madison, USA
11:40 - 12:00
PLDI Research Papers
Jason R. KoenigStanford University, USA, Oded PadonStanford University, USA, Neil ImmermanUniversity of Massachusetts at Amherst, USA, Alex AikenStanford University, USA