Full Papers
- Reynald Affeldt, David Nowak and Kiyoshi Yamada.
Certifying assembly with formal cryptographic proofs: the case of BBS. - Étienne André, Laurent Fribourg and Jeremy Sproston.
Behavior-preserving relaxation of timing bounds of probabilistic timed automata. - Ulrich Berger and Sion Lloyd.
A coinductive approach to verified exact real number computation. - Loïc Besnard, Thierry Gautier, Matthieu Moy, Jean-Pierre Talpin,
Kenneth Johnson and Florence Maraninchi.
Automatic translation of C/C++ parallel code into synchronous formalism using an SSA intermediate form. - Neil Brown.
Automatically generating CSP models for communicating Haskell processes. - Nathaniel Charlton and Bernhard Reus.
A decidable class of verification conditions for programs with higher order store. - Holger Gast and Julia Trieflinger.
High-level proofs about low-level programs. - Michael Huth, Nir Piterman and Huaxin Wang.
A workbench for preprocessor design and evaluation: toward benchmarks for parity games. - Hristina Palikareva, Joel Ouaknine and Bill Roscoe.
Faster FDR counterexample generation using SAT-solving. - Julio Peralta and Thierry Gautier.
Towards SMV Model Checking of Signal (multi-clocked) specifications. - Frank Stappers and Michel Reniers.
Verification of safety requirements for program code using data abstraction. - Beeta Vajar, Steve Schneider and Helen Treharne.
Mobile CSP||B.
Short Contributions
- Anaheed Ayoub, Ayman Wahba and Mohamed Sheirah.
B Based Verification for Real Time Systems. - Alan Bundy, Gudmund Grov and Cliff Jones.
Learning from experts to aid the automation of proof search. - Karim Kanso and Anton Setzer.
Specifying Railway Interlocking Systems. - Savas Konur, Ahmed Al Zahrani and Michael Fisher.
Verification of a Message Forwarding System using PRISM. - Alexei Lisitsa.
Reachability as deducibility, finite countermodels and verification. - Sadouanouan Malo and Annie Choquet-Geniet.
Analysis of critical scalable real-time systems by means of Petri nets. - Nikolaos Papanikolaou, Sadie Creese and Michael Goldsmith.
Policy Refinement Checking. - Shamim Ripon, Alice Miller and Alastair Donaldson.
A Semantic Embedding of Promela-Lite in PVS. - Monika Seisenberger.
Program Verification via Extraction from Coinductive Proofs. - Luke Ong and Nikos Tzevelekos.
Functional Reachability.