| 2008 | A Hybrid Type System for Lock-Freedom of Mobile Processes. Naoki Kobayashi, Davide Sangiorgi |
| 2008 | A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis. Bhargav S. Gulavani, Sumit Gulwani |
| 2008 | A Practical Approach to Word Level Model Checking of Industrial Netlists. Per Bjesse |
| 2008 | Abstract Interpretation with Applications to Timing Validation. Reinhard Wilhelm, Björn Wachter |
| 2008 | An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths. Oliver Wienand, Markus Wedler, Dominik Stoffel, Wolfgang Kunz, Gert-Martin Greuel |
| 2008 | Application of Formal Word-Level Analysis to Constrained Random Simulation. Hyondeuk Kim, HoonSang Jin, Kavita Ravi, Petr Spacek, John Pierce, Robert P. Kurshan, Fabio Somenzi |
| 2008 | Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems. Salil Joshi, Barbara König |
| 2008 | Assertion-Based Verification: Industry Myths to Realities (Invited Tutorial). Harry Foster |
| 2008 | AutoMOTGen: Automatic Model Oriented Test Generator for Embedded Control Systems. Ambar A. Gadkari, Anand Yeolekar, J. Suresh, S. Ramesh, Swarup Mohalik, K. C. Shashidhar |
| 2008 | Automated Assume-Guarantee Reasoning by Abstraction Refinement. Mihaela Gheorghiu Bobaru, Corina S. Pasareanu, Dimitra Giannakopoulou |
| 2008 | CSIsat: Interpolation for LA+EUF. Dirk Beyer, Damien Zufferey, Rupak Majumdar |
| 2008 | Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings Aarti Gupta, Sharad Malik |
| 2008 | Computing Differential Invariants of Hybrid Systems as Fixedpoints. André Platzer, Edmund M. Clarke |
| 2008 | Conflict-Tolerant Features. Deepak D'Souza, Madhu Gopinathan |
| 2008 | Constraint-Based Approach for Analysis of Hybrid Systems. Sumit Gulwani, Ashish Tiwari |
| 2008 | Coping with Outside-the-Box Attacks. Edward W. Felten |
| 2008 | Correcting a Space-Efficient Simulation Algorithm. Rob J. van Glabbeek, Bas Ploeger |
| 2008 | Discriminative Model Checking. Peter Niebert, Doron A. Peled, Amir Pnueli |
| 2008 | Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings. Sarvani S. Vakkalanka, Ganesh Gopalakrishnan, Robert M. Kirby |
| 2008 | Effective Program Verification for Relaxed Memory Models. Sebastian Burckhardt, Madanlal Musuvathi |
| 2008 | Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations. Himanshu Jain, Edmund M. Clarke, Orna Grumberg |
| 2008 | Enhancing Program Verification with Lemmas. Huu Hai Nguyen, Wei-Ngan Chin |
| 2008 | FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement. Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith |
| 2008 | Faster Than Uppaal? Sebastian Kupferschmid, Martin Wehrle, Bernhard Nebel, Andreas Podelski |
| 2008 | Functional Verification of Power Gated Designs by Compositional Reasoning. Cindy Eisner, Amir Nahir, Karen Yorav |
| 2008 | Heap Assumptions on Demand. Andreas Podelski, Andrey Rybalchenko, Thomas Wies |
| 2008 | Implied Set Closure and Its Application to Memory Consistency Verification. Surender Baswana, Shashank K. Mehta, Vishal Powar |
| 2008 | Inferring Congruence Equations Using SAT. Andy King, Harald Søndergaard |
| 2008 | Jakstab: A Static Analysis Platform for Binaries. Johannes Kinder, Helmut Veith |
| 2008 | Linear Arithmetic with Stars. Ruzica Piskac, Viktor Kuncak |
| 2008 | Local Proofs for Linear-Time Properties of Concurrent Programs. Ariel Cohen, Kedar S. Namjoshi |
| 2008 | Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses. Ariel Cohen, Amir Pnueli, Lenore D. Zuck |
| 2008 | Monitoring Atomicity in Concurrent Programs. Azadeh Farzan, P. Madhusudan |
| 2008 | Monotonic Abstraction for Programs with Dynamic Memory Heaps. Parosh Aziz Abdulla, Ahmed Bouajjani, Jonathan Cederberg, Frédéric Haziza, Ahmed Rezine |
| 2008 | Probabilistic CEGAR. Holger Hermanns, Björn Wachter, Lijun Zhang |
| 2008 | Producing Short Counterexamples Using "Crucial Events". Sujatha Kashyap, Vijay K. Garg |
| 2008 | Prover's Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD-B. Laura I. Meikle, Jacques D. Fleuriot |
| 2008 | Proving Conditional Termination. Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, Mooly Sagiv |
| 2008 | QMC: A Model Checker for Quantum Systems. Simon J. Gay, Rajagopal Nagarajan, Nikolaos Papanikolaou |
| 2008 | Ranking Automata and Games for Prioritized Requirements. Rajeev Alur, Aditya Kanade, Gera Weiss |
| 2008 | Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis. Akash Lal, Thomas W. Reps |
| 2008 | Scalable Shape Analysis for Systems Code. Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn |
| 2008 | Semi-external LTL Model Checking. Stefan Edelkamp, Peter Sanders, Pavel Simecek |
| 2008 | Singularity: Designing Better Software (Invited Talk). James R. Larus |
| 2008 | T(O)RMC: A Tool for (omega)-Regular Model Checking. Axel Legay |
| 2008 | THOR: A Tool for Reasoning about Shape and Arithmetic. Stephen Magill, Ming-Hsien Tsai, Peter Lee, Yih-Kuen Tsay |
| 2008 | The Barcelogic SMT Solver. Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio |
| 2008 | The CASPA Tool: Causality-Based Abstraction for Security Protocol Analysis. Michael Backes, Stefan Lorenz, Matteo Maffei, Kim Pecina |
| 2008 | The MathSAT 4SMT Solver. Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani |
| 2008 | The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols. Cas J. F. Cremers |
| 2008 | Theorem Proving for Verification (Invited Tutorial). John Harrison |
| 2008 | Thread Quantification for Concurrent Shape Analysis. Josh Berdine, Tal Lev-Ami, Roman Manevich, G. Ramalingam, Shmuel Sagiv |
| 2008 | Tutorial on Separation Logic (Invited Tutorial). Peter W. O'Hearn |
| 2008 | Validating High-Level Synthesis. Sudipta Kundu, Sorin Lerner, Rajesh Gupta |