| James Baxter and Ana Cavalcanti. Algebraic Compilation of Safety-Critical Java Bytecode |
| Jörg Pfähler, Gidon Ernst, Stefan Bodenmüller, Gerhard Schellhorn and Wolfgang Reif. Modular Verification of Order-Preserving Write-Back Caches |
| Mark Utting, David Pearce and Lindsay Groves. Making Whiley Boogie! |
| Stefan Blom, Saeed Darabi, Marieke Huisman and Wytse Oortwijn. The VerCors Tool Set: Verification of Parallel and Concurrent Software |
| Simone Silvetti, Alberto Policriti and Luca Bortolussi. An Active Learning Approach to the Falsification of Black Box Cyber-Physical Systems |
| Andrii Kovalov, Elisabeth Lobe, Andreas Gerndt and Daniel Lüdtke. Task-Node Mapping in an Arbitrary Computer Network using SMT Solver |
| Yuting Chen and Carlo A. Furia. Triggerless Happy: Intermediate Verification with a First-Order Prover |
| Albert Rizaldi, Jonas Keinholz, Jochen Feldle, Fabian Immler, Matthias Althoff, Eric Hilgendorf and Tobias Nipkow. Formalising Traffic Rules for Autonomous Vehicles Involving Multiple Lanes in Isabelle/HOL |
| Fahrurrozi Rahman and Juliana Küster Filipe Bowles. Formal Verification of CNL Health Recommendations |
| Danilo Bruschi, Andrea Di Pasquale, Silvio Ghilardi, Andrea Lanzi and Elena Pagani. Formal verification of ARP (Address Resolution Protocol) through SMT-based model checking - A case study - |
| Olaf Owe, Toktam Ramezanifarkhani and Elahe Fazeldehkordi. Hoare-style Reasoning from Multiple Contracts |
| Stephen Gilmore, Daniel Reijsbergen and Andrea Vandin. Transient and Steady-State Statistical Analysis for Discrete Event Simulators |
| Ludovic Henrio, Cosimo Laneve and Vincenzo Mastandrea. Analysis of synchronisation patterns in stateful active objects |
| Sven Linker. Spatial Reasoning about Motorway Traffic Safety with Isabelle/HOL |
| Joao F. Ferreira, Saul A. Johnson, Alexandra Mendes and Phillip J. Brooke. Certified Password Quality — A Case Study Using Coq and Linux Pluggable Authentication Modules |
| Pedro Ribeiro, Alvaro Miyazawa, Wei Li, Ana Cavalcanti and Jon Timmis. Modelling and Verification of Timed Robotic Controllers |
| Bernhard Beckert, Suhyun Cha, Mattias Ulbrich, Birgit Vogel-Heuser and Alexander Weigl. Generalised Test Tables – a Practical Specification Language for Reactive Systems |
| Ajay Krishna, Pascal Poizat and Gwen Salaün. VBPMN: Automated Verification of BPMN Processes |
| Barbara Kordy and Wojciech Widel. How well can I secure my system? |
| Murat Moran and Dan Wallach. Verification of STAR-Vote and Evaluation of FDR and ProVerif |
| Dominic Steinhöfel and Nathan Wasser. A New Invariant Rule for the Analysis of Loops with Non-standard Control Flows |
| Bernhard Beckert, Thorsten Bormer, Stephan Gocht, Mihai Herda, Daniel Lentzsch and Mattias Ulbrich. SemSlice: Exploiting Relational Verification for Automatic Program Slicing |
| Florian Frohn and Jürgen Giesl. Complexity Analysis for Java with AProVE |
| Hao Wu. MaxUSE: A Tool for Finding Achievable Constraints and Conflicts for Inconsistent UML Class Diagrams |
| Dalay Israel de Almeida Pereira, Marcel Vinicius Medeiros Oliveira, Madiel Conserva Filho and Sarah Raquel Da Rocha Silva. BTS: A Tool for Formal Component-based Development |
| Ferruccio Damiani, Michael Lienhardt, Radu Muschevici and Ina Schaefer. An Extension of the ABS Toolchain with a Mechanism for Type Checking SPLs |
| Stavros Aronis, Scott Fritchie and Kostis Sagonas. Testing and Verifying Chain Repair Methods for CORFU Using Stateless Model Checking |
| Wei Ji, Farn Wang and Peng Wu. Synthesizing Coalitions for Multi-Agent Games |