| 2009 | A Concurrent Portfolio Approach to SMT Solving. Christoph M. Wintersteiger, Youssef Hamadi, Leonardo Mendonça de Moura |
| 2009 | A Markov Chain Monte Carlo Sampler for Mixed Boolean/Integer Constraints. Nathan Kitchen, Andreas Kuehlmann |
| 2009 | An Antichain Algorithm for LTL Realizability. Emmanuel Filiot, Naiyong Jin, Jean-François Raskin |
| 2009 | Apron: A Library of Numerical Abstract Domains for Static Analysis. Bertrand Jeannet, Antoine Miné |
| 2009 | Automated Analysis of Java Methods for Confidentiality. Pavol Cerný, Rajeev Alur |
| 2009 | Automatic Verification of Integer Array Programs. Marius Bozga, Peter Habermehl, Radu Iosif, Filip Konecný, Tomás Vojnar |
| 2009 | Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic. Susmit Jha, Rhishikesh Limaye, Sanjit A. Seshia |
| 2009 | Better Quality in Synthesis through Quantitative Objectives. Roderick Bloem, Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann |
| 2009 | Browser-Based Enforcement of Interface Contracts in Web Applications with BeepBeep. Sylvain Hallé, Roger Villemaire |
| 2009 | CalFuzzer: An Extensible Active Testing Framework for Concurrent Programs. Pallavi Joshi, Mayur Naik, Chang-Seo Park, Koushik Sen |
| 2009 | Cardinality Abstraction for Declarative Networking Applications. Juan Antonio Navarro Pérez, Andrey Rybalchenko, Atul Singh |
| 2009 | Centaur Technology Media Unit Verification. Warren A. Hunt Jr., Sol Swords |
| 2009 | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories. Yeting Ge, Leonardo Mendonça de Moura |
| 2009 | Component-Based Construction of Real-Time Systems in BIP. Joseph Sifakis |
| 2009 | Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings Ahmed Bouajjani, Oded Maler |
| 2009 | Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers. Isil Dillig, Thomas Dillig, Alex Aiken |
| 2009 | D-Finder: A Tool for Compositional Deadlock Detection and Verification. Saddek Bensalem, Marius Bozga, Thanh-Hung Nguyen, Joseph Sifakis |
| 2009 | Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences. Sven Verdoolaege, Gerda Janssens, Maurice Bruynooghe |
| 2009 | Explaining Counterexamples Using Causality. Ilan Beer, Shoham Ben-David, Hana Chockler, Avigail Orni, Richard J. Trefler |
| 2009 | Games through Nested Fixpoints. Thomas Gawlitza, Helmut Seidl |
| 2009 | Generalizing DPLL to Richer Logics. Kenneth L. McMillan, Andreas Kuehlmann, Mooly Sagiv |
| 2009 | Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models. Aditya Kanade, Rajeev Alur, Franjo Ivancic, S. Ramesh, Sriram Sankaranarayanan, K. C. Shashidhar |
| 2009 | Homer: A Higher-Order Observational Equivalence Model checkER. David Hopkins, C.-H. Luke Ong |
| 2009 | HybridFluctuat: A Static Analyzer of Numerical Programs within a Continuous Environment. Olivier Bouissou, Eric Goubault, Sylvie Putot, Karim Tekkal, Franck Védrine |
| 2009 | INFAMY: An Infinite-State Markov Model Checker. Ernst Moritz Hahn, Holger Hermanns, Björn Wachter, Lijun Zhang |
| 2009 | Image Computation for Polynomial Dynamical Systems Using the Bernstein Expansion. Thao Dang, David Salinas |
| 2009 | Incremental Instance Generation in Local Reasoning. Swen Jacobs |
| 2009 | Intra-module Inference. Shuvendu K. Lahiri, Shaz Qadeer, Juan P. Galeotti, Jan W. Voung, Thomas Wies |
| 2009 | InvGen: An Efficient Invariant Generator. Ashutosh Gupta, Andrey Rybalchenko |
| 2009 | Linear Functional Fixed-points. Nikolaj S. Bjørner, Joe Hendrix |
| 2009 | MCMAS: A Model Checker for the Verification of Multi-Agent Systems. Alessio Lomuscio, Hongyang Qu, Franco Raimondi |
| 2009 | Meta-analysis for Atomicity Violations under Nested Locking. Azadeh Farzan, P. Madhusudan, Francesco Sorrentino |
| 2009 | Mixed-Signal System Verification: A High-Speed Link Example. Jaeha Kim |
| 2009 | Modelling Epigenetic Information Maintenance: A Kappa Tutorial. Jean Krivine, Vincent Danos, Arndt Benecke |
| 2009 | Models and Proofs of Protocol Security: A Progress Report. Martín Abadi, Bruno Blanchet, Hubert Comon-Lundh |
| 2009 | Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique. Vineet Kahlon, Chao Wang, Aarti Gupta |
| 2009 | On Extending Bounded Proofs to Inductive Proofs. Oded Fuhrmann, Shlomo Hoory |
| 2009 | On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure. David Monniaux |
| 2009 | PAT: Towards Flexible Verification under Fairness. Jun Sun, Yang Liu, Jin Song Dong, Jun Pang |
| 2009 | Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints. Peter Lammich, Markus Müller-Olm, Alexander Wenner |
| 2009 | Predictability vs. Efficiency in the Multicore Era: Fight of Titans or Happy Ever after?. Luca Benini |
| 2009 | Priority Scheduling of Distributed Systems Based on Model Checking. Ananda Basu, Saddek Bensalem, Doron A. Peled, Joseph Sifakis |
| 2009 | Quantifier Elimination via Functional Composition. Jie-Hong R. Jiang |
| 2009 | Reachability Analysis of Hybrid Systems Using Support Functions. Colas Le Guernic, Antoine Girard |
| 2009 | Reducing Context-Bounded Concurrent Reachability to Sequential Reachability. Salvatore La Torre, P. Madhusudan, Gennaro Parlato |
| 2009 | Reducing Test Inputs Using Information Partitions. Rupak Majumdar, Ru-Gang Xu |
| 2009 | Regression Verification: Proving the Equivalence of Similar Programs. Ofer Strichman |
| 2009 | Replacing Testing with Formal Verification in Intel CoreTM i7 Processor Execution Engine Validation. Roope Kaivola, Rajnish Ghughal, Naren Narasimhan, Amber Telfer, Jesse Whittemore, Sudhindra Pandav, Anna Slobodová, Christopher Taylor, Vladimir A. Frolov, Erik Reeber, Armaghan Naik |
| 2009 | Requirements Validation for Hybrid Systems. Alessandro Cimatti, Marco Roveri, Stefano Tonetta |
| 2009 | SPEED: Symbolic Complexity Bound Analysis. Sumit Gulwani |
| 2009 | Size-Change Termination, Monotonicity Constraints and Ranking Functions. Amir M. Ben-Amram |
| 2009 | Sliding Window Abstraction for Infinite Markov Chains. Thomas A. Henzinger, Maria Mateescu, Verena Wolf |
| 2009 | Software Transactional Memory on Relaxed Memory Models. Rachid Guerraoui, Thomas A. Henzinger, Vasu Singh |
| 2009 | Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers. Shuvendu K. Lahiri, Shaz Qadeer, Zvonimir Rakamaric |
| 2009 | Symbolic Counter Abstraction for Concurrent Software. Gérard Basler, Michele Mazzucchi, Thomas Wahl, Daniel Kroening |
| 2009 | TASS: Timing Analyzer of Scenario-Based Specifications. Minxue Pan, Lei Bu, Xuandong Li |
| 2009 | The Zonotope Abstract Domain Taylor1+. Khalil Ghorbal, Eric Goubault, Sylvie Putot |
| 2009 | Towards Performance Prediction of Compositional Models in Industrial GALS Designs. Nicolas Coste, Holger Hermanns, Etienne Lantreibecq, Wendelin Serwe |
| 2009 | Transactional Memory: Glimmer of a Theory. Rachid Guerraoui, Michal Kapalka |
| 2009 | Translation Validation: From Simulink to C. Michael Ryabtsev, Ofer Strichman |
| 2009 | VS3: SMT Solvers for Program Verification. Saurabh Srivastava, Sumit Gulwani, Jeffrey S. Foster |