Computer Aided Verification

Computer-hindered verification (humans can do it too).- Modular abstractions for verifying real-time distributed systems.- Layering techniques for development of parallel systems.- Efficient local correctness checking.- Mechanical verification of concurrent systems with TLA.- Using a theorem prover for reasoning about concurrent algorithms.- Verifying a logic synthesis tool in Nuprl: A case study in software verification.- Higher-level specification and verification with BDDs.- Symbolic bisimulation minimisation.- Towards a verification technique for large synchronous circuits.- Verifying timed behavior automata with nonbinary delay constraints.- Timing verification by successive approximation.- A verification strategy for timing constrained systems.- Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits.- State space caching revisited.- Verification in process algebra of the distributed control of track vehicles—A case study.- Design verification of a microprocessor using branching time regular temporal logic.- A case study in safety-critical design.- Automatic reduction in CTL compositional model checking.- Compositional model checking for linear-time temporal logic.- Property preserving simulations.- Verification with real-time COSPAN.- Model-checking for real-time systems specified in Lotos.- Decidability of bisimulation equivalences for parallel timer processes.- A proof assistant for symbolic model-checking.- Tableau recycling.- Crocos: An integrated environment for interactive verification of SDL specifications.- Verifying general safety and liveness properties with integer programming.- Generating diagnostic information for behavioral preorders.- A verification procedure via invariant for extended communicating finite-state machines.- Efficient ?-regular language containment.- Faster model checking for the modal Mu-Calculus.