| 2010 | Complexity Bounds for the Verification of Real-Time Software. | Rohit Chadha, Axel Legay, Pavithra Prabhakar, Mahesh Viswanathan |
| 2010 | Path-Oriented Reachability Verification of a Class of Nonlinear Hybrid Automata Using Convex Programming. | Lei Bu, Jianhua Zhao, Xuandong Li |
| 2010 | Improved Model Checking of Hierarchical Systems. | Benjamin Aminof, Orna Kupferman, Aniello Murano |
| 2010 | Temporal Reasoning for Procedural Programs. | Rajeev Alur, Swarat Chaudhuri |
| 2009 | Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking. | Ralf Wimmer, Bettina Braitling, Bernd Becker |
| 2009 | Mixed Transition Systems Revisited. | Ou Wei, Arie Gurfinkel, Marsha Chechik |
| 2009 | Shape-Value Abstraction for Verifying Linearizability. | Viktor Vafeiadis |
| 2009 | Extending Symmetry Reduction by Exploiting System Architecture. | Richard J. Trefler, Thomas Wahl |
| 2009 | Synthesizing Switching Logic Using Constraint Solving. | Ankur Taly, Sumit Gulwani, Ashish Tiwari |
| 2009 | Thread-Modular Shape Analysis. | Mooly Sagiv |
| 2009 | A Scalable Memory Model for Low-Level Code. | Zvonimir Rakamaric, Alan J. Hu |
| 2009 | An Automata-Theoretic Dynamic Completeness Criterion for Bounded Model-Checking. | Rotem Oshman |
| 2009 | A PosterioriSoundness for Non-deterministic Abstract Interpretations. | Matthew Might, Panagiotis Manolios |
| 2009 | Deciding Extensions of the Theories of Vectors and Bags. | Patrick Maier |
| 2009 | SubPolyhedra: A (More) Scalable Approach to Infer Linear Inequalities. | Vincent Laviron, Francesco Logozzo |
| 2009 | An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries. | Johannes Kinder, Florian Zuleger, Helmut Veith |
| 2009 | Finding Concurrency-Related Bugs Using Random Isolation. | Nicholas Kidd, Thomas W. Reps, Julian Dolby, Mandana Vaziri |
| 2009 | Abstraction Refinement for Probabilistic Software. | Mark Kattenbelt, Marta Z. Kwiatkowska, Gethin Norman, David Parker |
| 2009 | Average-Price-per-Reward Games on Hybrid Automata with Strong Resets. | Marcin Jurdzinski, Ranko Lazic, Michal Rutkowski |
| 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 | Model Checking Concurrent Programs. | Aarti Gupta |
| 2009 | Constraint-Based Invariant Inference over Predicate Abstraction. | Sumit Gulwani, Saurabh Srivastava, Ramarathnam Venkatesan |
| 2009 | Monitoring the Full Range of omega-Regular Properties of Stochastic Systems. | Kalpana Gondi, Yogeshkumar Patel, A. Prasad Sistla |
| 2009 | LTL Generalized Model Checking Revisited. | Patrice Godefroid, Nir Piterman |