TACAS 2000 Session list
March 8, 2000
(thursday morning)
Chair: Bernhard Steffen
"On the Construction of Automata from Linear Arithmetic Constraints"
Pierre Wolper and Bernhard Boigelot (Univ. Liège)
(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
(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)
(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)
(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)
(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)
(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
(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)
(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)
(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)
(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)