Tools and Algorithms for the Construction and Analysis of Systems: Third International Workshop, TACAS’97 Enschede, The Netherlands, April 2–4, 1997 Proceedings

Gérard Berry (auth.), Ed Brinksma (eds.)3540627901, 9783540627906

This book constitutes the refereed proceedings of the Third International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS ’97, held in Enschede, The Netherlands, in April 1997.
The book presents 20 revised full papers and 5 tool demonstrations carefully selected out of 54 submissions; also included are two extended abstracts and a full paper corresponding to invited talks. The papers are organized in topical sections on space reduction techniques, tool demonstrations, logical techniques, verification support, specification and analysis, and theorem proving, model checking and applications.

---

Table of contents :
Hardware and software synthesis, optimization, and verification from Esterel programs….Pages 1-3
Manipulation algorithms for K * BMDs….Pages 4-18
Combining partial order and symmetry reductions….Pages 19-34
Partial model checking with ROBDDs….Pages 35-49
Space efficient reachability analysis through use of pseudo-root states….Pages 50-64
The reference component of PEP….Pages 65-80
A tool to support formal reasoning about computer languages….Pages 81-95
The term processor generator Kimwitu ….Pages 96-111
Graphs in Meta Frame: The unifying power of polymorphism….Pages 112-129
A tableau system for linear-TIME temporal logic….Pages 130-144
Model-checking for a subclass of event structures….Pages 145-164
Real-time logics: Fictitious clock as an abstraction of dense time….Pages 165-182
Mosel: A flexible toolset for monadic second-order logic….Pages 183-202
A brief introduction to coloured Petri Nets….Pages 203-208
Design/CPN — A computer tool for Coloured Petri Nets….Pages 209-223
Formal verification of statecharts with instantaneous chain reactions….Pages 224-238
Compositional state space generation from Lotos programs….Pages 239-258
Syntactic detection of process divergence and non-local choice in message sequence charts….Pages 259-274
An automata based verification environment for mobile processes….Pages 275-289
Compositional performance analysis….Pages 290-305
Incremental development of deadlock-free communicating systems….Pages 306-320
Automatic synthesis of specifications from the dynamic observation of reactive programs….Pages 321-333
Visual verification of reactive systems….Pages 334-350
Theorem prover support for the refinement of stream processing functions….Pages 351-365
Integration in PVS: Tables, types, and model checking….Pages 366-383
Test generation for intelligent networks using model checking….Pages 384-398
Mechanically verified self-stabilizing hierarchical algorithms….Pages 399-415
The bounded retransmission protocol must be on time!….Pages 416-431