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
Volume 20, Number 2, March 2002
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
Volume 20, Number 3, May 2002
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
Copyright ©
Sat May 16 23:59:09 2009 by
Michael Ley
(
ley@uni-trier.de
)