ECOOP 2015
Sun 5 - Fri 10 July 2015 Prague, Czech Republic
Fri 10 Jul 2015 15:00 - 15:30 at Bohemia - Verification Chair(s): Pavel Parizek

Permission-based veri fication logics such as separation logic have led to the development of many practical veri fication tools over the last decade. Verifi ers employ the separating conjunction A ‡* B to elegantly handle aliasing problems, framing, race conditions, etc. Introduced along with the separating conjunction, the magic wand connective, written A –* B, can describe hypothetical modi fications of the current state, and provide guarantees about the results. Its formal semantics involves quantifying over states: as such, the connective is typically not supported in automatic verifi cation tools. Nonetheless, the magic wand has been shown to be useful in by-hand and mechanised proofs, for example, for specifying loop invariants and partial data structures.

In this paper, we show how to integrate support for the magic wand into an automatic verifi er, requiring low specifi cation overhead from the tool user, due to a novel approach for choosing footprints for magic wand formulas automatically. We show how to extend this technique to interact elegantly with common specifi cation features such as recursive predicates. Our solution is designed to be compatible with a variety of logics and underlying implementation techniques.

We have implemented our approach, and a prototype veri fier is available to download, along with a collection of examples.

Fri 10 Jul

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

15:00 - 16:30
VerificationResearch Track at Bohemia
Chair(s): Pavel Parizek Charles University in Prague
15:00
30m
Talk
Lightweight Support for Magic Wands in an Automatic Verifier
Research Track
Malte Schwerhoff ETH Zurich, Switzerland, Alexander J. Summers ETH Zurich
15:30
30m
Talk
Modular Verification of Finite Blocking in Non-terminating Programs
Research Track
Pontus Boström Abo Akademi University, Peter Müller ETH Zurich
16:00
30m
Talk
Modular Termination Verification
Research Track
Bart Jacobs iMinds - Distrinet, KU Leuven, Dragan Bosnacki Eindhoven University of Technology, The Netherlands, Ruurd Kuiper Eindhoven University of Technology, The Netherlands