Tools and Algorithms for the Construction and Analysis of Systems: 4th International Conference, TACAS’98 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS’98 Lisbon, Portugal, March 28 – April 4, 1998 Proceedings

Randal E. Bryant (auth.), Bernhard Steffen (eds.)3540643567, 9783540643562

This book constitutes the refereed proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’98, held in conjunction with ETAPS in Lisbon, Portugal, in March/April 1998. The 28 revised full papers presented together with an invited talk were selected from a total of 78 submissions. The volume is devoted to conceptual foundations, development, and applications of tools and algorithms for the specification, verification, analysis, and construction of software and hardware systems. The papers are organized in sections on model checking, design and architecture, various applications, fielded applications, verification of real-time systems, mixed analysis techniques, and case studies and experience.

---

Table of contents :
Formal verification of pipelined processors….Pages 1-4
Fully local and efficient evaluation of alternating fixed points….Pages 5-19
Modular model checking of software….Pages 20-35
Verification based on local states….Pages 36-51
Exploiting symmetry in linear time temporal logic model checking: One step beyond….Pages 52-67
OPEN/CÆSAR: An open software architecture for verification, simulation, and testing….Pages 68-84
Practical model-checking using games….Pages 85-101
Combining finite automata, parallel programs and SDL using Petri nets….Pages 102-117
Mesa: Support for scenario-based design of concurrent systems….Pages 118-135
Efficient modeling of memory arrays in symbolic ternary simulation….Pages 136-150
Translation validation….Pages 151-166
A verified model checker for the modal Μ-calculus in Coq….Pages 167-183
Detecting races in relay ladder logic programs….Pages 184-200
Verification of large state/event systems using compositionality and dependency analysis….Pages 201-216
Tamagotchis need not die — Verification of statemate designs….Pages 217-231
Modeling and verification of sC++ applications….Pages 232-248
Factotum: Automatic and systematic sharing support for systems analyzers….Pages 249-262
Model checking via reachability testing for timed automata….Pages 263-280
Formal design and analysis of a gear controller….Pages 281-297
Verifying networks of timed processes….Pages 298-312
Model checking of real-time reachability properties using abstractions….Pages 313-329
Symbolic exploration of transition hierarchies….Pages 330-344
Static partial order reduction….Pages 345-357
Set-based analysis of reactive infinite-state systems….Pages 358-375
Deciding fixed and non-fixed size bit-vectors….Pages 376-392
Experience with literate programming in the modelling and validation of systems….Pages 393-408
A proof of burns N -process mutual exclusion algorithm using abstraction….Pages 409-423
Automated verification of Szymanski’s algorithm….Pages 424-438
Formal verification of SDL systems at the siemens mobile phone department….Pages 439-455