PROGRAM OF TACAS

Program of TACAS

MONDAY 2/4

11.00
12.30
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)

15.00
17.00 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)

17.30
19.00 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)

TUESDAY 3/4

10.30
12.30 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)

15.00
16.00 Session chair: Ed Brinksma Michael Fourman (Invited Lecture)

16.00
17.00 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)

17.30
19.00 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)

WEDNESDAY 4/4

16.00
17.00 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)

THURSDAY 5/4

10.30
12.30 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)

15.00
17.00 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)

FRIDAY 6/4

10.30
12.30 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)

15.00
17.00 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)

17.30
19.00 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)

MONDAY 2/4
11.00 12.30	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)
15.00 17.00	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)
17.30 19.00	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)
TUESDAY 3/4
10.30 12.30	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)
15.00 16.00	Session chair: Ed Brinksma Michael Fourman (Invited Lecture)
16.00 17.00	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)
17.30 19.00	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)
WEDNESDAY 4/4
16.00 17.00	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)
THURSDAY 5/4
10.30 12.30	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)
15.00 17.00	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)
FRIDAY 6/4
10.30 12.30	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)
15.00 17.00	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)
17.30 19.00	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)