Computer Aided Verification

Practical challenges for industrial formal verification tools.- Formal verification of digital systems, from ASICs to HW/SW codesign - a pragmatic approach.- The industrial success of verification tools based on stålmarck's method.- Formal verification - Applications & case studies.- Automatic abstraction techniques for propositional ?-calculus model checking.- A compositional rule for hardware design refinement.- Module checking revisited.- Using compositional preorders in the verification of sliding window protocol.- An efficient decision procedure for the theory of fixed-sized bit-vectors.- Construction of abstract state graphs with PVS.- Verification of a chemical process leak test procedure.- Automatic datapath extraction for efficient usage of HDD.- An n log n algorithm for online BDD refinement.- Weak bisimulation for fully probabilistic processes.- Towards a mechanization of cryptographic protocol verification.- Efficient model checking using tabled resolution.- Containment of regular languages in non-regular timing diagram languages is decidable.- An improved reachability analysis method for strongly linear hybrid systems (extended abstract).- Some progress in the symbolic verification of timed automata.- STARI: A case study in compositional and hierarchical timing verification.- A provably correct embedded verifier for the certification of safety critical software.- Model checking in a microprocessor design project.- Some thoughts on statecharts, 13 years later.- On-the-fly model checking under fairness that exploits symmetry.- Exploiting symmetry when verifying transistor-level circuits by symbolic trajectory evaluation.- Parallelizing the Mur? verifier.- A new heuristic for bad cycle detection using BDDs.- Efficient detection of vacuity in ACTL formulas.- Model checking and transitive-closure logic.- Boolean and 2-adic numbers based techniques for verifying synchronous designs.- Programs with quasi-stable channels are effectively recognizable.- Combining