TACAS: Bounded Model Checking and SAT-based Methods
Session chair: Moshe Vardi
Automatic Abstraction without Counterexamples
Nina Amla, Kenneth McMillan (Cadence Design Systems, USA)
Bounded Model Checking for Past LTL
Marco Benedetti, Alessandro Cimatti
(Istituto per la Ricerca Scientifica e Tecnologica, I)
Experimental Analysis of Different Techniques for Bounded Model Checking
Nina Amla, Robert Kurshan, Kenneth McMillan, Ricardo Medel
(Cadence Design Systems & Cadence Berkeley Labs &
Stevens Institute of Technology, USA)
12.30 - 14.30:
LUNCH
14.30 - 16.00:
TACAS: Mu-calculus and Temporal Logics
Session chair: Rance Cleaveland
On the Universal and Existential Fragments of the Mu Calculus
Thomas A. Henzinger, Orna Kupferman, Rupak Majumdar
(University of California, USA & Hebrew University, IL)
Resets vs Aborts in Linear Temporal Logic
Roy Armoni, Doron Bustan, Orna Kupferman, Moshe Y. Vardi
(Inter Israel Development Center, IL & Rice University, USA &
Hebrew University, IL)
A Generic On-the-Fly Solver for Alternation-Free Boolean Equation Systems
Radu Mateescu (INRIA Rhone-Alpes, F)
16.00 - 16.30:
coffee
16.30 - 18.30:
TACAS: Verification of Parameterized Systems
Session chair: Alain Finkel
Decidability of Invariant Validation for Parameterized Systems
Pascal Fontaine, Pascal Gribomont (University of Liege, B)
Verification and Improvement of the Sliding Window Protocol
Dmitri Chkliaev, Jozef Hooman, Erik de Vink
(Eindhoven University of Technology, NL &
University of Nijmegen, NL)
Simple Representative Instantiations for Multicast Protocols
Javier Esparza, Monika Maidl (University of Edinburgh, UK)
Rapid Parameterized Model Checking of Snoopy Cache Coherence Protocols
Allen Emerson, Vineet Kahlon (University of Texas, USA)
Tuesday, April 8:
10.30 - 12.30:
TACAS: Abstractions and Counter-examples
Session chair: Kim Larsen
Proof-like Counter-Examples
Arie Gurfinkel, Marsha Chechik (University of Toronto, CDN)
Multiple-Counterexample Guided Iterative Abstraction Refinement:
An Industrial Evaluation
Marcelo Glusman, Gila Kamhi, Sela Mador-Haim,
Ranan Fraer, Moshe Y. Vardi
(The Technion, IL & Intel Corporation, IL & Rice University, USA)
Verification of Hybrid Systems Based on Counterexample-Guided
Abstraction Refinement
Edmund Clarke, Ansgar Fehnker, Zhi Han, Bruce Krogh,
Olaf Stursberg, Michael Theobald
(Carnegie Mellon University, USA & Universitat Dortmund, D)
Counter-example Guided Predicate Abstraction of Hybrid Systems
Rajeev Alur, Thao Dang, Franjo Ivancic
(University of Pennsylvania, USA & CNRS, Verimag, F)
12.30 - 14.30:
LUNCH
14.30 - 16.30:
TACAS: Real-Time and Scheduling
Session chair: Rajeev Alur
Schedulability Analysis Using Two Clocks
Elena Fersman, Leonid Mokrushin, Paul Pettersson, Wang Yi
(Uppsala University, S)
On Optimal Scheduling under Uncertainty
Yasmina Abdeddaim, Eugene Asarin, Oded Maler (VERIMAG, F)
Static Guard Analysis in Timed Automata Verification
Gerd Behrmann, Patricia Bouyer, Emmanuel Fleury, Kim G. Larsen
(Aalborg University, DK & ENS de Cachan, F)
Tool demo: Moby/DC - A Tool for Model-Checking Parametric Real-Time
Specifications
Henning Dierks, Josef Tapken
(University of Oldenburg, D)
Tool demo: VERICS: A Tool for Verifying Timed Automata and Estelle
Specifications
Piotr Dembinski, Agata Janowska, Pawel Janowski, Wojciech Penczek,
Agata Polrola, Maciej Szreter, Bozena Wozna, Andrzej Zbrzezny
(Institute of Comp. Science PAS, PL)
Wednesday, April 9:
15.45 - 16.45:
TACAS: Security and Cryptography
Session chair: Kurt Jensen
A New Knowledge Representation Strategy for Cryptographic Protocol
Analysis
Ivan Cibrario Bertolotti, Luca Durante, Riccardo Sisto, Adriano Valenzano
(Istituto di Elettronica e di Ingegneria dell'Informazione e
delle Telecomunicazioni, I & Politecnico di Torino, I)
Pattern-based Abstraction for Verifying Secrecy in Protocols
Liana Bozga, Lakhnech Yassine, Michael Perin (Verimag, F)
Thursday, April 10:
10.30 - 12.30:
TACAS: Modules and Compositional Verification
Session chair: Bernhard Steffen
Compositional Analysis for Verification of Parameterized Systems
Samik Basu, C.R. Ramakrishnan (SUNY at Stony Brook, USA)
Learning Assumptions for Compositional Verification
Jamieson M. Cobleigh, Dimitra Giannakopoulou, Corina S. Pasareanu
(University of Massachusets, USA & NASA Ames Research Center, USA)
Modular Strategies for Recursive Game Graphs
Rajeev Alur, Salvatore La Torre, P. Madhusudan
(University of Pennsylvania, USA & University of Salerno, I)
12.30 - 14.30:
LUNCH
14.30 - 15.30:
TACAS invited lecture:
Session chair: John Hatcliff
What Are We Trying to Prove? Lessons from our Experiences with
Proof-Carrying Code
Peter Lee (Carnegie Mellon University, USA)
15.45 - 16.45:
TACAS: Symbolic State Spaces and Decision Diagrams
Session chair: Jan Friso Groote
Saturation Unbound
Gianfranco Ciardo, Robert Marmorstein, Radu Siminiceanu
(College of William and Mary, USA)
Construction of Efficient BDDs for Bounded Arithmetic Constraints
Constantinos Bartzis, Tevfik Bultan (University of California, USA)
16.45 - 17.15:
coffee
17.15 - 18.45:
TACAS: Performance and Mobility
Session chair: Joost-Pieter Katoen
Modeling and Analysis of Power-Aware Systems
Kyriakos Christou, Insup Lee, Anna Philippou, Oleg Sokolsky
(University of Pennsylvania, USA & University of Cyprus, CY)
Tool demo: A Set of Performance and Dependability Analysis
Components for CADP
Holger Hermanns, Christophe Joubert
(INRIA Rhone-Alpes, Montbonnot Saint-Martin, F)
Tool demo: The Integrated CWB-NC/PIOA Tool for Functional Verification
and Performance Analysis of Concurrent Systems
Dezhuang Zhang, Rance Cleaveland, Eugene Stark
(State University of New York at Stony Brook, USA)
Tool demo: BANANA: A Tool for Boundary Ambients Nesting ANAlysis
Chiara Braghin, Agostino Cortesi, Stefano Filippone,
Riccardo Focardi, Flaminia L. Luccio, Carla Piazza
(University de Venezia, I)
Friday, April 11:
10.30 - 12.30:
TACAS: State Space Reductions
Session chair: Hubert Garavel
State Class Constructions for Branching Analysis of Time Petri Nets
Bernard Berthomieu, Francois Vernadat (LAAS-CNRS, F)
Branching Processes of High-Level Petri Nets
Victor Khomenko, Maciej Koutny (University of Newcastle, UK)
Using Petri Net Invariants in State Space Construction
Karsten Schmidt (Humboldt-Universitat zu Berlin, D)
Optimistic Synchronization-Based State-Space Reduction
Scott Stoller, Ernie Cohen
(State University of New York at Stony Brook, USA & Cambridge, UK)
12.30 - 14.30:
LUNCH
14.30 - 16.00:
TACAS: Constraint-Solving and Decision Procedures
Session chair: Andreas Podelski
Checking Properties of Heap-Manipulating Procedures with a Constraint Solver
Mandana Vaziri, Daniel Jackson
(Massachusetts Institute of Technology, USA)
An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic
Sergey Berezin, Vijay Ganesh, David L. Dill (Stanford University, USA)
Strategies for Combining Decision Procedures
Sylvain Conchon, Sava Krstic (Oregon Health & Sciences University, USA)
16.00 - 16.30:
coffee
16.30 - 18.30:
TACAS: Testing and Verification
Session chair: Alessandro Fantechi
Generalized Symbolic Execution for Model Checking and Testing
Sarfraz Khurshid, Corina Pasareanu, and Willem Visser
(Massachusets Institute of Technology, USA &
NASA Ames Research Center, USA)
Code-based Test Generation for Validation of Functional Processor
Descriptions
Fabrice Barray, Philippe Codognet, Daniel Diaz, Henri Michel
(ST-Microelectronics, F & University of Paris, F)
Tool demo: Large State Space Visualization
Jan Friso Groote, Frank van Ham
(Technische Universiteit Eindhoven, NL)
Tool demo: Automatic Test Generation with AGATHA
Céline Bigot, Alain Faivre, Jean-Pierre Gallois, Arnault Lapitre,
David Lugato, Jean-Yves Pierron, Nicolas Rapin
(CEA - SACLAY, DRT/LIST/DTSI/SLA, Gif-sur-Yvette, F)
Tool demo: LTSA-MSC: Tool Support for Behaviour Model Elaboration
Using Implied Scenarios
Sebastian Uchitel, Robert Chatley, Jeff Kramer, Jeff Magee
(Imperial College, UK)
