CAV 1998 - PDF Preprint Papers

CAV 1998 International Workshop on Computer Aided Verification

Teaser Browsing | Click Here

Title Browsing | Click Here

Wall of Fame | Most Viewed CAV-1998 Paper

click to vote

CAV
1998
Springer

175views Hardware» more CAV 1998»

An ACL2 Proof of Write Invalidate Cache Coherence

13 years 9 months ago

Download userweb.cs.utexas.edu

As a pedagogical exercise in ACL2, we formalize and prove the correctness of a write invalidate cache scheme. In our formalization, an arbitrary number of processors, each with its...

J. Strother Moore

claim paper

Read More »

Disclaimer and Copyright Notice

Sciweavers respects the rights of all copyright holders and in this regard, authors are only allowed to share a link to their preprint paper on their own website. Every contribution is associated with a desciptive image. It is the sole responsibility of the authors to ensure that their posted image is not copyright infringing. This service is compliant with IEEE copyright.

Id	Views	Title	Status

1	175	An ACL2 Proof of Write Invalidate Cache Coherence	claim
2	147	Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking	claim
3	138	Model Checking for a First-Order Temporal Logic Using Multiway Decision Graphs	claim
4	130	On Checking Model Checkers	claim
5	117	MONA 1.x: New Techniques for WS1S and WS2S	claim
6	108	Decomposing the Proof of Correctness of pipelined Microprocessors	claim
7	106	Synchronous Programming of Reactive Systems	claim
8	103	You Assume, We Guarantee: Methodology and Case Studies	claim
9	100	Mechanising BAN Kerberos by the Inductive Method	claim
10	98	Verification of Timed Systems Using POSETs	claim
11	86	Formal Verification of Out-of-Order Execution Using Incremental Flushing	claim
12	84	From Pre-historic to Post-modern Symbolic Model Checking	claim
13	79	Structural Symmetry and Model Checking	claim
14	77	Generating Finite-State Abstractions of Reactive Systems Using Decision Procedures	claim
15	75	MOCHA: Modularity in Model Checking	claim
16	66	Verification of Floating-Point Adders	claim

Sciweavers

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers