Symbolic Abstract Data Type Inference
Formal specification is a vital ingredient to scalable verification of software systems. In the case of efficient implementations of concurrent objects like atomic registers, queues, and locks, symbolic formal representations of their abstract data types (ADTs) enable efficient modular reasoning, decoupling clients from implementations. Writing adequate formal specifications, however, is a complex task requiring rare expertise. In practice, programmers write reference implementations as informal specifications.
In this work we demonstrate that effective symbolic ADT representations can be automatically generated from the executions of reference implementations. Our approach exploits two key features of naturally-occurring ADTs: violations can be decomposed into a small set of representative patterns, and these patterns manifest in executions with few operations. By identifying certain algebraic properties of naturally-occurring ADTs, and exhaustively sampling executions up to a small number of operations, we generate concise symbolic ADT representations which are complete in practice, enabling the application of efficient symbolic verification algorithms without the burden of manual specification. Furthermore, the concise ADT violation patterns we generate are human-readable, and can serve as useful, formal documentation.
Thu 21 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
14:20 - 16:00
Track 1: Learning and verificationResearch Papers at Grand Bay North
Chair(s): David Monniaux CNRS, VERIMAG
|Combining Static Analysis with Probabilistic Models to Enable Market-Scale Analysis|
Damien Octeau University of Wisconsin and Pennsylvania State University, Somesh Jha University of Wisconsin, Madison, Matthew Dering Pennsylvania State University, Patrick McDaniel Pennsylvania State University, Alexandre Bartel Technical University Darmstadt, Hongyu Li Rice University, Jacques Klein University of Luxembourg, Yves Le Traon University of LuxembourgMedia Attached
|Abstraction Refinement Guided by a Learnt Probabilistic Model|
Radu Grigore University of Oxford, Hongseok Yang University of Oxford, UKMedia Attached
|Learning Invariants using Decision Trees and Implication Counterexamples|
Pranav Garg University of Illinois at Urbana-Champaign, Daniel Neider University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign, Dan Roth University of Illinois at Urbana-ChampaignMedia Attached
|Symbolic Abstract Data Type Inference|
Michael Emmi IMDEA Software Institute, Constantin Enea LIAFA, Université Paris DiderotMedia Attached