Programme‎ > ‎

Accepted papers

(A) Research papers

Christian Engel and Peter Schmitt
A Formalization of the RTSJ Scoped Memory Model in Dynamic Logic

David Faitelson and Shmuel Tyszberowicz
Data refinement based testing

Christoph Gladisch
Satisfiability Solving and Model Generation for Quantified First-order Logic Formulas

Asma Tafat, Sylvain Boulmé and Claude Marché
A Refinement Methodology for Object-Oriented Programs

Séverine Maingaud, Vincent Balat, Richard Bubel, Reiner Hähnle and Alexandre Miquel
Specifying Imperative ML-like programs using Dynamic Logic

Peter H. Schmitt, Mattias Ulbrich and Benjamin Weiss
Dynamic Frames in Java Dynamic Logic

Davide Ancona, Andrea Corradi, Giovanni Lagorio and Ferruccio Damiani
Abstract compilation of object-oriented languages into coinductive CLP(X): when type inference meets verification

Mattias Ulbrich
A Dynamic Logic for Unstructured Programs with Embedded Assertions

Ilham W. Kurnia, Arnd Poetzsch-Heffter and Yannick Welsch
State-based Object Models are more Abstract than Trace-based Models: Towards a Unified Specification Framework

Samir Chouali, Sebti Mouelhi and Hassan Mountassir
Adapting Components using Interface Automata strengthened by Action Semantics

Einar Broch Johnsen, Olaf Owe, Rudolf Schlatte and Silvia Lizeth Tapia Tarifa
Validating Timed Models of Deployment Components with Parametric Concurrency

(B) System descriptions

Daniel M. Zimmerman and Rinkesh Nagmoti
JMLUnit: The Next Generation

Marieke Huisman and Dilian Gurov
CVPP: A Tool Set for Compositional Verification of Control-Flow Safety Properties

Laurent Hubert, Nicolas Barré, Frédéric Besson, Delphine Demange, Thomas Jensen, Vincent Monfort, David Pichardie and Tiphaine Turpin
SAWJA: Static Analysis Workshop for Java

(C) Experience reports / case studies

Jens Gerlach and Jochen Burghardt
An Experience Report on the Verification of Algorithms  in the C++ Standard Library using Frama-C

Dillon Pariente and Emmanuel Ledinot
Formal Verification of Industrial C Code using Frama-C: a Case Study

Crystal Din, Richard Bubel and Reiner Haehnle
Verification of Variable Software: An Experience Report

Wei Wei, Vitaly Kozyura, Andreas Roth Roth and Sebastian Wieczorek
Checking Consistency Between Message Choreographies And Their Implementation Models

Dermot Cochran and Joe Kiniry
A Formally Specified and Verified Ballot Counting System for Irish PR-STV Elections

(D) Position papers / work in progress

Daniel Bruns, Vladimir Klebanov and Ina Schaefer
Verification of Software Product Lines: Reducing the Effort with Delta-oriented Slicing and Proof Reuse

Gabriele Paganelli
Verification Based Test Case Generation for Scoped Memory in Safety-Critical Java

Casandra Holotescu
Controlling the Unknown

Markus Wagner and Thorsten Bormer
Testing a Verifying Compiler

Jurriaan Rot, Marcello Bonsangue and Frank de Boer
A Pushdown Automaton for Unbounded Object Creation