


default search action
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
Volume 20, Number 2, March 2002
- 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
Volume 20, Number 3, May 2002
- 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

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














