Computer aided verification : 10th International Conference, CAV'98, Vancouver, B.C., Canada June 28-July 2, 1998 : proceedings /
Alan J. Hu, Moshe Y. Vardi (eds.)
Berlin : Springer, 1998.
ix, 552 p. : ill ; 24 cm.
A Look Inside
Main Description
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 Systemsp. 1
Ten Years of Partial Order Reductionp. 17
An ACL2 Proof of Write Invalidate Cache Coherencep. 29
Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehiclep. 39
A Role for Theorem Proving in Multi-Processor Designp. 45
A Formal Method Experience at Secure Computing Corporationp. 49
Formal Methods in an Industrial Environmentp. 57
On Checking Model Checkersp. 61
Finite-State Analysis of Security Protocolsp. 71
Integrating Proof-Based and Model-Checking Techniques for the Formal Verification of Cryptographic Protocolsp. 77
Verifying Systems with Infinite but Regular State Spacesp. 88
Formal Verification of Out-of-Order Execution Using Incremental Flushingp. 98
Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checkingp. 110
Decomposing the Proof of Correctness of Pipelined Microprocessorsp. 122
Processor Verification with Precise Exceptions and Speculative Executionp. 135
Symmetry Reductions in Model Checkingp. 147
Structural Symmetry and Model Checkingp. 159
Using Magnetic Disk Instead of Main Memory in the Muro Verifierp. 172
On-the-Fly Model Checking of RCTL Formulasp. 184
From Pre-historic to Post-modern Symbolic Model Checkingp. 195
Model Checking LTL Using Net Unfoldingsp. 207
Model Checking for a First-Order Temporal Logic Using Multiway Decision Graphsp. 219
On the Limitations of Ordered Representations of Functionsp. 232
BDD Based Procedures for a Theory of Equality with Uninterpreted Functionsp. 244
Computing Reachable Control States of Systems Modeled with Uninterpreted Functions and Infinite Memoryp. 256
Multiple Counters Automata, Safety Analysis, and Presburger Arithmeticp. 268
A Comparison of Presburger Engines for EFSM Reachabilityp. 280
Generating Finite-State Abstractions of Reactive Systems Using Decision Proceduresp. 293
On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channelsp. 305
Computing Abstractions of Infinite State Systems Compositionally and Automaticallyp. 319
Normed Simulationsp. 332
An Experiment in Parallelizing an Application Using Formal Methodsp. 345
Efficient Symbolic Detection of Global Properties in Distributed Systemsp. 357
A Machine-Checked Proof of the Optimality of a Real-Time Scheduling Policyp. 369
A General Approach to Partial Order Reductions in Symbolic Verificationp. 379
Correctness of the Concurrent Approach to Symbolic Verification of Interleaved Modelsp. 391
Verification of Timed Systems Using POSETsp. 403
Mechanising BAN Kerberos by the Inductive Methodp. 416
Protocol Verification in Nuprlp. 428
You Assume, We Guarantee: Methodology and Case Studiesp. 440
Verification of a Parameterized Bus Arbitration Protocolp. 452
The 'Test Model-Checking' Approach to the Verification of Formal Memory Models of Multiprocessorsp. 464
Design Constraints in Symbolic Model Checkingp. 477
Verification of Floating-Point Addersp. 488
Xeve: An Esterel Verification Environmentp. 500
InVeSt: A Tool for the Verification of Invariantsp. 505
Verifying Mobile Processes in the HAL Environmentp. 511
Mona 1.x: New Techniques for WSIS and WS2Sp. 516
MOCHA: Modularity in Model Checkingp. 521
SCR: A Toolset for Specifying and Analyzing Software Requirementsp. 526
A Toolset for Message Sequence Chartsp. 532
Real-Time Verification of Statemate Designsp. 537
Optikron: A Tool Suite for Enhancing Model-Checking of Real-Time Systemsp. 542
Kronos: A Model-Checking Tool for Real-Time Systemsp. 546
Author Indexp. 551
Table of Contents provided by Blackwell. All Rights Reserved.

This information is provided by a service that aggregates data from review sources and other sources that are often consulted by libraries, and readers. The University does not edit this information and merely includes it as a convenience for users. It does not warrant that reviews are accurate. As with any review users should approach reviews critically and where deemed necessary should consult multiple review sources. Any concerns or questions about particular reviews should be directed to the reviewer and/or publisher.

  link to old catalogue

Report a problem