TACAS 2000 Session list

March 8, 2000

Invited Contribution

(thursday morning)
Chair: Bernhard Steffen
"On the Construction of Automata from Linear Arithmetic Constraints"
Pierre Wolper and Bernhard Boigelot (Univ. Liège)

Software and Formal Methods Tools

(monday afternoon 1)
Chair: Susanne Graf
"An Extensible Type System for Component-Based Design"
Yuhong Xiong and Edward A. Lee (Univ. of California at Berkeley)
"Proof General: A Generic Tool for Proof Development (tool demo)"
David Aspinall (University of Edinburgh)
"ViewPoint-oriented Software Development: Tool Support for Integrating Multiple Perspectives by Distributed Graph Transformation (tool demo)"
M. Goedicke, T. Meyer, B. Enders, G. Taentzer

Formal Methods Tools

(monday afternoon 2)
Chair: Perdita Stevens
"Consistent Integration of Formal Methods (tool)"
Peter Braun, Heiko Lötzbeyer, Bernhard Schätz and Oscar Slotosch (TU München)
"An Architecture for Interactive Program Provers (tool)"
Jörg Meyer, Arnd Poetzsch-Heffter (Fernuniversitaet Hagen)
"The PROSPER Toolkit"
Louise A. Dennis, Graham Collins, Graham Robinson and Tom Melham (Univ. of Glasgow) Michael Norrish, Konrad Slind and Mike Gordon (Univ. of Cambridge), Richard Boulton (Univ. of Edinbourgh)
"CASL: From Semantics to Tools (tool)"
Till Mossakowski (Univ. of Bremen)

Timed and Hybrid Systems

(tuesday morning)
Chair: Ed Brinksma
"On the Construction of Live Timed Systems"
Sebastien Bornot, Gregor Gößler and Joseph Sifakis (VERIMAG, Grenoble)
"On Memory-Block Traversal Problems in Model-Checking Timed Systems  "
Fredrik Larsson, Paul Pettersson and Wang Yi (Uppsala University)
"Symbolic Model Checking for Rectangular Hybrid Systems"
Thomas A. Henzinger and Rupak Majumdar (UC Berkeley)
"Efficient Data Structure for Fully Symbolic Verification of Real Time Software Systems"
Farn Wang (Academia Sinica)

Infinite and Parameterized Systems

(wednesday morning)
Chair: Tiziana Margaria
"Verification of Parameterized Systems using Logic Program Transformations"
Abhik Roychoudhury, K. Narayan Kumar, C.R. Ramakrishnan, I.V. Ramakrishnan and Scott A. Smolka (SUNY, Stony Brook)
"Abstracting WS1S Systems to verify Parameterized Networks"
Kai Baukus (Univ. of Kiel), Saddek Bensalem and Yassine Lakhnech (VERIMAG, Grenoble) and Karsten Stahl (Univ. of Kiel)
"FMona: a Tool for Expressing Validation Techniques over Infinite-State Systems"
J.-P. Bodeveix, M. Filali (IRIT, Toulouse)
"Transitive Closures of Regular Relations for Verifying Infinite State Systems"
Bengt Jonsson and Marcus Nilsson (Uppsala University)

Diagnostic and Test Generation

(wednesday afternoon)
Chair: Claude Jard
"Using Static Analysis to Improve Automatic Test Generation"
Marius Bozga, Jean-Claude Fernandez and Lucian Ghirvu (VERIMAG, Grenoble)
"Efficient Diagnostic Generation for Boolean Equation Systems"
Radu Mateescu (INRIA Rhône-Alpes, Grenoble)

Efficient Model-Checking

(thursday morning)
Chair: Wang Yi
"Compositional State Space Generation with Partial Order Reductions for Asynchronous Communicating Systems"
Jean-Pierre Krimm and Laurent Mounier (VERIMAG, Grenoble)
"Checking for CFFD-preorder with Tester Processes "
Juhana Helovuo and Antti Valmari (Tampere University of Technology)
"Fair Bisimulation"
Thomas A. Henzinger (UC Berkeley), Sriram K. Rajamani (Microsoft Research)
"Integrating Low Level Symmetries into Reachability Analysis"
K. Schmidt

Model-Checking Tools

(thursday afternoon)
Chair: Conny Heitmeyer
"Model checking for the ASM high level language"
Giuseppe Del Castillo (Univ. of Paderborn), Kirsten Winter (GMD Berlin)
"A Markov Chain Model Checker"
Holger Hermanns and Joost-Pieter Katoen Univ. of Twente), Joachim Meyer-Kayser and Markus Siegle (Univ. of Erlangen)
"Model Checking SDL with Spin"
Dragan Bosnacki, Dennis Dams, Leszek Holenderski and Natalia Sidorova (UT Eindhoven)
"Salsa: Combining Constraint Solvers with BDDs for Automatic Invariant Checking"
Ramesh Bharadwaj(Naval Research Lab) and Steve Sims (SUNY Stony Brook)

Symbolic Model-Checking

(friday morning)
Chair: Perdita Stevens
"Symbolic Model Checking of Probabilistic Processes using MTBDDs and the Kronecker Representation"
Luca de Alfaro (UC Berkeley), Marta Kwiatkowska, Gethin Norman and David Parker (Univ. Birmingham) and Roberto Segala (Univ. of Bologna)
"Symbolic Reachability Analysis based on SAT-Solvers"
Parosh Aziz Abdulla (Uppsala University) Per Bjesse, Niklas Eén (Chalmers Univ.)
"Symbolic Representation of Upward-closed Sets"
G.Delzanno (MPI, Saarbrücken) and J.-F. Raskin (UC Berkeley)
"BDD vs. Constraint-Based Model Checking: An Experimental Evaluation for Asynchronous Concurrent Systems"
Tevfik Bultan (UC Santa Barabara)

Visual Tools

(friday afternoon 1)
Chair: Michael Schwartzbach
"Tool-based Specification of Visual Languages and Graphic Editors"
Magnus Niemann and Roswitha Bardohl (TU Berlin)
"VIP: A Visual Editor and Compiler for V-Promela"
Moataz Kamel and Stefan Leue (Univ. of Waterloo, Canada)

Verification of Critical Systems

(friday afternoon 2)
Chair: Claude Jard
"A Comparison of two Verification Methods for Speculative Instruction Execution"
Tamarah Arons and Amir Pnueli (Weizmann Institut)
"Partial Order Reductions for Security Protocol Verification"
Edmund Clarke, Somesh Jha, and Will Marrero (Carnegie Mellon University)
"Model Checking Security Protocols Using a Logic of Belief"
Massimo Benerecetti and Fausto Giunchiglia (DISA, Univ. of Trento)
"A Formal Specification and Validation of a Critical System in Presence of Byzantine Errors"
S. Gnesi, D. Latella and G. Lenzini (CNR, Pisa),C. Abbaneo, A. Amendola and P. Marmo (Ansaldo, I)