Checking Cache-Coherence Protocols with TLA (2003)
Rajeev Joshi, John Matthews, Serdar Tasiran, Mark Tuttle, Yuan Yu
We have a great deal of experience using the specification language and its model checker TLC to analyze protocols designed at Digital and Compaq (both now part of HP). The tools and techniques we...
Certifying Compositional Model Checking Algorithms in ACL2 (2003)
Sandip Ray, John Matthews, Mark Tuttle
We prove the soundness of a compositional model checking algorithm using ACL2. The algorithm uses conjunctive and cone of inuence reductions to reduce a large model checking problem into a collection...
Specifying and Verifying Systems with TLA+ (2003)
John Matthews, Mark Tuttle, Yuan Yu
is a high-level specification language that has been used to specify and check the correctness of several hardware protocols. We expect that it can also be used to specify and check concurrent...
The Wildfire Challenge Problem (2001)
Leslie Lamport, Madhu Sharma, Mark Tuttle, Yuan Yu
We pose as a challenge to the verification community the problem of finding errors in the specification of a complicated cache-coherence protocol. It specifies a simplified version of the protocol...
Logical Logging to Extend Recovery to New Domains (2000)
Recovery can be extended to new domains at reduced logging cost by exploiting "logical" log operations. During recovery, a logical log operation may read data values from any recoverable object, not...
Verification of Cache-Coherence Protocols (2000)
Homayoon Akhiani, Damien Doligez, Paul Harter, Leslie Lamport, Mark Tuttle, Yuan Yu, ...
Protocol . . . . . . . . . . . . . . . . . . . . . . 6 3.3 The Lower-Level Protocol . . . . . . . . . . . . . . . . . . . . 7 3.3.1 Writing the Specification . . . . . . . . . . . . . . . . 7 3.3.2...
TLA+ Verification of Cache-Coherence Protocols (1999)
Homayoon Akhiani, Damien Doligez, Paul Harter, Leslie Lamport, Mark Tuttle, Yuan Yu, ...
This paper describes two projects to formally specify and verify cache-coherence protocols for multiprocessor computers being built by Compaq. These protocols are significant components...
Verification of Cache-Coherence Protocols (1999)
Homayoon Akhiani, Damien Doligez, Paul Harter, Leslie Lamport, Mark Tuttle, Yuan Yu, ...
Protocol . . . . . . . . . . . . . . . . . . . . . . 6 3.3 The Lower-Level Protocol . . . . . . . . . . . . . . . . . . . . 7 3.3.1 Writing the Specification . . . . . . . . . . . . . . . . 7 3.3.2...
Verification of Cache-Coherence Protocols (1999)
Homayoon Akhiani, Damien Doligez, Paul Harter, Leslie Lamport, Mark Tuttle, Yuan Yu, ...
Protocol . . . . . . . . . . . . . . . . . . . . . . 6 3.3 The Lower-Level Protocol . . . . . . . . . . . . . . . . . . . . 7 3.3.1 Writing the Specification . . . . . . . . . . . . . . . . 7 3.3.2...
Knowledge and Distributed computation. (1998)
Understanding systems of agents that interact in some way is fundamental to many areas of science, including philosophy, linguistics, economics, game theory, logic artificial intelligence, robotics,...
Logical Logging to Extend Recovery to New Domains (1970)
Recovery can be extended to new domains at reduced logging cost by exploiting "logical" log operations. During recovery, a logical log operation may read data values from any recoverable object, not...
Thesis (M.A.)--Boston University, 1955.
Richesson, Rachel, Young, Ken, Guillette, Heather, Tuttle, Mark, Abbondondolo, Michael, Krischer, Jeffrey
The NIH roadmap endorses the use of data standards in clinical research that are compatible with health care data standards. To facilitate standards use, members of the Rare Disease Clinical Research...
Web-based, Micro-terminology Development: The MMHCC Experience
Wong, Joanne, Kogan, Scott, Cardiff, Robert, Carter, John, Nelson, Victoria, Tuttle, Mark, ...
The MMHCC (Mouse Models of Human Cancers Consortium) is an NCI (National Cancer Institute) initiative aimed at the development, validation, and use of transgenic mouse models to help explore the...
Drug and Chemical Entries in Meta-1
Fuller, Lloyd, Hole, William, Olson, Nels, Schuyler, Peri, Tuttle, Mark
Thirty-two percent of the concepts in the National Library of Medicine's UMLS Metathesaurus, Meta-1 [10], are the names of biomedically important chemicals. This paper describes the origin of the...
Using Meta-1-The 1st Version of the UMLS Metathesaurus
Tuttle, Mark, Sherertz, David, Olson, Nels, Erlbaum, Mark, Sperzel, David, Fuller, Lloyd, ...
The National Library of Medicine (NLM) is developing the Unified Medical Language System (UMLS) to provide uniform access to the world's biomedical knowledge. The foundation of the UMLS is a...
Editing the UMLS Metathesaurus: Review and Enhancement of a Computed Knowledge Source
Sperzel, David, Erlbaum, Mark, Fuller, Lloyd, Sherertz, David, Olson, Nels, Schuyler, Peri, ...
This paper describes the editing of Meta-1, the first official version of the National Library of Medicine's (NLM) Unified Medical Language System (UMLS) Metathesaurus. After a preliminary version of...
A HyperCard Implementation of Meta-1: The First Version of the UMLS Metathesaurus*
Sherertz, David, Tuttle, Mark, Cole, William, Erlbaum, Mark, Olson, Nels, Nelson, Stuart
The Unified Medical Language System (UMLS) is being designed to provide uniform access to computer-based resources in biomedicine. For the foreseeable future, the foundation of the UMLS will be a...
Implementing Meta-1: The First Version of the UMLS Metathesaurus*
Tuttle, Mark, Sherertz, David, Erlbaum, Mark, Olson, Nels, Nelson, Stuart
The Unified Medical Language System (UMLS) is being designed to provide uniform access to computer-based resources in biomedicine. For the foreseeable future, the foundation of the UMLS will be a...