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.

Thu 21 Jan

Hide past events
POPL-2016-papers
14:20 - 16:00: Research Papers - Track 1: Learning and verification at Grand Bay North
Chair(s): David MonniauxCNRS, VERIMAG
POPL-2016-papers14:20 - 14:45
Talk
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
POPL-2016-papers14:45 - 15:10
Talk
Radu GrigoreUniversity of Oxford, Hongseok YangUniversity of Oxford, UK
Media Attached
POPL-2016-papers15:10 - 15:35
Talk
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
POPL-2016-papers15:35 - 16:00
Talk
Michael EmmiIMDEA Software Institute, Constantin EneaLIAFA, Université Paris Diderot
Media Attached