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 OctDisplayed time zone: Tijuana, Baja California change
13:30 - 15:00 | |||
13:30 22mTalk | 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 22mTalk | 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 22mTalk | 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 22mTalk | Reasoning on Divergent Computations with Coaxioms OOPSLA DOI |