Invited Talks / I: |
From Retrospective Verification to Forward-Looking Development / K. Rustan ; M. Leino |
Specifications for Free / Andreas Zeller |
Invited Tutorials / II: |
The Theory and Practice of SALT / Andreas Bauer ; Martin Leucker |
VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java / Bart Jacobs ; Jan Smans ; Pieter Philippaerts ; Frédéric Vogels ; Willem Penninckx ; Prank Piessens |
Verifying Functional Correctness of C Programs with VCC / Michal Moskal |
Regular Papers / III: |
Bakar Kiasan: Flexible Contract Checking for Critical Systems Using Symbolic Execution / Jason Belt ; John Hatcliff ; Robby ; Patrice Chalin ; David Hardin ; Xianghua Deng |
Approximate Quantifier Elimination for Propositional Boolean Formulae / Jörg Brauer ; Andy King |
Towards Flight Control Verification Using Automated Theorem Proving / William Denman ; Mohamed H. Zaki ; Sofiène Tahar ; Luis Rodrigues |
Generalized Rabin(1) Synthesis with Applications to Robust System Synthesis / Rüdiger Ehlers |
Integrating an Automated Theorem Prover into Agda / Simon Foster ; Georg Struth |
Efficient Predicate Abstraction of Program Summaries / Arie Gurfinkel ; Sagar Chaki ; Samir Sapra |
Synthesis for PCTL in Parametric Markov Decision Processes / Ernst Moritz Hahn ; Tingling Han ; Lijun Zhang |
Formalizing Probabilistic Safety Claims / Heber Herencia-Zapana ; George Hagen ; Anthony Narkawicz |
The Open Theory Standard Theory Library / Joe Hurd |
Instantiation-Based Invariant Discovery / Temesghen Kahsai ; Yeting Ge ; Cesare Tinelli |
Stuttering Mostly Speeds Up Solving Parity Games / Sjoerd Cranen ; Jeroen J.A. Keiren ; Tim A.C. Willemse |
Counterexample-Based Error Localization of Behavior Models / Tsutomu Kumazawa ; Tetsuo Tamai |
Call Invariants / Shuvendu K. Lahiri ; Shaz Qadeer |
Symmetry for the Analysis of Dynamic Systems / Zarrin Langari ; Richard Trefler |
Implementing Cryptographic Primitives in the Symbolic Model / Peeter Laud |
Model Checking Using SMT and Theory of Lists / Aleksandar Milicevic ; Hillel Kugler |
Automated Test Case Generation with SMT-Solving and Abstract Interpretation / Jan Peleska ; Elena Vorobev ; Florian Lapschies |
Generating Data Race Witnesses by an SMT-Based Analysis / Mahmoud Said ; Chao Wang ; Zijiang Yang ; Karem Sakallah |
Applying Atomicity and Model Decomposition to a Space Craft System in Event-B / Asieh Salehi Fathabadi ; Abdolbaghi Rezazadeh ; Michael Butler |
A Theory of Skiplists with Applications to the Verification of Concurrent Datatypes / Alejandro Sánchez ; César Sánchez |
Coral: Solving Complex Constraints for Symbolic PathFinder / Matheus Souza ; Mateus Borges ; Marcelo d'Amorim ; Corina S. Pasareanu |
Automated Formal Verification of the TTEthernet Synchronization Quality / Wilfried Steiner ; Bruno Dutertre |
Extending the GWV Security Policy and Its Modular Application to a Separation Kernel / Sergey Tverdyshev |
Combining Partial-Order Reduction and Symbolic Model Checking to Verify LTL Properties / José Vander Meulen ; Charles Pecheur |
Towards Informed Swarm Verification / Anton Wijs |
Scaling Up with Event-B: A Case Study / Faqing Yang ; Jean-Pierre Jacquot |
Tool Papers / IV: |
D-Finder 2: Towards Efficient Correctness of Incremental Design / Saddek Bensalem ; Andreas Griesmayer ; Axel Legay ; Thanh-Hung Nguyen ; Joseph Sifakis ; Rongjie Yan |
Infer: An Automatic Program Verifier for Memory Safety of C Programs / Cristiano Calcagno ; Dino Distefano |
Model Construction and Priority Synthesis for Simple Interaction Systems / Chih-Hong Cheng ; Barbara Jobstmann ; Alois Knoll ; Harald Ruess |
OpenJML: JML for Java 7 by Extending OpenJDK / David R. Cok |
jSMTLIB: Tutorial, Validation and Adapter Tools for SMT-LIBv2 |
opaal: A Lattice Model Checker / Andreas Engelbredt Dalsgaard ; René Rydhof Hansen ; Kenneth Yrke Jørgensen ; Kim Gulstrand Larsen ; Mads Chr. Olesen ; Petur Olsen ; Jirà Srba |
A Tabular Expression Toolbox for Matlab/Simulink / Colin Eles ; Mark Lawford |
LLVM2CSP: Extracting CSP Models from Concurrent Programs / Moritz Kleine ; Björn Bartels ; Thomas Göthel ; Steffen Helke ; Dirk Prenzel |
Multi-Core LTSmin: Marrying Modularity and Scalability / Alfons Laarman ; Jaco van de Pol ; Michael Weber |
Ginacra: A C++ Library or Real Algebraic Computations / Ulrich Loup ; 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 |
Author Index |
Invited Talks / I: |
From Retrospective Verification to Forward-Looking Development / K. Rustan ; M. Leino |
Specifications for Free / Andreas Zeller |