| 2009 | A PosterioriSoundness for Non-deterministic Abstract Interpretations. Matthew Might, Panagiotis Manolios |
| 2009 | A Scalable Memory Model for Low-Level Code. Zvonimir Rakamaric, Alan J. Hu |
| 2009 | Abstraction Refinement for Probabilistic Software. Mark Kattenbelt, Marta Z. Kwiatkowska, Gethin Norman, David Parker |
| 2009 | Advances in Program Termination and Liveness. Byron Cook |
| 2009 | An Abort-Aware Model of Transactional Programming. Kousha Etessami, Patrice Godefroid |
| 2009 | An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries. Johannes Kinder, Florian Zuleger, Helmut Veith |
| 2009 | An Automata-Theoretic Dynamic Completeness Criterion for Bounded Model-Checking. Rotem Oshman |
| 2009 | Average-Price-per-Reward Games on Hybrid Automata with Strong Resets. Marcin Jurdzinski, Ranko Lazic, Michal Rutkowski |
| 2009 | Constraint-Based Invariant Inference over Predicate Abstraction. Sumit Gulwani, Saurabh Srivastava, Ramarathnam Venkatesan |
| 2009 | Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking. Ralf Wimmer, Bettina Braitling, Bernd Becker |
| 2009 | Deciding Extensions of the Theories of Vectors and Bags. Patrick Maier |
| 2009 | Extending Symmetry Reduction by Exploiting System Architecture. Richard J. Trefler, Thomas Wahl |
| 2009 | Finding Concurrency-Related Bugs Using Random Isolation. Nicholas Kidd, Thomas W. Reps, Julian Dolby, Mandana Vaziri |
| 2009 | LTL Generalized Model Checking Revisited. Patrice Godefroid, Nir Piterman |
| 2009 | Mixed Transition Systems Revisited. Ou Wei, Arie Gurfinkel, Marsha Chechik |
| 2009 | Model Checking Concurrent Programs. Aarti Gupta |
| 2009 | Model Checking: Progress and Problems. E. Allen Emerson |
| 2009 | Model-Checking the Linux Virtual File System. Andy Galloway, Gerald Lüttgen, Jan Tobias Mühlberg, Radu Siminiceanu |
| 2009 | Monitoring the Full Range of omega-Regular Properties of Stochastic Systems. Kalpana Gondi, Yogeshkumar Patel, A. Prasad Sistla |
| 2009 | Mostly-Functional Behavior in Java Programs. William C. Benton, Charles N. Fischer |
| 2009 | Query-Driven Program Testing. Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith |
| 2009 | Reducing Behavioural to Structural Properties of Programs with Procedures. Dilian Gurov, Marieke Huisman |
| 2009 | Shape-Value Abstraction for Verifying Linearizability. Viktor Vafeiadis |
| 2009 | SubPolyhedra: A (More) Scalable Approach to Infer Linear Inequalities. Vincent Laviron, Francesco Logozzo |
| 2009 | Synthesizing Switching Logic Using Constraint Solving. Ankur Taly, Sumit Gulwani, Ashish Tiwari |
| 2009 | The Higher-Order Aggregate Update Problem. Christos Dimoulas, Mitchell Wand |
| 2009 | Thread-Modular Shape Analysis. Mooly Sagiv |
| 2009 | Towards Automatic Stability Analysis for Rely-Guarantee Proofs. Hasan Amjad, Richard Bornat |
| 2009 | Verification of Security Protocols. Véronique Cortier |
| 2009 | Verification, Model Checking, and Abstract Interpretation, 10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009. Proceedings Neil D. Jones, Markus Müller-Olm |