Computer-Aided Verification

This volume is the proceedings of a workshop presenting results that lead to new or more powerful computer aided verification methods: advances in the use of binary decision diagrams, dense time, reductions based upon partial order representations, and proof-checking in controller verification.

Inhalt
Temporal logic model checking: Two techniques for avoiding the state explosion problem.- Automatic verification of extensions of hardware descriptions.- Papetri : Environment for the analysis of PETRI nets.- Verifying temporal properties of sequential machines without building their state diagrams.- Formal verification of digital circuits using symbolic ternary system models.- Vectorized model checking for computation tree logic.- to a computational theory and implementation of sequential hardware equivalence.- Auto/autograph.- A data path verifier for register transfer level using temporal logic language Tokio.- The use of model checking in ATPG for sequential circuits.- Compositional design and verification of communication protocols, using labelled petri nets.- Issues arising in the analysis of L.0.- Automated RTL verification based on predicate calculus.- On using protean to verify ISO FTAM protocol.- Quantitative temporal reasoning.- Using partial-order semantics to avoid the state explosion problem in asynchronous systems.- A stubborn attack on state explosion.- Using optimal simulations to reduce reachability graphs.- Using partial orders to improve automatic verification methods.- Compositional minimization of finite state systems.- Minimal model generation.- A context dependent equivalence relation between kripke structures.- The modular framework of computer-aided verification.- Verifying liveness properties by verifying safety properties.- Memory efficient algorithms for the verification of temporal properties.- A unified approach to the deadlock detection problem in networks of communicating finite state machines.- Branching time regular temporal logic for model checking with linear time complexity.- The algebraic feedback product of automata.- Synthesizing processes and schedulers from temporal specifications.- Task-driven supervisory control of discrete event systems.- A proof lattice-based technique for analyzing liveness of resource controllers.- Verification of a multiprocessor cache protocol using simulation relations and higher-order logic (summary).- Computer assistance for program refinement.- Program verification by symbolic execution of hyperfinite ideal machines.- Extension of the Karp and miller procedure to lotos specifications.- An algebra for delay-insensitive circuits.- Finiteness conditions and structural construction of automata for all process algebras.- On automatically explaining bisimulation inequivalence.