Tools and Algorithms for the Construction and Analysis of Systems: 4th International Conference, TACAS'98, Held as Part of the Joint European ... March 28 - April 4, 1998, Proceeding

by Bernhard Steffen (Editor)

Formal verification of pipelined processors.- Fully local and efficient evaluation of alternating fixed points.- Modular model checking of software.- Verification based on local states.- Exploiting symmetry in linear time temporal logic model One step beyond.- OPEN/CÆ An open software architecture for verification, simulation, and testing.- Practical model-checking using games.- Combining finite automata, parallel programs and SDL using Petri nets.- Support for scenario-based design of concurrent systems.- Efficient modeling of memory arrays in symbolic ternary simulation.- Translation validation.- A verified model checker for the modal ?-calculus in Coq.- Detecting races in relay ladder logic programs.- Verification of large state/event systems using compositionality and dependency analysis.- Tamagotchis need not die - Verification of statemate designs.- Modeling and verification of sC++ applications.- Automatic and systematic sharing support for systems analyzers.- Model checking via reachability testing for timed automata.- Formal design and analysis of a gear controller.- Verifying networks of timed processes.- Model checking of real-time reachability properties using abstractions.- Symbolic exploration of transition hierarchies.- Static partial order reduction.- Set-based analysis of reactive infinite-state systems.- Deciding fixed and non-fixed size bit-vectors.- Experience with literate programming in the modelling and validation of systems.- A proof of burns N-process mutual exclusion algorithm using abstraction.- Automated verification of Szymanski's algorithm.- Formal verification of SDL systems at the siemens mobile phone department.

476 pages, Paperback

First published March 18, 1998