Formal Methods in System Design, Volume 20

Volume 20, Number 1, January 2002

Dominique Méry, Beverly A. Sanders: Editorial Note. 5 BibTeX
K. Mani Chandy, Michel Charpentier: An Experiment in Program Composition and Proof. 7-21 BibTeX
Jayadev Misra: A Simple, Object-Based View of Multiprogramming. 23-45 BibTeX
Gruia-Catalin Roman, Peter J. McCann: A Notation and Logic for Mobile Computing. 47-68 BibTeX
Jean-Paul Bodeveix, Mamoun Filali: Reduction and Quantifier Elimination Techniques for Program Validation. 69-89 BibTeX
Ruben Gamboa: The Correctness of the Fast Fourier Transform: A Structured Proof in ACL2. 91-106 BibTeX
Ratan Nalumasu, Ganesh Gopalakrishnan: Deriving Efficient Cache Coherence Protocols Through Refinement. 107-125 BibTeX

Warren A. Hunt Jr.: Introduction: Special Issue on Microprocessor Verifications. 135-137 BibTeX
Robert B. Jones, Jens U. Skakkebæk, David L. Dill: Formal Verification of Out-of-Order Execution with Incremental Flushing. 139-158 BibTeX
Sergey Berezin, Edmund M. Clarke, Armin Biere, Yunshan Zhu: Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function. 159-186 BibTeX
Jun Sawada, Warren A. Hunt Jr.: Verification of FM9801: An Out-of-Order Microprocessor Model with Speculative Execution, Exceptions, and Program-Modifying Capability. 187-222 BibTeX

Ratan Nalumasu, Ganesh Gopalakrishnan: An Efficient Partial Order Reduction Algorithm with an Alternative Proviso Implementation. 231-247 BibTeX
Teodor Rus, Eric Van Wyk, Tom Halverson: Generating Model Checkers from Algebraic Specifications. 249-284 BibTeX
Javier Esparza, Stefan Römer, Walter Vogler: An Improvement of McMillan's Unfolding Algorithm. 285-310 BibTeX
Christoph Scholl, Bernd Becker, Thomas M. Weis: On WLCDs and the Complexity of Word-Level Decision Diagrams-A Lower Bound for Division. 311-326 BibTeX