VMCAI 2012 Accepted Papers

Nathaniel Charlton, Ben Horsfall and Bernhard Reus. Crowfoot: a verifier for higher order store programs
Samik Basu, Tevfik Bultan and Meriem Ouederni. Synchronizability for Verification of Asynchronously Communicating Systems
Christian Von Essen and Barbara Jobstmann. Synthesizing Efficient Controllers
Dmitry Bugaychenko. On Application of Multi-Rooted Binary Decision Diagrams to Probabilistic Model Checking
Woosuk Lee, Wonchan Lee and Kwangkeun Yi. Sound Non-Statistical Clustering of Static Analysis Alarms
Joshua Sack and Lijun Zhang. A general framework for probabilistic characterizing formulae
Uri Klein, Nir Piterman and Amir Pnueli. Effective Synthesis of Asynchronous Systems from GR(1) Specifications
Kedar Namjoshi and Richard Trefler. Local Symmetry and Compositional Verification
Pietro Ferrara and Peter Müller. Automatic Inference of Access Permissions
Bernd Finkbeiner and Swen Jacobs. Lazy Synthesis
Falk Howar, Bernhard Steffen, Sofia Cassel and Bengt Jonsson. Inferring Canonical Register Automata
Sagar Chaki, Arie Gurfinkel and Ofer Strichman. Regression Verification for Multi-Threaded Programs
Damien Zufferey, Thomas Wies and Thomas Henzinger. Ideal Abstractions for Well-Structured Transition Systems
Khalil Ghorbal, Franjo Ivancic, Gogul Balakrishnan, Naoto Maeda and Aarti Gupta. Donut Domains: Efficient Non-Convex Domains for Abstract Interpretation
Johannes Kinder and Dmitry Kravchenko. Alternating Control Flow Reconstruction
Stan Rosenberg, Anindya Banerjee and David Naumann. Decision Procedures for Region Logic
Stephen F. Siegel and Timothy Zirkel. Symbolic Execution with Collective Loop Invariants
Rayna Dimitrova, Bernd Finkbeiner, Mate Kovacs, Markus Rabe and Helmut Seidl. Model Checking Secrecy in Reactive Systems
Krishnendu Chatterjee and Vishwanath Raman. Synthesizing Protocols for Digital Contract Signing
Aws Albarghouthi, Arie Gurfinkel and Marsha Chechik. Whale: An Interpolation-based Algorithm for Inter-procedural Verification
Evren Ermis, Jochen Hoenicke and Andreas Podelski. Splitting via Interpolants
Amir Ben-Amram, Samir Genaim and Abu Naser Masud. On the Termination of Integer Loops
Everett Morse, Eric Mercer and Jay Mccarthy. Modeling Asynchronous Message Passing for C Programs
Duckki Oe, Aaron Stump, Corey Oliver and Kevin Clancy. A Verified Modern SAT Solver
Laura Bozzelli and Sophie Pinchinat. Verification of gap-order constraint abstractions of counter systems
Rustan Leino. Automating induction with an SMT solver