Write a Blog >>
SPLASH 2017
Sun 22 - Fri 27 October 2017 Vancouver, Canada
Thu 26 Oct 2017 13:30 - 13:52 at Regency C - Verification Chair(s): Jonathan Edwards

Algorithms that create and mutate graph data structures are challenging to implement correctly. However, verifying even basic properties of low-level implementations, such as referential integrity and memory safety, remains non-trivial. Furthermore, any extension to such a data structure multiplies the complexity of its implementation, while compounding the challenges in reasoning about correctness. We take a language design approach to this problem. We propose Seam, a language for expressing local edits to graph-like data structures, based on a relational data model, and such that data integrity can be verified automatically. We present a verification method that leverages an SMT solver, and prove it sound and precise (complete modulo termination of the SMT solver). We evaluate the verification capabilities of Seam empirically, and demonstrate its applicability to a variety of examples, most notably a new class of verification tasks derived from geometric remeshing operations used in scientific simulation and computer graphics. We describe our prototype implementation of a Seam compiler that generates low-level code, which can then be integrated into larger applications. We evaluate our compiler on a sample application, and demonstrate competitive execution time, compared to hand-written implementations.

Thu 26 Oct

Displayed time zone: Tijuana, Baja California change

13:30 - 15:00
VerificationOOPSLA at Regency C
Chair(s): Jonathan Edwards
13:30
22m
Talk
Seam: Provably Safe Local Edits on Graphs
OOPSLA
Manolis Papadakis Stanford University, USA, Gilbert Louis Bernstein Stanford University, USA, Rahul Sharma Microsoft Research, Alex Aiken Stanford University, Pat Hanrahan Stanford University, USA
DOI
13:52
22m
Talk
TiML: A Functional Language for Practical Complexity Analysis with Invariants
OOPSLA
Peng Wang Massachusetts Institute of Technology, USA, Di Wang Peking University, China, Adam Chlipala Massachusetts Institute of Technology, USA
DOI
14:15
22m
Talk
FairSquare: Probabilistic Verification of Program Fairness
OOPSLA
Aws Albarghouthi University of Wisconsin-Madison, Loris D'Antoni University of Wisconsin–Madison, Samuel Drews University of Wisconsin-Madison, Aditya Nori
DOI
14:37
22m
Talk
Reasoning on Divergent Computations with Coaxioms
OOPSLA
Davide Ancona University of Genova, Francesco Dagnino , Elena Zucca University of Genova
DOI