Program of TACAS


Opening: Tiziana Margaria and Wang Yi

Symbolic Verification
Session chair: Tiziana Margaria

Language Containment Checking with Nondeterministic BDDs
Bernd Finkbeiner (Stanford University)

Satisfiability Checking Using Boolean Expression Diagrams
Poul Frederick Williams, Henrik Reif Andersen, Henrik Hulgaard (IT University of Copenhagen)

A Library for Composite Symbolic Representations
Tuba Yavuz-Kahveci, Murat Tuncer, Tevfik Bultan (University of California)

Infinite State Systems: Deduction and Abstraction
Session chair: Rance Cleaveland

Synthesis of Linear Ranking Functions
Michael A. Colón, Henny B. Sipma (Stanford University)

Automatic Deductive Verification with Invisible Invariants
Amir Pnueli, Sitvanit Ruah (Weizmann Institute),
Lenore Zuck (New York University)

Incremental Verification by Abstraction
Yassine Lakhnech, S. Bensalem (VERIMAG),
S. Berezin (Carnegie Mellon University),
S. Owre (SRI International)

A Technique for Invariant Generation
A. Tiwari, H. Ruess, H. Saidi, N. Shankar (SRI International)

Applications of Model Checking Techniques
Session chair: John Hatcliff

Model Checking Syllabi and Student Careers
Roberto Sebastiani, Alessandro Tomasi, Fausto Giunchiglia (Università di Trento)

Verification of Vortex Workflows
Xiang Fu, Tevfik Bultan, Jianwen Su (University of California)

Parameterized Verification of Multithreaded Software Libraries
Thomas Ball, Sagar Chaki, Sriram K. Rajamani (Microsoft Research)

Timed and Probabilistic Systems
Session chair: Yassine Lakhnech

Efficient Guiding Towards Cost-Optimality in Uppaal
Gerd Behrmann (Aalborg University),
Ansgar Fehnker (University of Nijmegen),
Thomas Hune (Aarhus University),
Kim Larsen (University of Twente),
Paul Pettersson (Uppsala University),
Judi Romijn (University of Nijmegen)

Linear Parametric Model Checking of Timed Automata
Thomas Hune (Aarhus University),
Judi Romijn, Marielle Stoelinga, Frits Vaandrager (University of Nijmegen)

Abstraction in Probabilistic Process Algebra
Suzana Andova, J.C.M. Baeten (Eindhoven University)

First Passage Time Analysis of Stochastic Process Algebra Using Partial Orders
Theo C. Ruys, Rom Langerak, Joost-Pieter Katoen (University of Twente),
Diego Latella, Mieke Massink (CNUCE, Pisa)

Session chair: Ed Brinksma
Michael Fourman (Invited Lecture)
Hardware: Design and Verification
Session chair: Ed Brinksma

Hardware/Software Co-Design using Functional Languages
Alan Mycroft (Cambridge University, AT&T Laboratories),
Richard Sharp (AT&T Laboratories)

Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors
Miroslav Velev (Carnegie Mellon University)

Software verification
Session chair: Susanne Graf

Boolean and Cartesian Abstractions for Model Checking C programs
Thomas Ball, Andreas Podelski, Sriram Rajamani (Microsoft Research)

Finding Feasible Counter-examples when Model Checking Abstracted Java Programs
Corina S. Pãsãreanu, Matthew B. Dwyer (Kansas State Univ.),
W. Visser (Nasa Ames Research Center, Moffet Field)

The LOOP Compiler for Java and JML
Joachim van den Berg, Bart Jacobs (University of Nijmegen)

Symbolic Verification
Session chair: Andreas Podelski

Searching Powerset Automata by Combining Explicit-State and Symbolic Model Checking
Alessandro Cimatti (ITC-IRST, Trento),
Marco Roveri (ITC-IRST, Trento and DSI, Università di Milano),
Piergiorgio Bertoli (ITC-IRST, Trento)

