Write a Blog >>
Thu 21 Jan 2016 15:35 - 16:00 at Grand Bay North - Track 1: Learning and verification Chair(s): David Monniaux

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.

Conference Day
Thu 21 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

14:20 - 16:00
Track 1: Learning and verificationResearch Papers at Grand Bay North
Chair(s): David MonniauxCNRS, VERIMAG
14:20
25m
Talk
Combining Static Analysis with Probabilistic Models to Enable Market-Scale Analysis
Research Papers
Damien OcteauUniversity of Wisconsin and Pennsylvania State University, Somesh JhaUniversity of Wisconsin, Madison, Matthew DeringPennsylvania State University, Patrick McDanielPennsylvania State University, Alexandre BartelTechnical University Darmstadt, Hongyu LiRice University, Jacques KleinUniversity of Luxembourg, Yves Le TraonUniversity of Luxembourg
Media Attached
14:45
25m
Talk
Abstraction Refinement Guided by a Learnt Probabilistic Model
Research Papers
Radu GrigoreUniversity of Oxford, Hongseok YangUniversity of Oxford, UK
Media Attached
15:10
25m
Talk
Learning Invariants using Decision Trees and Implication Counterexamples
Research Papers
Pranav GargUniversity of Illinois at Urbana-Champaign, Daniel NeiderUniversity of Illinois at Urbana-Champaign, P. MadhusudanUniversity of Illinois at Urbana-Champaign, Dan RothUniversity of Illinois at Urbana-Champaign
Media Attached
15:35
25m
Talk
Symbolic Abstract Data Type Inference
Research Papers
Michael EmmiIMDEA Software Institute, Constantin EneaLIAFA, Université Paris Diderot
Media Attached