| 2007 | A Decision Procedure for Bit-Vectors and Arrays. Vijay Ganesh, David L. Dill |
| 2007 | A JML Tutorial: Modular Specification and Verification of Functional Behavior for Java. Gary T. Leavens, Joseph R. Kiniry, Erik Poll |
| 2007 | A Lazy and Layered SMT($\mathcal{BV}$) Solver for Hard Industrial Verification Problems. Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Ziyad Hanna, Alexander Nadel, Amit Palti, Roberto Sebastiani |
| 2007 | A Mathematical Approach to RTL Verification. David M. Russinoff |
| 2007 | A Tutorial on Satisfiability Modulo Theories. Leonardo Mendonça de Moura, Bruno Dutertre, Natarajan Shankar |
| 2007 | Abstraction and Counterexample-Guided Construction of Marc Segelken |
| 2007 | Adaptive Symmetry Reduction. Thomas Wahl |
| 2007 | Algorithms for Interface Synthesis. Dirk Beyer, Thomas A. Henzinger, Vasu Singh |
| 2007 | An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software. Sumit Gulwani, Ashish Tiwari |
| 2007 | An Accelerated Algorithm for 3-Color Parity Games with an Application to Timed Games. Luca de Alfaro, Marco Faella |
| 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 | Automatically Proving Program Termination. Byron Cook |
| 2007 | BAT: The Bit-Level Analysis Tool. Panagiotis Manolios, Sudarshan K. Srinivasan, Daron Vroon |
| 2007 | Boolean Abstraction for Temporal Logic Satisfiability. Alessandro Cimatti, Marco Roveri, Viktor Schuppan, Stefano Tonetta |
| 2007 | C32SAT: Checking C Expressions. Robert Brummayer, Armin Biere |
| 2007 | CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes. Hubert Garavel, Radu Mateescu, Frédéric Lang, Wendelin Serwe |
| 2007 | CVC3. Clark W. Barrett, Cesare Tinelli |
| 2007 | Comparison Under Abstraction for Verifying Linearizability. Daphna Amit, Noam Rinetzky, Thomas W. Reps, Mooly Sagiv, Eran Yahav |
| 2007 | Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings Werner Damm, Holger Hermanns |
| 2007 | Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis. Dirk Beyer, Thomas A. Henzinger, Grégory Théoduloz |
| 2007 | Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures. Ahmed Bouajjani, Séverine Fratani, Shaz Qadeer |
| 2007 | Fast and Accurate Static Data-Race Detection for Concurrent Programs. Vineet Kahlon, Yu Yang, Sriram Sankaranarayanan, Aarti Gupta |
| 2007 | From Liveness to Promptness. Orna Kupferman, Nir Piterman, Moshe Y. Vardi |
| 2007 | Hector: Software Model Checking with Cooperating Analysis Plugins. Nathaniel Charlton, Michael Huth |
| 2007 | Hybrid Systems: From Verification to Falsification. Erion Plaku, Lydia E. Kavraki, Moshe Y. Vardi |
| 2007 | I/O Efficient Accepting Cycle Detection. Jiri Barnat, Lubos Brim, Pavel Simecek |
| 2007 | LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals. Bernd Becker, Christian Dax, Jochen Eisinger, Felix Klaedtke |
| 2007 | Leaping Loops in the Presence of Abstraction. Thomas Ball, Orna Kupferman, Mooly Sagiv |
| 2007 | Local Proofs for Global Safety Properties. Ariel Cohen, Kedar S. Namjoshi |
| 2007 | Low-Level Library Analysis and Summarization. Denis Gopan, Thomas W. Reps |
| 2007 | Magnifying-Lens Abstraction for Markov Decision Processes. Luca de Alfaro, Pritam Roy |
| 2007 | On Synthesizing Controllers from Bounded-Response Properties. Oded Maler, Dejan Nickovic, Amir Pnueli |
| 2007 | Parallelising Symbolic State-Space Generators. Jonathan Ezekiel, Gerald Lüttgen, Gianfranco Ciardo |
| 2007 | Parameterized Verification of Infinite-State Processes with Global Conditions. Parosh Aziz Abdulla, Giorgio Delzanno, Ahmed Rezine |
| 2007 | Parametric and Sliced Causality. Feng Chen, Grigore Rosu |
| 2007 | RAT: A Tool for the Formal Analysis of Requirements. Roderick Bloem, Roberto Cavada, Ingo Pill, Marco Roveri, Andrei Tchaltsev |
| 2007 | Revamping TVLA: Making Parametric Shape Analysis Competitive. Igor Bogudlov, Tal Lev-Ami, Thomas W. Reps, Mooly Sagiv |
| 2007 | SAT-Based Compositional Verification Using Lazy Learning. Nishant Sinha, Edmund M. Clarke |
| 2007 | Shape Analysis for Composite Data Structures. Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn, Thomas Wies, Hongseok Yang |
| 2007 | Software Bugs Seen from an Industrial Perspective or Can Formal Methods Help on Automotive Software Development? Thomas Kropf |
| 2007 | Spade: Verification of Multithreaded Dynamic and Recursive Programs. Gaël Patin, Mihaela Sighireanu, Tayssir Touili |
| 2007 | Structural Abstraction of Software Verification Conditions. Domagoj Babic, Alan J. Hu |
| 2007 | Systematic Acceleration in Regular Model Checking. Bengt Jonsson, Mayank Saksena |
| 2007 | Test Coverage for Continuous and Hybrid Systems. Tarik Nahhal, Thao Dang |
| 2007 | The TASM Toolset: Specification, Simulation, and Formal Verification of Real-Time Systems. Martin Ouimet, Kristina Lundqvist |
| 2007 | The Why/Krakatoa/Caduceus Platform for Deductive Program Verification. Jean-Christophe Filliâtre, Claude Marché |
| 2007 | Three-Valued Abstraction for Continuous-Time Markov Chains. Joost-Pieter Katoen, Daniel Klink, Martin Leucker, Verena Wolf |
| 2007 | UPPAAL-Tiga: Time for Playing Games! Gerd Behrmann, Agnès Cougnard, Alexandre David, Emmanuel Fleury, Kim Guldstrand Larsen, Didier Lime |
| 2007 | Underapproximation for Model-Checking Based on Random Cryptographic Constructions. Arie Matsliah, Ofer Strichman |
| 2007 | Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra. Chao Wang, Zijiang Yang, Aarti Gupta, Franjo Ivancic |
| 2007 | Verification Across Intellectual Property Boundaries. Sagar Chaki, Christian Schallhart, Helmut Veith |
| 2007 | Verification of Hybrid Systems. Martin Fränzle |
| 2007 | jMoped: A Test Environment for Java Programs. Dejvuth Suwimonteerabuth, Felix Berger, Stefan Schwoon, Javier Esparza |