Formal Methods in System Design, Volume 20

Volume 20, Number 1, January 2002

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

Warren A. Hunt Jr.: Introduction: Special Issue on Microprocessor Verifications. 135-137
Robert B. Jones, Jens U. Skakkebæk, David L. Dill: Formal Verification of Out-of-Order Execution with Incremental Flushing. 139-158
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
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

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