Skip to main content
These web pages use cascading style sheet features for formatting. You may still browse the text of the site, but for best results, use a modern CSS-enabled browser.
Title Image

Regular Papers

Bakar Kiasan: Flexible Contract Checking for Critical Systems using Symbolic Execution
     Jason Belt, John Hatcliff, Robby, Patrice Chalin, David Hardin and Xianghua Deng.

Approximate Quantifier Elimination for Propositional Boolean Formulae
     Joerg Brauer and Andy King.

Towards Flight Control Verification using Automated Theorem Proving
     William Denman, Mohamed H. Zaki, Sofiene Tahar and Luis Rodrigues.

Generalized Rabin(1) Synthesis with Applications to Robust System Synthesis
     Rüdiger Ehlers.

Applying Atomicity and Model Decomposition to a Space Craft System in Event-B
     Asieh Salehi Fathabadi, Abdolbaghi Rezazadeh and Michael Butler.

Integrating an Automated Theorem Prover into Agda
     Simon Foster and Georg Struth.

Efficient Predicate Abstraction of Program Summaries
     Arie Gurfinkel, Sagar Chaki and Samir Sapra.

Synthesis for PCTL in Parametric Markov Decision Processes
     Ernst Moritz Hahn, Tingting Han, Alexandru Mereacre and Lijun Zhang.

Formalizing Probabilistic Safety Claims
     Heber Herencia-Zapana, George Hagen and Anthony Narkawicz.

The OpenTheory Standard Theory Library
     Joe Hurd.

Instantiation-Based Invariant Discovery
     Temesghen Kahsai, Yeting Ge and Cesare Tinelli.

Stuttering Mostly Speeds Up Solving Parity Games
     Jeroen Keiren, Sjoerd Cranen and Tim Willemse.

Counterexample-based Error Localization of Behavior Models
     Tsutomu Kumazawa and Tetsuo Tamai.

Call invariants
     Shuvendu Lahiri and Shaz Qadeer.

Symmetry for the Analysis of Dynamic Systems
     Zarrin Langari and Richard Trefler.

Implementing Cryptographic Primitives in the Symbolic Model
     Peeter Laud.

Combining Partial Order Reduction and Symbolic Model Checking to verify LTL properties
     José Vander Meulen and Charles Pecheur.

Model Checking Using SMT and Theory of Lists
     Aleksandar Milicevic and Hillel Kugler.

Generating Data Race Witnesses by an SMT-based Analysis
     Mahmoud Said, Chao Wang, Zijiang Yang and Karem Sakallah.

A Theory of Skiplists with Applications to the Verification of   Concurrent Datatypes
     Alejandro Sanchez and Cesar Sanchez.

CORAL: Solving Complex Constraints for Symbolic PathFinder
     Matheus Souza, Mateus Borges, Marcelo d'Amorim and Corina Pasareanu.

Automated Formal Verification of the TTEthernet Synchronization Quality
     Wilfried Steiner and Bruno Dutertre.

Extending the GWV Security Policy and its Modular Application to a Separation Kernel
     Sergey Tverdyshev.

Automated Test Case Generation with SMT-Solving and Abstract Interpretation
     Jan Peleska, Elena Vorobev and Florian Lapschies.

Towards Informed Swarm Verification
     Anton Wijs.

Scaling up with Event-B: A Case Study
     Faqing Yang and Jean-Pierre Jacquot.

Tool Papers

D-Finder 2: Towards Efficient Correctness of Incremental Design
     Saddek Bensalem, Andreas Griesmayer, Axel Legay, Thanh-Hung Nguyen,
     Joseph Sifakis and Rongjie Yan.

Infer: an Automatic Program Verifier for Memory Safety of C Programs
     Cristiano Calcagno and Dino Distefano.

Model Construction and Priority Synthesis for Simple Interaction Systems
     Chih-Hong Cheng, Barbara Jobstmann, Saddek Bensalem, Rongjie Yan,
     Alois Knoll and Harald Ruess.

jSMTLIB: Tutorial, Validation and Adapter Tools for SMT-LIBv2
     David Cok.

OpenJML: JML for Java 7 by extending OpenJDK
     David Cok.

opaal: A Lattice Model Checker
     Andreas Engelbredt Dalsgaard, Rene Rydhof Hansen, Kenneth Yrke Jørgensen,
     Kim G. Larsen, Mads Chr. Olesen, Petur Olsen and Jiri Srba.

A Tabular Expression Toolbox for Matlab/Simulink
     Colin Eles and Mark Lawford.

LLVM2CSP : Extracting CSP Models from Concurrent Programs
     Moritz Kleine, Björn Bartels, Thomas Goethel, Steffen Helke and Dirk Prenzel.

Multi-Core LTSmin: Marrying Modularity and Scalability
     Alfons Laarman, Jaco van de Pol and Michael Weber.

GiNaCRA: A C++ Library for Real Algebraic Computations
     Ulrich Loup and Erika Ábrahám.

Kopitiam: modular incremental interactive full functional static verification of Java code
     Hannes Mehnert.

Milestones: A Model Checker Combining Symbolic Model Checking and Partial Order Reduction
     José Vander Meulen and Charles Pecheur.