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 constraint solving and symbolic model checking for a class of systems with non-linear constraints.- Relaxed visibility enhances partial order reduction.- Partial-order reduction in symbolic state space exploration.- Deadlock checking using net unfoldings.- Trace table based approach for pipelined microprocessor verification.- On combining formal and informal verification.- Efficient modeling of memory arrays in symbolic simulation.- Symbolic model checking of infinite state systems using presburger arithmetic.- Parametrized verification of linear networks using automata as invariants.- Symbolic model checking with rich assertional languages.- The invariant checker: Automated deductive verification of reactive systems.- The PEP tool.- TermiLog: A system for checking termination of queries to logic programs.- Mosel: A sound and efficient tool for M2L(Str).- The verus tool: A quantitative approach to the formal verification of real-time systems.- Uppaal: Status & developments.- HyTech: A model checker for hybrid systems.- SMC: A symmetry based model checker for verification of liveness properties.- ?cke — Efficient ?-calculus model checking.- Prod 3.2 An advanced tool for efficient reachability analysis.- VeriSoft: A tool for the automatic analysis of concurrent reactive software.- RuleBase: Model checking at IBM.