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

We present TiML (Timed ML), an ML-like functional language with time-complexity annotations in types. It uses indexed types to express sizes of data structures and upper bounds on running time of functions; and refinement kinds to constrain these indices, expressing data-structure invariants and pre/post-conditions. Indexed types are flexible enough that TiML avoids a built-in notion of ``size,'' and the programmer can choose to index user-defined datatypes in any way that helps her analysis. TiML's distinguishing characteristic is supporting highly automated time-bound verification applicable to data structures with nontrivial invariants. The programmer provides type annotations, and the typechecker generates verification conditions that are discharged by an SMT solver. Type and index inference are supported to lower annotation burden, and, furthermore, big-O complexity can be inferred from recurrences generated during typechecking by a recurrence solver based on heuristic pattern matching (e.g. using the Master Theorem to handle divide-and-conquer-like recurrences). We have evaluated TiML's usability by implementing a broad suite of case-study modules, demonstrating that TiML, though lacking full automation and theoretical completeness, is versatile enough to verify worst-case and/or amortized complexities for algorithms and data structures like classic list operations, merge sort, Dijkstra's shortest-path algorithm, red-black trees, Braun trees, functional queues, and dynamic tables with bounds like $m n \log n$. The learning curve and annotation burden are reasonable, as we argue with empirical results on our case studies. We formalized TiML's type-soundness proof in Coq.

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