TACAS 2003

Monday, April 7:

11.00 - 12.30:

Bounded Model Checking and SAT-based Methods (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)

14.30 - 16.00:

Mu-calculus and Temporal Logics (Chair: Amir Pneli)

• 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.30 - 18.30:

Verification of Parameterized Systems (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:

Abstractions and Counter-examples (Chair: Kim Larsen)

• Proof-like Counter-Examples
  Arie Gurfinkel, Marsha Chechik (University of Toronto, CDN)
• Multiple-Counterexample Guided Iterative Abstraction Refinement
  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: An Industrial Evaluation
  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)

14.30 - 16.30:

Real-Time and Scheduling (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 Dembiński, Agata Janowska, Paweł Janowski, Wojciech Penczek, Agata Półrola, Maciej Szreter, Bożena Woźna, Andrzej Zbrzeźny (Institute of Comp. Science PAS, PL)

Wednesday, April 9:

15.45 - 16.45:

Security and Cryptography (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:

Modules and Compositional Verification (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)
• Automated Module Composition
  Stavros Tripakis (VERIMAG, F)
• Modular Strategies for Recursive Game Graphs
  Rajeev Alur, Salvatore La Torre, P. Madhusudan (University of Pennsylvania, USA & University of Salerno, I)

14.30 - 15.30:

TACAS invited lecture (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:

Symbolic State Spaces and Decision Diagrams (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)

17.15 - 18.45:

Performance and Mobility (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:

State Space Reductions (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)

14.30 - 16.00:

Constraint-Solving and Decision Procedures (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.30 - 18.30:

Testing and Verification (Chair: Alessandro Cimatti)

• 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)

Back to the TACAS 2003 Home Page