Interesting Papers and Theses
Model Checking
A methodology for hardware verification using
compositional model checking - Ken McMillan
Basically describes the theory behind SMV.
A Performance Study of BDD-Based
Model Checking - B.Yang et al
Decidability of model-checking for
infinite-state concurrent systems - J.Esparza
Exploiting Symmetry in Temporal Logic Model
Checking - E.M. Clarke, R. Enders, T. Filkorn, S. Jha
Induction in Compositional Model
Checking - K.L. McMillan, S.Qadeer, J.Saxe
Symmetry and Induction in Model
Checking - E.M. Clarke, S. Jha
Memory Models and Protocol Verification
A Characterization of Scalable Shared
Memories - P.Kohli, G.Neiger, M.Ahamad
A New Approach for the Verification of
Cache Coherence Protocols - F.Pong, M.Dubois
A Survey of Verification
Techniques for Cache Coherence Protocols - F.Pong, M.Dubois
Automatable Verification of Sequential
Consistency - A.E.Condon, A.J.Hu
Automatic Verification of Parameterized Cache
Coherence Protocols - Giorgio Delzanno
Cache Coherence Protocols: Evaluation
using a Multiprocessor Simulation Model - J.Archibald, J.Baer
Formal Automatic Verification of
Cache Coherence in Multiprocessors with Relaxed Memory Models
- F.Pong, M.Dubois
Lamport Clocks: Reasoning about
Shared-Memory Correctness - D.J.Sorin, M.Plakal, M.D.Hill, A.E.Condon
Lazy Caching - Y.Afek,
G.Brown, M.Merrill
On the Verification of Memory Models of
Shared-Memory Multiprocessors - S.Qadeer
Shared Memory Consistency Models: A
Tutorial - S.V.Adve, K.Gharachorloo
Teapot: Language Support for Writing
Memory Coherence Protocols - S.Chandra, B.Richards, J.R.Larus
Verification of Cache Coherence Protocols by
Aggregation of Distributed Transactions - S.Park, D.L.Dill
Verification Theory
A Structural Induction Theorem for
Processes - R.P.Kurshan, K.McMillan
Abstract Interpretation - Patrick Cousot
Checking Safety Properties using Compositional
Reachability Analysis - Shing Chi Cheung and Jeff Kramer
Construction of abstract
state graphs with PVS - S.Graf, H.Saidi
Control and
Data Abstraction : The Cornerstones of Practical Formal
Verification - Y. Kesten, A. Pnueli
Deciding Global Partial-Order properties -
Rajeev Alur, Ken McMillan, Doron Peled
Formal Methods: State of the art and
future directions - Edmund M. Clarke and Jeannette M. Wing
Good survey paper
Formal Specification and Verification for
Critical Systems: Tools, Achievements and Prospects - John Rushby
Formal Verification of Complex Coherence
Protocols Using Symbolic State Models - F.Pong, M.Dubois
Model-checking of correctness conditions
for concurrent objects - R.Alur, K.McMillan, D.Peled
Modularization and Abstraction: The Keys to
Practical Formal Verification - Y.Kesten, A. Pnueli
Partial-Order Methods for Model Checking: From
Linear Time to Branching Time - B. Willems, P.Wolper
Partial-Order Methods for Temporal
Verification - P.Wolper, P. Godefroid
"Sometimes" and "Not Never" Revisited: On
Branching versus Linear Time Temporal Logic - E.A. Emerson, J.Y.Halpern
Symbolic Boolean Manipulation with
Ordered Binary Decision Diagrams - Randal E. Bryant
Time, Clocks and the Ordering of Events
in a Distributed System - L.Lamport
Undecidability of Partial Order
Logics - Rajeev Alur, Doron Peled
Verifying Temporal Properties without
Temporal Logic - Bowen Alpern and Fred Schneider
What's between simulation and formal
verification ? - David L. Dill
Slides from CAV 99 presentation
win and sin: Predicate Transformers for
Concurrency - Leslie Lamport
Theses
Designing Memory Consistency Models
for Shared-Memory Multiprocessors - Sarita V. Adve
State Reduction Methods for Automatic
Formal Verification - Chung-Wah Norris Ip
Techniques for Efficient Formal
Verification using Binary Decision Diagrams - Alan John Hu