| 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 |
ＥＢ
図書
