| 2009 | Software model checking via large-block encoding. | Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, Roberto Sebastiani |
| 2009 | Scalable conditional equivalence checking: An automated invariant-generation based approach. | Jason Baumgartner, Hari Mony, Michael L. Case, Jun Sawada, Karen Yorav |
| 2009 | SAT-based synthesis of clock gating functions using 3-valued abstraction. | Eli Arbel, Oleg Rokhlenko, Karen Yorav |
| 2008 | Verifying an Arbiter Circuit. | Chao Yan, Mark R. Greenstreet |
| 2008 | Going with the Flow: Parameterized Verification Using Message Flows. | Murali Talupur, Mark R. Tuttle |
| 2008 | A Temporal Language for SystemC. | Deian Tabakov, Gila Kamhi, Moshe Y. Vardi, Eli Singerman |
| 2008 | Automatic Formal Verification of Block Cipher Implementations. | Eric Whitman Smith, David L. Dill |
| 2008 | Formal Verification of Hardware Support for Advanced Encryption Standard. | Anna Slobodov |
| 2008 | Symbolic Program Analysis Using Term Rewriting and Generalization. | Nishant Sinha |
| 2008 | Automatic Generation of Local Repairs for Boolean Programs. | Roopsha Samanta, Jyotirmoy V. Deshmukh, E. Allen Emerson |
| 2008 | BackSpace: Formal Analysis for Post-Silicon Debug. | Flavio M. de Paula, Marcel Gort, Alan J. Hu, Steven J. E. Wilton, Jin Yang |
| 2008 | Machine-Code Verification for Multiple Architectures - An Application of Decompilation into Logic. | Magnus O. Myreen, Michael J. C. Gordon, Konrad Slind |
| 2008 | Recording Synthesis History for Sequential Verification. | Alan Mishchenko, Robert K. Brayton |
| 2008 | Model Checking Nash Equilibria in MAD Distributed Systems. | Federico Mari, Igor Melatti, Ivano Salvo, Enrico Tronci, Lorenzo Alvisi, Allen Clement, Harry C. Li |
| 2008 | A Theory of Mutations with Applications to Vacuity, Coverage, and Fault Tolerance. | Orna Kupferman, Wenchao Li, Sanjit A. Seshia |
| 2008 | Mechanized Information Flow Analysis through Inductive Assertions. | Warren A. Hunt Jr., Robert Bellarmine Krug, Sandip Ray, William D. Young |
| 2008 | Scheduling Optimisations for SPIN to Minimise Buffer Requirements in Synchronous Data Flow. | Pieter H. Hartel, Theo C. Ruys, Marc C. W. Geilen |
| 2008 | Invited Tutorial: Considerations in the Design and Verification of Microprocessors for Safety-Critical and Security-Critical Applications. | David S. Hardin |
| 2008 | Scaling Up the Formal Verification of Lustre Programs with SMT-Based Techniques. | George Hagen, Cesare Tinelli |
| 2008 | Combining Predicate and Numeric Abstraction for Software Model Checking. | Arie Gurfinkel, Sagar Chaki |
| 2008 | A Theory-Based Decision Heuristic for DPLL(T). | Dan Goldwasser, Ofer Strichman, Shai Fine |
| 2008 | Augmenting a Regular Expression-Based Temporal Logic with Local Variables. | Cindy Eisner, Dana Fisman |
| 2008 | Beyond Vacuity: Towards the Strongest Passing Formula. | Hana Chockler, Arie Gurfinkel, Ofer Strichman |
| 2008 | Invariant-Strengthened Elimination of Dependent State Elements. | Michael L. Case, Alan Mishchenko, Robert K. Brayton, Jason Baumgartner, Hari Mony |
| 2008 | Trading-Off SAT Search and Variable Quantifications for Effective Unbounded Model Checking. | Gianpiero Cabodi, Paolo Camurati, Luz Amanda Garcia, Marco Murciano, Sergio Nocco, Stefano Quer |