Saturation: An Efficient Iteration Strategy for Symbolic State-space Generation
Gianfranco Ciardo (College of William and Mary, Williamsburg),
Gerald Lüttgen (Sheffield University),
Radu Siminiceanu (College of William and Mary, Williamsburg)

Testing: Techniques and Tools
Session chair: Ed Brinksma

Automated Test Generation from Timed Automata
Brian Nielsen, Arne Skou (Aalborg University)

Testing an Intentional Naming Scheme Using Genetic Algorithms
Sarfraz Khurshid (Massachusetts Institute of Technology, Cambridge)

Building a Tool for the Analysis and Testing of Web Applications: Problems and Solutions
Filippo Ricca, Paolo Tonella (Centro per la Ricerca Scientifica e Tecnologica, Povo di Trento)

TATOO: Testing and Analysis Tool for Object-Oriented Software
Amie L. Souter (University of Delaware),
Tiffany M. Wong (Dartmouth College, Hanover, NH),
Starcey A. Shindo, Lori L. Pollock (University of Delaware)

Tool Demos
Session chair: Hubert Garavel

CPN/Tools: A Tool for Editing and Simulating Coloured Petri Nets
M. Beaudouin-Lafon, W. Mackay, M. Jensen, P. Andersen, P. Janecek, M. Lassen, K. Lund, K. Mortensen, S. Munck, A. Ratzer, K. Ravn, S. Christensen, K. Jensen (Aarhus University)

The ASM Workbench: A Tool Environment for Computer-Aided Analysis and Validation of Abstract State Machine Models
G. Del Castillo (Universität Paderborn)

The EVT Erlang Verification Tool
T. Noll (Royal Institute of Technology, Stockholm),
L. Fredlund, D. Gurov (Swedish Institute of Computer Science, Kista)

Implementation Techniques
Session chair: Doron Peled

Implementing a Multi-Valued Symbolic Model Checker
Marsha Chechik, Benet Devereux, Steve Easterbrook (University of Toronto)

Is There a Best Symbolic Cycle-Detection Algorithm?
Kathi Fisler (Rice University, Worcester Polytechnic Institute),
Ranan Fraer (Intel Development Center, Haifa),
Gila Kamhi (Intel Development Center, Haifa),
Moshe Y. Vardi (Rice University),
Zijiang Yang (Rice University and CCRL, NEC Princeton)

Combining Structural and Enumerative Techniques for the Validation of Bounded Petri Nets
Rubén Carvajal-Schiaffino, Giorgio Delzanno, Giovanni Chiola (Università di Genova)

A Sweep-Line Method for State Space Exploration
Søren Christensen (University of Aarhus),
Lars Michael Kristensen (University of Aarhus and University of South Australia),
Thomas Mailund (University of Aarhus)

Semantics and Compositional Verification
Session chair: Perdita Stevens

Assume-Guarantee based Compositional Reasoning for Synchronous Timing Diagrams
Nina Amla, E. Allen Emerson (University of Texas at Austin),
Kedar Namjoshi (Bell Laboratories, Lucent Technologies),
Richard Trefler (AT&T Research)

Simulation Revisited
Li Tan, Rance Cleaveland (State University of New York at Stony Brook)

Compositional Message Sequence Charts
Elsa Gunter (Bell Laboratories),
Anca Muscholl (University of Paris 7),
Doron Peled (Bell Laboratories)

An Automata Based Interpretation of Live Sequence Charts
Jochen Klose (University of Oldenburg),
Hartmut Wittke (OFFIS Oldenburg)

Logics and Model Checking
Session chair: Wang Yi

Coverage Metrics for Temporal Logic Model Checking
Hana Chockler, Orna Kupferman (Hebrew University),
Moshe Y. Vardi (Rice University)

Parallel Model Checking for the Alternation Free mu-Calculus
Benedikt Bollig, Martin Leucker, Michael Weber (University of Aachen)

Model Checking CTL*[DC]
Paritosh Pandya (Tata Institute of Fundamental Research, Mumbai, India)