Tools and Algorithms for the Construction and Analysis of Systems

by Tacas 2000; Graf, Susanne; Schwartzbach, Michael I.

• ISBN13: 9783540672821
• ISBN10: 3540672826
• Format: Paperback
• Copyright: 2000-05-01
• Publisher: Springer Nature

Summary

This book constitutes the refereed proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2000, held as part of ETAPS 2000 in Berlin, Germany, in March/April 2000.The 33 revised full papers presented together with one invited paper and two short tool descriptions were carefully reviewed and selected from a total of 107 submissions. The papers are organized in topical sections on software and formal methods, formal methods, timed and hybrid systems, infinite and parameterized systems, diagnostic and test generation, efficient model checking, model-checking tools, symbolic model checking, visual tools, and verification of critical systems.

Table of Contents

Invited Contribution
On the Construction of Automata from Linear Arithmetic Constraints	1	(19)
Pierre Wolper
Bernard Boigelot
Software and Formal Methods Tools
An Extensible Type System for Component-Based Design	20	(18)
Yuhong Xiong
Edward A. Lee
Proof General: A Generic Tool for Proof Development	38	(5)
David Aspinall
ViewPoint-Oriented Software Development: Tool Support for Integrating Multiple Perspectives by Distributed Graph Transformation	43	(5)
Michael Goedicke
Bettina Enders
Torsten Meyer
Gabriele Taentzer
Formal Methods Tools
Consistent Integration of Formal Methods	48	(15)
Peter Braun
Heiko Lotzbeyer
Bernhard Schatz
Oscar Slotosch
An Architecture for Interactive Program Provers	63	(15)
Jorg Meyer
Arnd Poetzsch-Heffter
The PROSPER Toolkit	78	(15)
Louise A. Dennis
Graham Collins
Michael Norrish
Richard Boulton
Konrad Slind
Graham Robinson
Mike Gordon
Tom Melham
CASL: From Semantics to Tools	93	(16)
Till Mossakowski
Timed and Hybrid Systems
On the Construction of Live Timed Systems	109	(18)
Sebastien Bornot
Gregor Goβler
Joseph Sifakis
On Memory-Block Traversal Problems in Model-Checking Timed Systems	127	(15)
Fredrik Larsson
Paul Pettersson
Wang Yi
Symbolic Model Checking for Rectangular Hybrid Systems	142	(15)
Thomas A. Henzinger
Rupak Majumdar
Efficient Data Structure for Fully Symbolic Verification of Real-Time Software Systems	157	(15)
Farn Wang
Infinite and Parameterized Systems
Verification of Parameterized Systems Using Logic Program Transformations	172	(16)
Abhik Roychoudhury
K. Narayan Kumar
C.R. Ramakrishnan
I.V. Ramakrishnan
Scott A. Smolka
Abstracting WSIS Systems to Verify Parameterized Networks	188	(16)
Kai Baukus
Saddek Bensalem
Yassine Lakhnech
Karsten Stahl
FMona: A Tool for Expressing Validation Techniques over Infinite State Systems	204	(16)
J.-P. Bodeveix
M. Filali
Transitive Closures of Regular Relations for Verifying Infinite-State Systems	220	(15)
Bengt Jonsson
Marcus Nilsson
Diagnostic and Test Generation
Using Static Analysis to Improve Automatic Test Generation	235	(16)
Marius Bozga
Jean-Claude Fernandez
Lucian Ghirvu
Efficient Diagnostic Generation for Boolean Equation Systems	251	(15)
Radu Mateescu
Efficient Model-Checking
Compositional State Space Generation with Partial Order Reductions for Asynchronous Communicating Systems	266	(17)
Jean-Pierre Krimm
Laurent Mounier
Checking for CFFD-Preorder with Tester Processes	283	(16)
Juhana Helovuo
Antti Valmari
Fair Bisimulation	299	(16)
Thomas A. Henzinger
Sriram K. Rajamani
Integrating Low Level Symmetries into Reachability Analysis	315	(16)
Karsten Schmidt
Model-Checking Tools
Model Checking Support for the ASM High-Level Language	331	(16)
Giuseppe Del Castillo
Kirsten Winter
Markov Chain Model Checker	347	(16)
Holger Hermanns
Joost-Pieter Katoen
Joachim Meyer-Kayser
Markus Siegle
Model Checking SDL with Spin	363	(15)
Dragan Bosnacki
Dennis Dams
Leszek Holenderski
Natalia Sidorova
Salsa: Combining Constraint Solvers with BDDs for Automatic Invariant Checking	378	(17)
Ramesh Bharadwaj
Steve Sims
Symbolic Model-Checking
Symbolic Model Checking of Probabilistic Processes Using MTBDDs and the Kronecker Representation	395	(16)
Luca de Alfaro
Marta Kwiatkowska
Gethin Norman
David Parker
Roberto Segala
Symbolic Reachability Analysis Based on SAT-Solvers	411	(15)
Parosh Aziz Abdulla
Per Bjesse
Niklas Een
Symbolic Representation of Upward-Closed Sets	426	(15)
Giorgio Delzanno
Jean-Francois Raskin
BDD vs. Constraint-Based Model Checking: An Experimental Evaluation for Asynchronous Concurrent Systems	441	(15)
Tevfik Bultan
Visual Tools
Tool-Based Specification of Visual Languages and Graphic Editors	456	(15)
Magnus Niemann
Roswitha Bardohl
VIP: A Visual Editor and Compiler for v-Promela	471	(16)
Moataz Kamel
Stefan Leue
Verification of Critical Systems
A Comparison of Two Verification Methods for Speculative Instruction Execution	487	(16)
Tamarah Arons
Amir Pnueli
Partial Order Reductions for Security Protocol Verification	503	(16)
Edmund Clarke
Somesh Jha
Will Marrero
Model Checking Security Protocols Using a Logic of Belief	519	(16)
Massimo Benerecetti
Fausto Giunchiglia
A Formal Specification and Validation of a Critical System in Presence of Byzantine Errors	535	(16)
S. Gnesi
D. Latella
G. Lenzini
C. Abbaneo
A. Amendola
P. Marmo
Author Index	551