Wed 17 Jun 2015 16:50 - 17:15 at PLDI Main BLUE (Portland 254-255) - Synthesis II Chair(s): Işıl Dillig

We present a complete method for synthesizing lexicographic linear ranking functions (and thus proving termination), supported by inductive invariants, in the case where the transition relation of the program includes disjunctions and existentials (large block encoding of control flow).

Previous work would either synthesize a ranking function at every basic block head, not just loop headers, which reduces the scope of programs that may be proved to be terminating, or expand large block transitions including tests into (exponentially many) elementary transitions, prior to computing the ranking function, resulting in a very large global constraint system. In contrast, our algorithm incrementally refines a global linear constraint system according to extremal counterexamples: only constraints that exclude spurious solutions are included.

Experiments show marked performance and scalability improvements compared to other systems.

Wed 17 Jun

Displayed time zone: Tijuana, Baja California change

16:00 - 17:40
Synthesis IIResearch Papers at PLDI Main BLUE (Portland 254-255)
Chair(s): Işıl Dillig University of Texas, Austin
16:00
25m
Talk
Concurrency Debugging with Differential Schedule Projections
Research Papers
Nuno Machado INESC-ID / Instituto Superior Técnico, Universidade de Lisboa, Brandon Lucia Carnegie Mellon University, Luís Rodrigues Universidade de Lisboa, Instituto Superior Técnico, INESC-ID
Media Attached
16:25
25m
Talk
Synthesis of Machine Code from Semantics
Research Papers
Venkatesh Srinivasan University of Wisconsin - Madison, Thomas Reps University of Wisconsin - Madison and Grammatech Inc.
Media Attached
16:50
25m
Talk
Synthesis of ranking functions using extremal counterexamples
Research Papers
Laure Gonnord University of Lyon & LIP, France, David Monniaux CNRS, VERIMAG, Gabriel Radanne Université Denis Diderot Paris 7, PPS
Media Attached
17:15
25m
Talk
Type-and-Example-Directed Program Synthesis
Research Papers
Peter-Michael Osera University of Pennsylvania, Steve Zdancewic
Media Attached