Computer Aided Verification: 10th International Conference, CAV’98 Vancouver, BC, Canada, June 28 – July 2, 1998 Proceedings

Nicolas Halbwachs (auth.), Alan J. Hu, Moshe Y. Vardi (eds.)3540646086, 9783540646082

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 included are 11 invited contributions. Among the topics covered are modeling and specification formalisms; verification techniques like state-space exploration, model checking, synthesis, and automated deduction; various verification techniques; applications and case studies, and verification in practice.

---

Table of contents :
Synchronous programming of reactive systems….Pages 1-16
Ten years of partial order reduction….Pages 17-28
An ACL2 proof of write invalidate cache coherence….Pages 29-38
Transforming the theorem prover into a digital design tool: From concept car to off-road vehicle….Pages 39-44
A role for theorem proving in multi-processor design….Pages 45-48
A formal method experience at secure computing corporation….Pages 49-56
Formal methods in an industrial environment….Pages 57-60
On checking model checkers….Pages 61-70
Finite-state analysis of security protocols….Pages 71-76
Integrating proof-based and model-checking techniques for the formal verification of cryptographic protocols….Pages 77-87
Verifying systems with infinite but regular state spaces….Pages 88-97
Formal verification of out-of-order execution using incremental flushing….Pages 98-109
Verification of an implementation of Tomasulo’s algorithm by compositional model checking….Pages 110-121
Decomposing the proof of correctness of pipelined microprocessors….Pages 122-134
Processor verification with precise exceptions and speculative execution….Pages 135-146
Symmetry reductions in model checking….Pages 147-158
Structural symmetry and model checking….Pages 159-171
Using magnetic disk instead of main memory in the Mur ϕ verifier….Pages 172-183
On-the-fly model checking of RCTL formulas….Pages 184-194
From pre -historic to post -modern symbolic model checking….Pages 195-206
Model checking LTL using net unforldings….Pages 207-218
Model checking for a first-order temporal logic using multiway decision graphs….Pages 219-231
On the limitations of ordered representations of functions….Pages 232-243
BDD based procedures for a theory of equality with uninterpreted functions….Pages 244-255
Computing reachable control states of systems modeled with uninterpreted functions and infinite memory….Pages 256-267
Multiple counters automata, safety analysis and presburger arithmetic….Pages 268-279
A comparison of Presburger engines for EFSM reachability….Pages 280-292
Generating finite-state abstractions of reactive systems using decision procedures….Pages 293-304
On-the-fly analysis of systems with unbounded, lossy FIFO channels….Pages 305-318
Computing abstractions of infinite state systems compositionally and automatically….Pages 319-331
Normed simulations….Pages 332-344
An experiment in parallelizing an application using formal methods….Pages 345-356
Efficient symbolic detection of global properties in distributed systems….Pages 357-368
A machine-checked proof of the optimality of a real-time scheduling policy….Pages 369-378
A general approach to partial order reductions in symbolic verification….Pages 379-390
Correctness of the concurrent approach to symbolic verification of interleaved models….Pages 391-402
Verification of timed systems using POSETs….Pages 403-415
Mechanising BAN Kerberos by the inductive method….Pages 416-427
Protocol verification in Nuprl….Pages 428-439
You assume, we guarantee: Methodology and case studies….Pages 440-451
Verification of a parameterized bus arbitration protocol….Pages 452-463
The ‘test model-checking’ approach to the verification of formal memory models of multiprocessors….Pages 464-476
Design constraints in symbolic model checking….Pages 477-487
Verification of floating-point adders….Pages 488-499
Xeve , an Esterel verification environment….Pages 500-504
InVeSt : A tool for the verification of invariants….Pages 505-510
Verifying mobile processes in the HAL environment….Pages 511-515
MONA 1.x: New techniques for WS1S and WS2S….Pages 516-520
MOCHA: Modularity in model checking….Pages 521-525
SCR: A toolset for specifying and analyzing software requirements….Pages 526-531
A toolset for message sequence charts….Pages 532-536
Real-time verification of Statemate designs….Pages 537-541
Optikron: A tool suite for enhancing model-checking of real-time systems….Pages 542-545
Kronos: A model-checking tool for real-time systems….Pages 546-550