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

We propose an approach for the modular specification and verification of total correctness properties of object-oriented programs. We start from an existing program logic for partial correctness based on separation logic and abstract predicate families. We extend it with call permissions qualified by an arbitrary ordinal number, and we define a specification style that properly hides implementation details, based on the ideas of using methods and bags of methods as ordinals, and exposing the bag of methods reachable from an object as an abstract predicate argument. These enable each method to abstractly request permission to call all methods reachable by it any finite number of times, and to delegate similar permissions to its callees. We illustrate the approach with several examples.

We then extend the approach to a concurrent setting, by incorporating an existing approach for verifying deadlock-freedom of channels and locks. Our main contribution here is to achieve information hiding by using method bags for lock ordering. We also show how our approach prevents infinite thread creation and enables verification of termination of fine-grained concurrent algorithms involving compare-and-swap loops.

We explain how our approach can be used also to verify liveness properties of non-terminating programs.

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