Computer Aided Verification 10th International Conference, CAV'98, Vancouver, BC, Canada, June 28-July 2, 1998, Proceedings
This book consitutes the refereed proceedings of the 10th International Conference on Computer Aided Verification, CAV'98, held in Vancouver, BC, Canada, in June/July 1998. The 33 revised full papers and 10 tool papers presented were carefully selected from a total of 117 submissions. Also incl...
| Other Authors: | , |
|---|---|
| Format: | eBook |
| Language: | English |
| Published: |
Berlin, Heidelberg
Springer Berlin Heidelberg
1998, 1998
|
| Edition: | 1st ed. 1998 |
| Series: | Lecture Notes in Computer Science
|
| Subjects: | |
| Online Access: | |
| Collection: | Springer Book Archives -2004 - Collection details see MPG.ReNa |
Table of Contents:
- InVeSt : A tool for the verification of invariants
- Verifying mobile processes in the HAL environment
- MONA 1.x: New techniques for WS1S and WS2S
- MOCHA: Modularity in modelchecking
- SCR: A toolset for specifying and analyzing software requirements
- A toolset for message sequence charts
- Real-time verification of Statemate designs
- Optikron: A tool suite for enhancing model-checking of real-time systems
- Kronos: A model-checking tool for real-time systems
- 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
- Computing abstractions of infinite state systems compositionally and automatically
- Normed simulations
- An experiment in parallelizing an application using formal methods
- Efficient symbolic detection of global properties in distributed systems
- A machine-checked proof of the optimality of a real-time scheduling policy
- A general approach to partial order reductions in symbolic verification
- Correctness of the concurrent approach to symbolic verification of interleaved models
- Verification of timed systems using POSETs
- Mechanising BAN Kerberos by the inductive method
- Protocol verification in Nuprl
- You assume, we guarantee: Methodology and case studies
- Verification of a parameterized bus arbitration protocol
- The ‘test model-checking’ approach to the verification of formal memory models of multiprocessors
- Design constraints in symbolic model checking
- Verification of floating-point adders
- Xeve, an Esterel verification environment
- 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