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

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.

Conference Day
Fri 19 Jun

Displayed 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
20m
Talk
Scalable Validation of Binary Lifters
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
20m
Talk
Polynomial Invariant Generation for Non-deterministic Recursive Programs
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
20m
Talk
Templates and Recurrences: Better Together
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
20m
Talk
First-Order Quantified Separators
PLDI Research Papers
Jason R. KoenigStanford University, USA, Oded PadonStanford University, USA, Neil ImmermanUniversity of Massachusetts at Amherst, USA, Alex AikenStanford University, USA