| 2007 | The TASM Toolset: Specification, Simulation, and Formal Verification of Real-Time Systems. | Martin Ouimet, Kristina Lundqvist |
| 2007 | Test Coverage for Continuous and Hybrid Systems. | Tarik Nahhal, Thao Dang |
| 2007 | A Tutorial on Satisfiability Modulo Theories. | Leonardo Mendona de Moura, Bruno Dutertre, Natarajan Shankar |
| 2007 | Underapproximation for Model-Checking Based on Random Cryptographic Constructions. | Arie Matsliah, Ofer Strichman |
| 2007 | BAT: The Bit-Level Analysis Tool. | Panagiotis Manolios, Sudarshan K. Srinivasan, Daron Vroon |
| 2007 | On Synthesizing Controllers from Bounded-Response Properties. | Oded Maler, Dejan Nickovic, Amir Pnueli |
| 2007 | A JML Tutorial: Modular Specification and Verification of Functional Behavior for Java. | Gary T. Leavens, Joseph R. Kiniry, Erik Poll |
| 2007 | From Liveness to Promptness. | Orna Kupferman, Nir Piterman, Moshe Y. Vardi |
| 2007 | Software Bugs Seen from an Industrial Perspective or Can Formal Methods Help on Automotive Software Development? | Thomas Kropf |
| 2007 | Three-Valued Abstraction for Continuous-Time Markov Chains. | Joost-Pieter Katoen, Daniel Klink, Martin Leucker, Verena Wolf |
| 2007 | Fast and Accurate Static Data-Race Detection for Concurrent Programs. | Vineet Kahlon, Yu Yang, Sriram Sankaranarayanan, Aarti Gupta |
| 2007 | Systematic Acceleration in Regular Model Checking. | Bengt Jonsson, Mayank Saksena |
| 2007 | Anzu: A Tool for Property Synthesis. | Barbara Jobstmann, Stefan J. Galler, Martin Weiglhofer, Roderick Bloem |
| 2007 | Array Abstractions from Proofs. | Ranjit Jhala, Kenneth L. McMillan |
| 2007 | Automated Assumption Generation for Compositional Verification. | Anubhav Gupta, Kenneth L. McMillan, Zhaohui Fu |
| 2007 | An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software. | Sumit Gulwani, Ashish Tiwari |
| 2007 | Low-Level Library Analysis and Summarization. | Denis Gopan, Thomas W. Reps |
| 2007 | CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes. | Hubert Garavel, Radu Mateescu, Frdric Lang, Wendelin Serwe |
| 2007 | A Decision Procedure for Bit-Vectors and Arrays. | Vijay Ganesh, David L. Dill |
| 2007 | Verification of Hybrid Systems. | Martin Frnzle |
| 2007 | The Why/Krakatoa/Caduceus Platform for Deductive Program Verification. | Jean-Christophe Fillitre, Claude March |
| 2007 | Parallelising Symbolic State-Space Generators. | Jonathan Ezekiel, Gerald Lttgen, Gianfranco Ciardo |
| 2007 | Automatically Proving Program Termination. | Byron Cook |
| 2007 | Local Proofs for Global Safety Properties. | Ariel Cohen, Kedar S. Namjoshi |
| 2007 | Boolean Abstraction for Temporal Logic Satisfiability. | Alessandro Cimatti, Marco Roveri, Viktor Schuppan, Stefano Tonetta |