| 2006 | Verifying Concurrent Message-Passing C Programs with Recursive Calls. | Sagar Chaki, Edmund M. Clarke, Nicholas Kidd, Thomas W. Reps, Tayssir Touili |
| 2006 | SAT-Based Software Certification. | Sagar Chaki |
| 2006 | Easy Parameterized Verification of Biphase Mark and 8N1 Protocols. | Geoffrey M. Brown, Lee Pike |
| 2006 | MSCan - A Tool for Analyzing MSC Specifications. | Benedikt Bollig, Carsten Kern, Markus Schltter, Volker Stolz |
| 2005 | Symstra: A Framework for Generating Object-Oriented Unit Tests Using Symbolic Execution. | Tao Xie, Darko Marinov, Wolfram Schulte, David Notkin |
| 2005 | Mining Temporal Specifications for Error Detection. | Westley Weimer, George C. Necula |
| 2005 | Using Language Inference to Verify Omega-Regular Properties. | Abhay Vardhan, Koushik Sen, Mahesh Viswanathan, Gul Agha |
| 2005 | jMoped: A Java Bytecode Checker Based on Moped. | Dejvuth Suwimonteerabuth, Stefan Schwoon, Javier Esparza |
| 2005 | Bounded Validity Checking of Interval Duration Logic. | Babita Sharma, Paritosh K. Pandya, Supratik Chakraborty |
| 2005 | A Note on On-the-Fly Verification Algorithms. | Stefan Schwoon, Javier Esparza |
| 2005 | Shortest Counterexamples for Symbolic Model Checking of LTL with Past. | Viktor Schuppan, Armin Biere |
| 2005 | Model Checking Infinite-State Markov Chains. | Anne Remke, Boudewijn R. Haverkort, Lucia Cloth |
| 2005 | An Abstract Interpretation-Based Refinement Algorithm for Strong Preservation. | Francesco Ranzato, Francesco Tapparo |
| 2005 | Context-Bounded Model Checking of Concurrent Software. | Shaz Qadeer, Jakob Rehof |
| 2005 | Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems. | Amir Pnueli, Andreas Podelski, Andrey Rybalchenko |
| 2005 | Applications of Craig Interpolants in Model Checking. | Kenneth L. McMillan |
| 2005 | Using BDDs to Decide CTL. | Will Marrero |
| 2005 | jETI: A Tool for Remote Tool Integration. | Tiziana Margaria, Ralf Nagel, Bernhard Steffen |
| 2005 | A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover. | K. Rustan M. Leino, Madan Musuvathi, Xinming Ou |
| 2005 | Complementation Constructions for Nondeterministic Automata on Infinite Words. | Orna Kupferman, Moshe Y. Vardi |
| 2005 | Temporal Logic for Scenario-Based Specifications. | Hillel Kugler, David Harel, Amir Pnueli, Yuan Lu, Yves Bontemps |
| 2005 | Dependent Types for Program Understanding. | Raghavan Komondoor, Ganesan Ramalingam, Satish Chandra, John Field |
| 2005 | FocusCheck: A Tool for Model Checking and Debugging Sequential C Programs. | Curtis W. Keller, Diptikalyan Saha, Samik Basu, Scott A. Smolka |
| 2005 | Efficient Conflict Analysis for Finding All Satisfying Assignments of a Boolean Circuit. | HoonSang Jin, HyoJung Han, Fabio Somenzi |
| 2005 | On Some Transformation Invariants Under Retiming and Resynthesis. | Jie-Hong Roland Jiang |