| 2007 | Shape Analysis by Graph Decomposition. | Roman Manevich, Josh Berdine, Byron Cook, G. Ramalingam, Mooly Sagiv |
| 2007 | Generating Representation Invariants of Structurally Complex Data. | Muhammad Zubair Malik, Aman Pervaiz, Sarfraz Khurshid |
| 2007 | Verifying Object-Oriented Software: Lessons and Challenges. | K. Rustan M. Leino |
| 2007 | Uppaal/DMC- Abstraction-Based Heuristics for Directed Model Checking. | Sebastian Kupferschmid, Klaus Drger, Jrg Hoffmann, Bernd Finkbeiner, Henning Dierks, Andreas Podelski, Gerd Behrmann |
| 2007 | "Don't Care" Modeling: A Logical Framework for Developing Predictive System Models. | Hillel Kugler, Amir Pnueli, Michael J. Stern, E. Jane Albert Hubbard |
| 2007 | Combined Satisfiability Modulo Parametric Theories. | Sava Krstic, Amit Goel, Jim Grundy, Cesare Tinelli |
| 2007 | Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking. | Joost-Pieter Katoen, Tim Kemna, Ivan S. Zapreev, David N. Jansen |
| 2007 | Model Checking Probabilistic Timed Automata with One or Two Clocks. | Marcin Jurdzinski, Franois Laroussinie, Jeremy Sproston |
| 2007 | State of the Union: Type Inference Via Craig Interpolation. | Ranjit Jhala, Rupak Majumdar, Ru-Gang Xu |
| 2007 | VCEGAR: Verilog CounterExample Guided Abstraction Refinement. | Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke |
| 2007 | Faster Algorithms for Finitary Games. | Florian Horn |
| 2007 | Unfolding Concurrent Well-Structured Transition Systems. | Frdric Herbreteau, Grgoire Sutre, The Quang Tran |
| 2007 | Planned and Traversable Play-Out: A Flexible Method for Executing Scenario-Based Programs | David Harel, Itai Segall |
| 2007 | Counterexamples in Probabilistic Model Checking. | Tingting Han, Joost-Pieter Katoen |
| 2007 | MAVEN: Modular Aspect Verification. | Max Goldman, Shmuel Katz |
| 2007 | Refining Interface Alphabets for Compositional Verification. | Mihaela Gheorghiu, Dimitra Giannakopoulou, Corina S. Pasareanu |
| 2007 | Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications. | Marcelo F. Frias, Carlos Lpez Pombo, Mariano M. Moscato |
| 2007 | Deciding an Interval Logic with Accumulated Durations. | Martin Frnzle, Michael R. Hansen |
| 2007 | Causal Dataflow Analysis for Concurrent Programs. | Azadeh Farzan, P. Madhusudan |
| 2007 | Multi-objective Model Checking of Markov Decision Processes. | Kousha Etessami, Marta Z. Kwiatkowska, Moshe Y. Vardi, Mihalis Yannakakis |
| 2007 | Detecting Races in Ensembles of Message Sequence Charts. | Edith Elkind, Blaise Genest, Doron A. Peled |
| 2007 | Improved Algorithms for the Automata-Based Approach to Model-Checking. | Laurent Doyen, Jean-Franois Raskin |
| 2007 | Searching for Shapes in Cryptographic Protocols. | Shaddin F. Doghmi, Joshua D. Guttman, F. Javier Thayer |
| 2007 | A Symbolic Algorithm for Optimal Markov Chain Lumping. | Salem Derisavi |
| 2007 | From Time Petri Nets to Timed Automata: An Untimed Approach. | Davide D'Aprile, Susanna Donatelli, Arnaud Sangnier, Jeremy Sproston |