Accepted papers for TACAS'07 ---------------------------- 54 papers out of 204 submissions were accepted. The 54 accepted papers are listed in no particular order: Planned and Traversable Play-Out: A Flexible Method for Executing Scenario-Based Programs David Harel and Itai Segall Counterexamples in Probabilistic Model Checking Tingting Han and Joost-Pieter Katoen Adaptor synthesis for real-time components Massimo Tivoli, Pascal Fradet, Alain Girault, Gregor Goessler Assume Guarantee Synthesis Krishnendu Chatterjee and Thomas A. Henzinger Don't Care Modeling: A logical framework for developing predictive system models Hillel Kugler, Amir Pnueli, Michael Stern, and E. Jane Albert Hubbard Bounded Reachability Checking of Asynchronous Systems Using Decision Diagrams Jinqing Yu, Gianfranco Ciardo, and Gerald Luettgen State of the Union: Type Inference via Craig Interpolation Ranjit Jhala, Rupak Majumdar, and Ru-Gang Xu Bisimulation minimisation mostly speeds up probabilistic model checking Joost-Pieter Katoen, Tim Kemna, Ivan Zapreev, and David N. Jansen Kodkod: A Relational Model Finder Emina Torlak and Daniel Jackson Multi-Objective Model Checking of Markov Decision Processes Kousha Etessami, Marta Kwiatkowska, Moshe Y. Vardi, and Mihalis Yannakakis A Symbolic Algorithm for Optimal Markov Chain Lumping Salem Derisavi Improved algorithms for the automata based approach to model-checking Laurent Doyen and Jean-Francois Raskin VCEGAR: Verilog CounterExample Guided Abstraction Refinement Himanshu Jain, Daniel Kroening, Natasha Sharygina, and Edmund Clarke A Groebner Basis Approach to CNF-formulae Preprocessing Christopher Condrat and Priyank Kalla MAVEN: Modular Aspect Verification Max Goldman and Shmuel Katz A Generic Framework for Reasoning about Dynamic Networks of Infinite-State Processes Ahmed Bouajjani, Yan Jurski, and Mihaela Sighireanu Causal Concurrent Dataflow Analysis for Concurrent Programs Azadeh Farzan and P. Madhusudan Searching for Shapes in Cryptographic Protocols Shaddin F. Doghmi, Joshua D. Guttman, and F. Javier Thayer Shape Analysis by Graph Decomposition Roman Manevich, Joshua Berdine, Byron Cook, Ganesan Ramalingam, and Mooly Sagiv Deciding an Interval Logic with Accumulated Durations Martin Fraenzle and Michael R. Hansen Model Checking Probabilistic Timed Automata with One or Two Clocks Marcin Jurdzinski, Francois Laroussinie, and Jeremy Sproston MoToR: The MoDeST Tool Environment Henrik Bohnenkamp, Holger Hermanns, and Joost-Pieter Katoen mCRL Distributed State Space Generation in Practice Stefan Blom, Jens R. Calame, Bert Lisser, Simona Orzan, Jun Pang, Jaco van de Pol, Mohammad Torabi Dashti, and Anton J. Wijs Complexity in Simplicity: Flexible Agent-based State Space Exploration Jacob Illum Rasmussen, Gerd Behrmann, and Kim G. Larsen From Time Petri Nets to Timed Automata: an Untimed Approach Davide D'Aprile, Susanna Donatelli, Arnaud Sangnier, and Jeremy Sproston Hoare Logic for Realistically Modelled Machine Code Magnus O. Myreen and Michael J. C. Gordon Deciding Bit-Vector Arithmetic with Abstraction Randal E. Bryant, Daniel Kroening, Joel Ouaknine, Sanjit A. Seshia, Ofer Strichman, and Bryan Brady Syntactic Optimizations for PSL Verification Alessandro Cimatti, Marco Roveri, and Stefano Tonetta Faster Algorithms for Finitary Games Florian Horn Regular Model Checking without Transducers (On Efficient Verification of Parameterized Systems) Parosh Aziz Abdulla, Giorgio Delzanno, Noomene Ben Henda, and Ahmed Rezine The Heterogeneous Tool Set Till Mossakowski, Christian Maeder, and Klaus Luettich On Sampling Abstraction of Continuous Time Logic with Durations Paritosh K. Pandya, Shankara Narayanan Krishna, and Kuntal Loya Model Checking of Tree Logics with Path Equivalences Rajeev Alur, Pavol Cerny, and Swarat Chaudhuri Replaying Play in and Play out: Synthesis of Design Models from Scenarios by Learning Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, and Martin Leucker Automatic Analysis of the Security of XOR-based Key Management Schemes Veronique Cortier, Gavin Keighren, and Graham Steel Abstraction Refinement of Linear Programs with Arrays Alessandro Armando, Massimo Benerecetti, and Jacopo Mantovani Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations Lijun Zhang, Holger Hermanns, Friedrich Eisenbrand, and David N. Jansen PReMo: an analyzer for Probabilistic Recursive Models Dominik Wojtczak and Kousha Etessami GOAL: A Graphical Tool for Manipulating Buechi Automata and Temporal Formulae Yih-Kuen Tsay, Yu-Fang Chen, Ming-Hsien Tsai, Kang-Nien Wu, and Wen-Chin Chan Optimized L* for Assume-Guarantee Reasoning Sagar Chaki and Ofer Strichman Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications Marcelo F. Frias, Carlos G. Lopez Pombo, and Mariano M. Moscato Model Checking Liveness Properties of Genetic Regulatory Networks Gregory Batt, Calin Belta, and Ron Weiss Property-Driven Partitioning for Abstraction Refinement Roberto Sebastiani, Stefano Tonetta, and Moshe Y. Vardi Combining Abstraction Refinement and SAT-based Model Checking Nina Amla and Kenneth McMillan Type-dependency Analysis and Program Transformation for Symbolic Execution Saswat Anand, Alessandro Orso, and Mary Jean Harrold Refining Interface Alphabets for Compositional Verification Mihaela Gheorghiu, Dimitra Giannakopoulou, and Corina S. Pasareanu JPF--SE: A Symbolic Execution Extension to Java PathFinder Saswat Anand, Corina S. Pasareanu, and Willem Visser Detecting Races in Ensembles of Message Sequence Charts Edith Elkind, Blaise Genest, and Doron Peled Unfolding Concurrent Well-Structured Transition Systems Frederic Herbreteau, Gregoire Sutre, and The Quang Tran Combined Satisfiability Modulo Parametric Theories Sava Krstic, Amit Goel, Jim Grundy, and Cesare Tinelli Generating Representation Invariants of Structurally Complex Data Muhammad Zubair Malik, Aman Pervaiz, and Sarfraz Khurshid A reachability predicate for analyzing low-level software Shaunak Chatterjee, Shuvendu K. Lahiri, Shaz Qadeer, and Zvonimir Rakamaric Checking Pedigree Consistency with SAT Panagiotis Manolios, Marc Galceran Oms, and Sergi Oliva Valls Uppaal/DMC - Abstraction-based Heuristics for Directed Model Checking Sebastian Kupferschmid