Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Tue 15 Jan 2019 12:00 - 12:30 at Sala III - Software Verification and Synthesis Chair(s): Ori Lahav

We introduce program synthesis with equivalence reduction, a synthesis methodology that utilizes relational specifications over components of a given synthesis domain to reduce the search space. Leveraging a blend of classic and modern techniques from term rewriting, we use relational specifications to discover a canonical representative per equivalence class of programs. We show how to design synthesis procedures that only consider programs in normal form, thus pruning the search space. We discuss how to implement equivalence reduction using efficient data structures, and demonstrate the significant reductions it can achieve in synthesis time.

Tue 15 Jan

Displayed time zone: Belfast change

11:00 - 12:30
Software Verification and SynthesisVMCAI at Sala III
Chair(s): Ori Lahav Tel Aviv University
11:00
30m
Talk
Mechanically Proving Determinacy of Hierarchical Block Diagram Translations
VMCAI
Viorel Preoteasa , Iulia Dragomir , Stavros Tripakis Aalto University and UC Berkeley
Link to publication DOI Pre-print File Attached
11:30
30m
Talk
euforia: Complete Software Model Checking with Uninterpreted Functions
VMCAI
12:00
30m
Talk
Program Synthesis with Equivalence Reduction
VMCAI
Calvin Smith University of Wisconsin - Madison, Aws Albarghouthi University of Wisconsin-Madison