Computer Aided Verification

Synchronous programming of reactive systems.- Ten years of partial order reduction.- An ACL2 proof of write invalidate cache coherence.- Transforming the theorem prover into a digital design tool: From concept car to off-road vehicle.- A role for theorem proving in multi-processor design.- A formal method experience at secure computing corporation.- Formal methods in an industrial environment.- On checking model checkers.- Finite-state analysis of security protocols.- Integrating proof-based and model-checking techniques for the formal verification of cryptographic protocols.- Verifying systems with infinite but regular state spaces.- Formal verification of out-of-order execution using incremental flushing.- Verification of an implementation of Tomasulo's algorithm by compositional model checking.- Decomposing the proof of correctness of pipelined microprocessors.- Processor verification with precise exceptions and speculative execution.- Symmetry reductions in model checking.- Structural symmetry and model checking.- Using magnetic disk instead of main memory in the Mur ? verifier.- On-the-fly model checking of RCTL formulas.- From pre-historic to post-modern symbolic model checking.- Model checking LTL using net unforldings.- Model checking for a first-order temporal logic using multiway decision graphs.- On the limitations of ordered representations of functions.- BDD based procedures for a theory of equality with uninterpreted functions.- Computing reachable control states of systems modeled with uninterpreted functions and infinite memory.- Multiple counters automata, safety analysis and presburger arithmetic.- A comparison of Presburger engines for EFSM reachability.- Generating finite-state abstractions of reactive systems using decision procedures.- On-the-fly analysis of systems with unbounded, lossy FIFO channels.- Computing abstractions of infinite state systems compositionally and automatically.- Normed simulations.- An experiment in parallelizing an