| 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 | A Generic Framework for Reasoning About Dynamic Networks of Infinite-State Processes. Ahmed Bouajjani, Yan Jurski, Mihaela Sighireanu |
| 2007 | A Gröbner Basis Approach to CNF-Formulae Preprocessing. Christopher Condrat, Priyank Kalla |
| 2007 | A Reachability Predicate for Analyzing Low-Level Software. Shaunak Chatterjee, Shuvendu K. Lahiri, Shaz Qadeer, Zvonimir Rakamaric |
| 2007 | A Symbolic Algorithm for Optimal Markov Chain Lumping. Salem Derisavi |
| 2007 | Abstraction Refinement of Linear Programs with Arrays. Alessandro Armando, Massimo Benerecetti, Jacopo Mantovani |
| 2007 | Adaptor Synthesis for Real-Time Components. Massimo Tivoli, Pascal Fradet, Alain Girault, Gregor Gößler |
| 2007 | Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications. Marcelo F. Frias, Carlos López Pombo, Mariano M. Moscato |
| 2007 | Assume-Guarantee Synthesis. Krishnendu Chatterjee, Thomas A. Henzinger |
| 2007 | Automatic Analysis of the Security of XOR-Based Key Management Schemes. Véronique Cortier, Gavin Keighren, Graham Steel |
| 2007 | Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking. Joost-Pieter Katoen, Tim Kemna, Ivan S. Zapreev, David N. Jansen |
| 2007 | Bounded Reachability Checking of Asynchronous Systems Using Decision Diagrams. Andy Jinqing Yu, Gianfranco Ciardo, Gerald Lüttgen |
| 2007 | Causal Dataflow Analysis for Concurrent Programs. Azadeh Farzan, P. Madhusudan |
| 2007 | Checking Pedigree Consistency with PCS. Panagiotis Manolios, Marc Galceran Oms, Sergi Oliva Valls |
| 2007 | Combined Satisfiability Modulo Parametric Theories. Sava Krstic, Amit Goel, Jim Grundy, Cesare Tinelli |
| 2007 | Combining Abstraction Refinement and SAT-Based Model Checking. Nina Amla, Kenneth L. McMillan |
| 2007 | Complexity in Simplicity: Flexible Agent-Based State Space Exploration. Jacob Illum Rasmussen, Gerd Behrmann, Kim Guldstrand Larsen |
| 2007 | Counterexamples in Probabilistic Model Checking. Tingting Han, Joost-Pieter Katoen |
| 2007 | Deciding Bit-Vector Arithmetic with Abstraction. Randal E. Bryant, Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady |
| 2007 | Deciding an Interval Logic with Accumulated Durations. Martin Fränzle, Michael R. Hansen |
| 2007 | Detecting Races in Ensembles of Message Sequence Charts. Edith Elkind, Blaise Genest, Doron A. Peled |
| 2007 | Distributed Analysis with Stefan Blom, Jens R. Calamé, Bert Lisser, Simona Orzan, Jun Pang, Jaco van de Pol, Muhammad Torabi Dashti, Anton Wijs |
| 2007 | Faster Algorithms for Finitary Games. Florian Horn |
| 2007 | Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations. Lijun Zhang, Holger Hermanns, Friedrich Eisenbrand, David N. Jansen |
| 2007 | From Time Petri Nets to Timed Automata: An Untimed Approach. Davide D'Aprile, Susanna Donatelli, Arnaud Sangnier, Jeremy Sproston |
| 2007 | GOAL: A Graphical Tool for Manipulating Büchi Automata and Temporal Formulae. Yih-Kuen Tsay, Yu-Fang Chen, Ming-Hsien Tsai, Kang-Nien Wu, Wen-Chin Chan |
| 2007 | Generating Representation Invariants of Structurally Complex Data. Muhammad Zubair Malik, Aman Pervaiz, Sarfraz Khurshid |
| 2007 | Hoare Logic for Realistically Modelled Machine Code. Magnus O. Myreen, Michael J. C. Gordon |
| 2007 | Improved Algorithms for the Automata-Based Approach to Model-Checking. Laurent Doyen, Jean-François Raskin |
| 2007 | JPF-SE: A Symbolic Execution Extension to Java PathFinder. Saswat Anand, Corina S. Pasareanu, Willem Visser |
| 2007 | Kodkod: A Relational Model Finder. Emina Torlak, Daniel Jackson |
| 2007 | MAVEN: Modular Aspect Verification. Max Goldman, Shmuel Katz |
| 2007 | Model Checking Liveness Properties of Genetic Regulatory Networks. Grégory Batt, Calin Belta, Ron Weiss |
| 2007 | Model Checking Probabilistic Timed Automata with One or Two Clocks. Marcin Jurdzinski, François Laroussinie, Jeremy Sproston |
| 2007 | Model Checking on Trees with Path Equivalences. Rajeev Alur, Pavol Cerný, Swarat Chaudhuri |
| 2007 | Multi-objective Model Checking of Markov Decision Processes. Kousha Etessami, Marta Z. Kwiatkowska, Moshe Y. Vardi, Mihalis Yannakakis |
| 2007 | On Sampling Abstraction of Continuous Time Logic with Durations. Paritosh K. Pandya, Shankara Narayanan Krishna, Kuntal Loya |
| 2007 | Optimized L*-Based Assume-Guarantee Reasoning. Sagar Chaki, Ofer Strichman |
| 2007 | PReMo : An Analyzer for P robabilistic Re cursive Mo dels. Dominik Wojtczak, Kousha Etessami |
| 2007 | Planned and Traversable Play-Out: A Flexible Method for Executing Scenario-Based Programs David Harel, Itai Segall |
| 2007 | Property-Driven Partitioning for Abstraction Refinement. Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi |
| 2007 | Refining Interface Alphabets for Compositional Verification. Mihaela Gheorghiu, Dimitra Giannakopoulou, Corina S. Pasareanu |
| 2007 | Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems). Parosh Aziz Abdulla, Giorgio Delzanno, Noomene Ben Henda, Ahmed Rezine |
| 2007 | Replaying Play In and Play Out: Synthesis of Design Models from Scenarios by Learning. Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, Martin Leucker |
| 2007 | Searching for Shapes in Cryptographic Protocols. Shaddin F. Doghmi, Joshua D. Guttman, F. Javier Thayer |
| 2007 | Shape Analysis by Graph Decomposition. Roman Manevich, Josh Berdine, Byron Cook, G. Ramalingam, Mooly Sagiv |
| 2007 | State of the Union: Type Inference Via Craig Interpolation. Ranjit Jhala, Rupak Majumdar, Ru-Gang Xu |
| 2007 | Syntactic Optimizations for PSL Verification. Alessandro Cimatti, Marco Roveri, Stefano Tonetta |
| 2007 | THERE AND BACK AGAIN: Lessons Learned on the Way to the Market. Rance Cleaveland |
| 2007 | The Heterogeneous Tool Set, Hets. Till Mossakowski, Christian Maeder, Klaus Lüttich |
| 2007 | Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007, Proceedings Orna Grumberg, Michael Huth |
| 2007 | Type-Dependence Analysis and Program Transformation for Symbolic Execution. Saswat Anand, Alessandro Orso, Mary Jean Harrold |
| 2007 | Unfolding Concurrent Well-Structured Transition Systems. Frédéric Herbreteau, Grégoire Sutre, The Quang Tran |
| 2007 | Uppaal/DMC- Abstraction-Based Heuristics for Directed Model Checking. Sebastian Kupferschmid, Klaus Dräger, Jörg Hoffmann, Bernd Finkbeiner, Henning Dierks, Andreas Podelski, Gerd Behrmann |
| 2007 | VCEGAR: Verilog CounterExample Guided Abstraction Refinement. Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke |
| 2007 | Verifying Object-Oriented Software: Lessons and Challenges. K. Rustan M. Leino |
| 2007 | motor: The modestTool Environment. Henrik C. Bohnenkamp, Holger Hermanns, Joost-Pieter Katoen |