VMCAI 2012

29 papers

1. A General Framework for Probabilistic Characterizing Formulae · Joshua Sack, Lijun Zhang
2. Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data · Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Mihaela Sighireanu
3. Alternating Control Flow Reconstruction · Johannes Kinder, Dmitry Kravchenko
4. Automatic Inference of Access Permissions · Pietro Ferrara, Peter Müller
5. Automating Induction with an SMT Solver · K. Rustan M. Leino
6. Crowfoot: A Verifier for Higher-Order Store Programs · Nathaniel Charlton, Ben Horsfall, Bernhard Reus
7. Decision Procedures for Region Logic · Stan Rosenberg, Anindya Banerjee, David A. Naumann
8. Donut Domains: Efficient Non-convex Domains for Abstract Interpretation · Khalil Ghorbal, Franjo Ivancic, Gogul Balakrishnan, Naoto Maeda, Aarti Gupta
9. Effective Synthesis of Asynchronous Systems from GR(1) Specifications · Uri Klein, Nir Piterman, Amir Pnueli
10. Ideal Abstractions for Well-Structured Transition Systems · Damien Zufferey, Thomas Wies, Thomas A. Henzinger
11. Inferring Canonical Register Automata · Falk Howar, Bernhard Steffen, Bengt Jonsson, Sofia Cassel
12. Lazy Synthesis · Bernd Finkbeiner, Swen Jacobs
13. Local Symmetry and Compositional Verification · Kedar S. Namjoshi, Richard J. Trefler
14. Loop Invariant Symbolic Execution for Parallel Programs · Stephen F. Siegel, Timothy K. Zirkel
15. Model Checking Information Flow in Reactive Systems · Rayna Dimitrova, Bernd Finkbeiner, Máté Kovács, Markus N. Rabe, Helmut Seidl
16. Modeling Asynchronous Message Passing for C Programs · Everett Morse, Nick Vrvilo, Eric Mercer, Jay McCarthy
17. On Application of Multi-Rooted Binary Decision Diagrams to Probabilistic Model Checking · Dmitry Bugaychenko
18. On the Termination of Integer Loops · Amir M. Ben-Amram, Samir Genaim, Abu Naser Masud
19. Regression Verification for Multi-threaded Programs · Sagar Chaki, Arie Gurfinkel, Ofer Strichman
20. Software Verification with Liquid Types · Ranjit Jhala
21. Sound Non-statistical Clustering of Static Analysis Alarms · Woosuk Lee, Wonchan Lee, Kwangkeun Yi
22. Splitting via Interpolants · Evren Ermis, Jochen Hoenicke, Andreas Podelski
23. Synchronizability for Verification of Asynchronously Communicating Systems · Samik Basu, Tevfik Bultan, Meriem Ouederni
24. Synthesizing Efficient Controllers · Christian von Essen, Barbara Jobstmann
25. Synthesizing Protocols for Digital Contract Signing · Krishnendu Chatterjee, Vishwanath Raman
26. Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs · Tobias Nipkow
27. Verification of Gap-Order Constraint Abstractions of Counter Systems · Laura Bozzelli, Sophie Pinchinat
28. Whale: An Interpolation-Based Algorithm for Inter-procedural Verification · Aws Albarghouthi, Arie Gurfinkel, Marsha Chechik
29. versat: A Verified Modern SAT Solver · Duckki Oe, Aaron Stump, Corey Oliver, Kevin Clancy