| 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 | Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique. | Vineet Kahlon, Chao Wang, Aarti Gupta |
| 2009 | CalFuzzer: An Extensible Active Testing Framework for Concurrent Programs. | Pallavi Joshi, Mayur Naik, Chang-Seo Park, Koushik Sen |
| 2009 | Quantifier Elimination via Functional Composition. | Jie-Hong R. Jiang |
| 2009 | Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic. | Susmit Jha, Rhishikesh Limaye, Sanjit A. Seshia |
| 2009 | Apron: A Library of Numerical Abstract Domains for Static Analysis. | Bertrand Jeannet, Antoine Min |
| 2009 | Incremental Instance Generation in Local Reasoning. | Swen Jacobs |
| 2009 | Centaur Technology Media Unit Verification. | Warren A. Hunt Jr., Sol Swords |
| 2009 | Homer: A Higher-Order Observational Equivalence Model checkER. | David Hopkins, C.-H. Luke Ong |
| 2009 | Sliding Window Abstraction for Infinite Markov Chains. | Thomas A. Henzinger, Maria Mateescu, Verena Wolf |
| 2009 | Browser-Based Enforcement of Interface Contracts in Web Applications with BeepBeep. | Sylvain Hall, Roger Villemaire |
| 2009 | INFAMY: An Infinite-State Markov Model Checker. | Ernst Moritz Hahn, Holger Hermanns, Bjrn Wachter, Lijun Zhang |
| 2009 | InvGen: An Efficient Invariant Generator. | Ashutosh Gupta, Andrey Rybalchenko |
| 2009 | SPEED: Symbolic Complexity Bound Analysis. | Sumit Gulwani |
| 2009 | Transactional Memory: Glimmer of a Theory. | Rachid Guerraoui, Michal Kapalka |
| 2009 | Software Transactional Memory on Relaxed Memory Models. | Rachid Guerraoui, Thomas A. Henzinger, Vasu Singh |
| 2009 | Reachability Analysis of Hybrid Systems Using Support Functions. | Colas Le Guernic, Antoine Girard |
| 2009 | The Zonotope Abstract Domain Taylor1+. | Khalil Ghorbal, Eric Goubault, Sylvie Putot |
| 2009 | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories. | Yeting Ge, Leonardo Mendona de Moura |
| 2009 | Games through Nested Fixpoints. | Thomas Gawlitza, Helmut Seidl |
| 2009 | On Extending Bounded Proofs to Inductive Proofs. | Oded Fuhrmann, Shlomo Hoory |
| 2009 | An Antichain Algorithm for LTL Realizability. | Emmanuel Filiot, Naiyong Jin, Jean-Franois Raskin |
| 2009 | Meta-analysis for Atomicity Violations under Nested Locking. | Azadeh Farzan, P. Madhusudan, Francesco Sorrentino |
| 2009 | Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers. | Isil Dillig, Thomas Dillig, Alex Aiken |
| 2009 | Image Computation for Polynomial Dynamical Systems Using the Bernstein Expansion. | Thao Dang, David Salinas |