| 2008 | A Refinement Approach to Design and Verification of On-Chip Communication Protocols. Peter Böhm, Tom Melham |
| 2008 | A Temporal Language for SystemC. Deian Tabakov, Gila Kamhi, Moshe Y. Vardi, Eli Singerman |
| 2008 | A Theory of Mutations with Applications to Vacuity, Coverage, and Fault Tolerance. Orna Kupferman, Wenchao Li, Sanjit A. Seshia |
| 2008 | A Theory-Based Decision Heuristic for DPLL(T). Dan Goldwasser, Ofer Strichman, Shai Fine |
| 2008 | A Write-Based Solver for SAT Modulo the Theory of Arrays. Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio |
| 2008 | Augmenting a Regular Expression-Based Temporal Logic with Local Variables. Cindy Eisner, Dana Fisman |
| 2008 | Automatic Formal Verification of Block Cipher Implementations. Eric Whitman Smith, David L. Dill |
| 2008 | Automatic Generation of Local Repairs for Boolean Programs. Roopsha Samanta, Jyotirmoy V. Deshmukh, E. Allen Emerson |
| 2008 | Automatic Non-Interference Lemmas for Parameterized Model Checking. Jesse D. Bingham |
| 2008 | BACH : Bounded ReAchability CHecker for Linear Hybrid Automata. Lei Bu, You Li, Linzhang Wang, Xuandong Li |
| 2008 | BackSpace: Formal Analysis for Post-Silicon Debug. Flavio M. de Paula, Marcel Gort, Alan J. Hu, Steven J. E. Wilton, Jin Yang |
| 2008 | Beyond Vacuity: Towards the Strongest Passing Formula. Hana Chockler, Arie Gurfinkel, Ofer Strichman |
| 2008 | Combining Predicate and Numeric Abstraction for Software Model Checking. Arie Gurfinkel, Sagar Chaki |
| 2008 | Consistency Checking of All Different Constraints over Bit-Vectors within a SAT Solver. Armin Biere, Robert Brummayer |
| 2008 | Formal Methods in Computer-Aided Design, FMCAD 2008, Portland, Oregon, USA, 17-20 November 2008 Alessandro Cimatti, Robert B. Jones |
| 2008 | Formal Verification of Hardware Support for Advanced Encryption Standard. Anna Slobodová |
| 2008 | Going with the Flow: Parameterized Verification Using Message Flows. Murali Talupur, Mark R. Tuttle |
| 2008 | Invariant-Strengthened Elimination of Dependent State Elements. Michael L. Case, Alan Mishchenko, Robert K. Brayton, Jason Baumgartner, Hari Mony |
| 2008 | Invited Tutorial: Considerations in the Design and Verification of Microprocessors for Safety-Critical and Security-Critical Applications. David S. Hardin |
| 2008 | Machine-Code Verification for Multiple Architectures - An Application of Decompilation into Logic. Magnus O. Myreen, Michael J. C. Gordon, Konrad Slind |
| 2008 | Mechanized Information Flow Analysis through Inductive Assertions. Warren A. Hunt Jr., Robert Bellarmine Krug, Sandip Ray, William D. Young |
| 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 | Optimal Constraint-Preserving Netlist Simplification. Jason Baumgartner, Hari Mony, Adnan Aziz |
| 2008 | Recording Synthesis History for Sequential Verification. Alan Mishchenko, Robert K. Brayton |
| 2008 | Scaling Up the Formal Verification of Lustre Programs with SMT-Based Techniques. George Hagen, Cesare Tinelli |
| 2008 | Scheduling Optimisations for SPIN to Minimise Buffer Requirements in Synchronous Data Flow. Pieter H. Hartel, Theo C. Ruys, Marc C. W. Geilen |
| 2008 | Symbolic Program Analysis Using Term Rewriting and Generalization. Nishant Sinha |
| 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 |
| 2008 | Verifying an Arbiter Circuit. Chao Yan, Mark R. Greenstreet |
| 2008 | Word-Level Sequential Memory Abstraction for Model Checking. Per Bjesse |