Wed 17 Jun 2015 14:00 - 14:25 at PLDI Main RED (Portland 256) - Logic Chair(s): Nate Foster

We consider the problem of automated reasoning about dynamically manipulated data structures. Essential properties are encoded as predicates whose definitions are formalised via user-defined recursive rules. Traditionally, proving relationships between such properties is limited to the unfold-and-match (U+M) paradigm which employs systematic transformation steps of folding/unfolding the rules. A proof, using U+M, succeeds when we find a sequence of transformations that produces a final formula which is obviously provable by simply matching terms.

Our contribution here is the addition of the fundamental principle of induction to this automated process. We first show that some proof obligations that are dynamically generated in the process can be used as induction hypotheses in the future, and then we show how to use these hypotheses in an induction step which generates a new proof obligation aside from those obtained from the fold/unfold operations. While the adding of induction is an obvious need in general, no automated method has managed to include this in a systematic and general way. The main reason for this is the problem of avoiding circular reasoning. Our main result overcomes this with a novel checking condition. Our contribution is a proof method which – beyond U+M – performs automatic formula re-writing by treating previously encountered obligations in each proof path as possible induction hypotheses.

In the practical evaluation part of this paper, we show how the commonly used technique of using unproven lemmas can be avoided, using realistic benchmarks. This not only removes the current burden of coming up with the appropriate lemmas, but also significantly boosts up the verification process, since lemma applications, coupled with unfolding, often induce a very large search space. In the end, our method automatically reasons about a new class of formulas arising from practical program verification.

Wed 17 Jun

Displayed time zone: Tijuana, Baja California change

14:00 - 15:40
LogicResearch Papers at PLDI Main RED (Portland 256)
Chair(s): Nate Foster Cornell University
14:00
25m
Talk
Automatic Induction Proofs of Data-Structures in Imperative Programs
Research Papers
Duc-Hiep Chu National University of Singapore, Joxan Jaffar National University of Singapore, Minh-Thai Trinh National University of Singapore
Media Attached
14:25
25m
Talk
Compositional Certified Resource Bounds
Research Papers
Quentin Carbonneaux Yale University, Jan Hoffmann Yale University, Zhong Shao Yale University
Link to publication Media Attached
14:50
25m
Talk
Peer-to-peer Affine Commitment using Bitcoin
Research Papers
Karl Crary Carnegie Mellon University, Michael J. Sullivan
Media Attached
15:15
25m
Talk
Termination and Non-Termination Specification Inference
Research Papers
Ton Chanh Le National University of Singapore, Shengchao Qin Teesside University, Wei-Ngan Chin National University of Singapore
Media Attached