| 2004 | QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings. | Ganesh Gopalakrishnan, Yue Yang, Hemanthkumar Sivaraj |
| 2004 | Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional Vectors. | Amit Goel, Randal E. Bryant |
| 2004 | A Formal Reduction for Lock-Free Parallel Algorithms. | Hui Gao, Wim H. Hesselink |
| 2004 | DPLL( T): Fast Decision Procedures. | Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli |
| 2004 | Efficient Modeling of Embedded Memories in Bounded Model Checking. | Malay K. Ganai, Aarti Gupta, Pranav Ashar |
| 2004 | MCK: Model Checking the Logic of Knowledge. | Peter Gammie, Ron van der Meyden |
| 2004 | WSAT: A Tool for Formal Analysis of Web Services. | Xiang Fu, Tevfik Bultan, Jianwen Su |
| 2004 | Stuck-Free Conformance. | Cdric Fournet, C. A. R. Hoare, Sriram K. Rajamani, Jakob Rehof |
| 2004 | Image Computation in Infinite State Model Checking. | Alain Finkel, Jrme Leroux |
| 2004 | Formal Analysis of Java Programs in JavaFAN. | Azadeh Farzan, Feng Chen, Jos Meseguer, Grigore Rosu |
| 2004 | Using Interface Refinement to Integrate Formal Verification into the Design Cycle. | Jacob Chang, Sergey Berezin, David L. Dill |
| 2004 | Verifying omega-Regular Properties of Markov Chains. | Doron Bustan, Sasha Rubin, Moshe Y. Vardi |
| 2004 | ObsSlice: A Timed Automata Slicer Based on Observers. | Vctor A. Braberman, Diego Garbervetsky, Alfredo Olivero |
| 2004 | Abstract Regular Model Checking. | Ahmed Bouajjani, Peter Habermehl, Toms Vojnar |
| 2004 | Automatic Verification of Sequential Consistency for Unbounded Addresses and Data Values. | Jesse D. Bingham, Anne Condon, Alan J. Hu, Shaz Qadeer, Zhichuan Zhang |
| 2004 | Widening Arithmetic Automata. | Constantinos Bartzis, Tevfik Bultan |
| 2004 | CVC Lite: A New Implementation of the Cooperating Validity Checker Category B. | Clark W. Barrett, Sergey Berezin |
| 2004 | Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement. | Thomas Ball, Byron Cook, Shuvendu K. Lahiri, Lintao Zhang |
| 2004 | Proving More Properties with Bounded Model Checking. | Mohammad Awedh, Fabio Somenzi |
| 2004 | JNuke: Efficient Dynamic Analysis for Java. | Cyrille Artho, Viktor Schuppan, Armin Biere, Pascal Eugster, Marcel Baur, Boris Zweimller |
| 2004 | Verification of an Advanced mips-Type Out-of-Order Execution Algorithm. | Tamarah Arons |
| 2004 | Zing: A Model Checker for Concurrent Software. | Tony Andrews, Shaz Qadeer, Sriram K. Rajamani, Jakob Rehof, Yichen Xie |
| 2004 | Regular Model Checking for LTL(MSO). | Parosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson, Julien d'Orso, Mayank Saksena |
| 2003 | Dense Counter Machines and Verification Problems. | Gaoyan Xie, Zhe Dang, Oscar H. Ibarra, Pierluigi San Pietro |
| 2003 | A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement. | Sharon Shoham, Orna Grumberg |