% BibTeX bibliography file
@techreport{jovial:pv,
TITLE = {A {JOVIAL} Verifier},
AUTHOR = {B. Elspas and M. Green and M. Moriconi and R. Shostak},
MONTH = jan,
YEAR = 1979,
INSTITUTION = {Computer Science Laboratory, SRI International}
}
@article{Robinson&Levitt,
TITLE = {Proof Techniques for Hierarchically Structured Programs},
AUTHOR = {Lawrence Robinson and Karl N. Levitt},
JOURNAL = {Communications of the ACM},
PAGES = {271--283},
VOLUME = 20,
NUMBER = 4,
MONTH = apr,
YEAR = 1976
}
@manual{HDM:Handbook,
TITLE = {The {HDM} Handbook},
AUTHOR = {L. Robinson and K. N. Levitt and B. A. Silverberg},
MONTH = jun,
YEAR = 1979,
ORGANIZATION = {Computer Science Laboratory, SRI International},
ADDRESS = {Menlo Park, CA},
NOTE = {Three Volumes}
}
@article{Spitzen:example,
TITLE = {An Example of Hierarchical Design and Proof},
AUTHOR = {Jay M. Spitzen and Karl N. Levitt and Lawrence Robinson},
JOURNAL = {Communications of the ACM},
PAGES = {1064--1075},
VOLUME = 21,
NUMBER = 12,
MONTH = dec,
YEAR = 1978
}
@techreport{Feiertag:Tool,
TITLE = {A Technique for Proving Specifications are Multilevel
Secure},
AUTHOR = {R. J. Feiertag},
NUMBER = {CSL-109},
MONTH = jan,
YEAR = 1980,
INSTITUTION = {Computer Science Laboratory, SRI International},
ADDRESS = {Menlo Park, CA}
}
@inproceedings{FLR77,
TITLE = {Proving Multilevel Security of a System Design},
AUTHOR = {R. J. Feiertag and K. N. Levitt and L. Robinson},
BOOKTITLE = {Sixth ACM Symposium on Operating System Principles},
PAGES = {57--65},
MONTH = nov,
YEAR = 1977
}
@inproceedings{Benzel:scomp-eval,
TITLE = {Analysis of a Kernel Verification},
AUTHOR = {Terry Vickers Benzel},
BOOKTITLE = {Proceedings of the Symposium on Security and Privacy},
PAGES = {125--131},
MONTH = apr,
YEAR = 1984,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Oakland, CA}
}
@inproceedings{Silverman83,
TITLE = {Reflections on the Verification of the Security of an
Operating System Kernel},
AUTHOR = {J. M. Silverman},
BOOKTITLE = {Ninth ACM Symposium on Operating System Principles},
PAGES = {143--154},
MONTH = oct,
YEAR = 1983,
ADDRESS = {Bretton Woods, NH},
NOTE = {(ACM Operating Systems Review, Vol.\ 17, No.\ 5)}
}
@manual{Criteria,
TITLE = {Department of Defense Trusted Computer System Evaluation
Criteria},
MONTH = dec,
YEAR = 1985,
ORGANIZATION = {Department of Defense},
NOTE = {DOD 5200.28-STD (supersedes CSC-STD-001-83)}
}
@inproceedings{Lindsay88:Regency,
TITLE = {A Taxonomy of the Causes of Proof Failures in Applications
Using the {HDM} Methodology},
AUTHOR = {Kenneth S. Lindsay},
BOOKTITLE = {Fourth Aerospace Computer Security Applications
Conference},
PAGES = {419--423},
MONTH = dec,
YEAR = 1988,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Orlando, FL},
NOTE = {Reprinted in~\cite[pp.~79--83]{Compass89}}
}
@inproceedings{Regency88,
TITLE = {A Description of a Formal Verification and Validation
{(FVV)} Process},
AUTHOR = {Bill Smith and Cynthia Reese and Kenneth S. Lindsay
and Brian Crane},
BOOKTITLE = {Fourth Aerospace Computer Security Applications
Conference},
PAGES = {401--408},
MONTH = dec,
YEAR = 1988,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Orlando, FL},
NOTE = {Reprinted in~\cite[pp.~71--78]{Compass89}}
}
@book{Boyer-Moore79,
TITLE = {A Computational Logic},
AUTHOR = {R. S. Boyer and J S. Moore},
PUBLISHER = {Academic Press},
YEAR = 1979,
ADDRESS = {New York, NY}
}
@inproceedings{STP,
TITLE = {{STP}: A Mechanized Logic for Specification and Verification},
AUTHOR = {R. E. Shostak and R. Schwartz and P. M. Melliar-Smith},
BOOKTITLE = {6th International Conference on Automated Deduction
(CADE)},
EDITOR = {D. Loveland},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 138,
YEAR = 1982,
ADDRESS = {New York, NY}
}
@article{Shostak:sup-inf,
TITLE = {On the {SUP-INF} Method for Proving {Presburger} Formulas},
AUTHOR = {Robert E. Shostak},
JOURNAL = {Journal of the ACM},
PAGES = {529--543},
VOLUME = 24,
NUMBER = 4,
MONTH = oct,
YEAR = 1977
}
@article{Shostak:equality,
TITLE = {An Algorithm for Reasoning about Equality},
AUTHOR = {Robert E. Shostak},
JOURNAL = {Communications of the ACM},
PAGES = {583--585},
VOLUME = 21,
NUMBER = 7,
MONTH = jul,
YEAR = 1978
}
@article{Shostak:arithmetic,
TITLE = {A Practical Decision Procedure for Arithmetic with Function
Symbols},
AUTHOR = {Robert E. Shostak},
JOURNAL = {Journal of the ACM},
PAGES = {351--360},
VOLUME = 26,
NUMBER = 2,
MONTH = apr,
YEAR = 1979
}
@article{Shostak:residues,
TITLE = {Deciding Linear Inequalities by Computing Loop Residues},
AUTHOR = {Robert E. Shostak},
JOURNAL = {Journal of the ACM},
PAGES = {769--779},
VOLUME = 28,
NUMBER = 4,
MONTH = oct,
YEAR = 1981
}
@article{Shostak:combination,
TITLE = {Deciding Combinations of Theories},
AUTHOR = {Robert E. Shostak},
JOURNAL = {Journal of the ACM},
PAGES = {1--12},
VOLUME = 31,
NUMBER = 1,
MONTH = jan,
YEAR = 1984
}
@inproceedings{Weinstock80,
TITLE = {{SIFT}: System Design and Implementation},
AUTHOR = {Charles B. Weinstock},
BOOKTITLE = {Fault Tolerant Computing Symposium 10},
PAGES = {75--77},
MONTH = oct,
YEAR = 1980,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Kyoto, Japan},
NOTE = {Reprinted in~\cite[pp.\ 29--30]{FTCS-highlights}}
}
@article{SIFT-design,
TITLE = {{SIFT}: Design and Analysis of a Fault-Tolerant Computer
for Aircraft Control},
AUTHOR = {John H. Wensley and Leslie Lamport and Jack Goldberg
and Milton W. Green and Karl N. Levitt and P. M. Melliar-Smith
and Robert E. Shostak and Charles B. Weinstock},
JOURNAL = {Proceedings of the IEEE},
PAGES = {1240--1255},
VOLUME = 66,
NUMBER = 10,
MONTH = oct,
YEAR = 1978
}
@article{Sift-verif,
TITLE = {Formal Specification and Verification of {SIFT}: A Fault-Tolerant
Flight Control System},
AUTHOR = {P. M. Melliar-Smith and R. L. Schwartz},
JOURNAL = {IEEE Transactions on Computers},
PAGES = {616--630},
VOLUME = {C-31},
NUMBER = 7,
MONTH = jul,
YEAR = 1982
}
@proceedings{SIFT:review,
TITLE = {Peer Review of a Formal Verification/Design Proof Methodology},
MONTH = jul,
YEAR = 1983,
ORGANIZATION = {NASA Conference Publication 2377}
}
@incollection{Shostak:circuits,
TITLE = {Formal Verification of Circuit Designs},
AUTHOR = {Robert E. Shostak},
BOOKTITLE = {Computer Hardware Description Languages},
EDITOR = {T. Uehara and M. Barbacci},
PAGES = {13--29},
PUBLISHER = {North-Holland},
YEAR = 1983
}
@techreport{Kemmerer:assess,
TITLE = {Verification Assessment Study Final Report},
AUTHOR = {Richard A. Kemmerer},
BOOKTITLE = {Verification Assessment Study Final Report},
NUMBER = {C3-CR01-86},
YEAR = 1986,
INSTITUTION = {National Computer Security Center},
ADDRESS = {Ft.\ Meade, MD},
NOTE = {5 Volumes (Overview, Gypsy, Affirm, FDM, and {\sc Ehdm}).
US distribution only}
}
@inproceedings{Melliar-Smith&Rushby,
TITLE = {The {Enhanced HDM} System for Specification and Verification},
AUTHOR = {P. Michael Melliar-Smith and John Rushby},
BOOKTITLE = {Proc.\ VerkShop III},
PAGES = {41--43},
MONTH = feb,
YEAR = 1985,
ADDRESS = {Watsonville, CA},
NOTE = {Published as ACM Software Engineering Notes, Vol.\ 10,
No.\ 4, Aug.\
85}
}
@inproceedings{Rushby:HDM,
TITLE = {The Security Model of {Enhanced HDM}},
AUTHOR = {John Rushby},
BOOKTITLE = {Proceedings 7th DoD/NBS Computer Security Initiative
Conference},
PAGES = {120--136},
MONTH = sep,
YEAR = 1984,
ADDRESS = {Gaithersburg, MD}
}
@inproceedings{EHDM:Overview88,
TITLE = {The {{\sc Ehdm}} Verification Environment: An Overview},
AUTHOR = {F. W. von Henke and J. S. Crow and R. Lee and J. M.
Rushby and R. A. Whitehurst},
BOOKTITLE = {Proceedings 11th National Computer Security Conference},
PAGES = {147--155},
MONTH = oct,
YEAR = 1988,
ORGANIZATION = {NBS/NCSC},
ADDRESS = {Baltimore, MD}
}
@techreport{EHDM:tutorial,
TITLE = {An Introduction to Formal Specification and Verification
Using {{\sc Ehdm}}},
AUTHOR = {John Rushby and Friedrich von Henke and Sam Owre},
NUMBER = {SRI-CSL-91-2},
MONTH = feb,
YEAR = 1991,
INSTITUTION = {Computer Science Laboratory, SRI International},
ADDRESS = {Menlo Park, CA}
}
@inproceedings{DiVito-DCCA-3,
TITLE = {Formal Techniques for Synchronized Fault-Tolerant Systems},
AUTHOR = {Ben L. {Di Vito} and Ricky W. Butler},
BOOKTITLE = {Dependable Computing for Critical Applications---3},
EDITOR = {C. E. Landwehr and B. Randell and L. Simoncini},
PAGES = {163--188},
PUBLISHER = {Springer-Verlag, Vienna, Austria},
SERIES = {Dependable Computing and Fault-Tolerant Systems},
VOLUME = 8,
MONTH = sep,
YEAR = 1992
}
@techreport{Miner93,
TITLE = {Verification of Fault-Tolerant Clock Synchronization
Systems},
AUTHOR = {Paul S. Miner},
TYPE = {NASA Technical Paper},
NUMBER = 3349,
MONTH = nov,
YEAR = 1993,
INSTITUTION = {NASA Langley Research Center},
ADDRESS = {Hampton, VA}
}
@techreport{Rushby92:OM,
TITLE = {Formal Verification of an {Oral Messages} Algorithm
for Interactive Consistency},
AUTHOR = {John Rushby},
NUMBER = {SRI-CSL-92-1},
MONTH = jul,
YEAR = 1992,
INSTITUTION = {Computer Science Laboratory, SRI International},
ADDRESS = {Menlo Park, CA},
NOTE = {Also available as NASA Contractor Report 189704, October
1992}
}
@incollection{Rushby93:masking,
TITLE = {A Fault-Masking and Transient-Recovery Model for Digital
Flight-Control Systems},
AUTHOR = {John Rushby},
BOOKTITLE = {Formal Techniques in Real-Time and Fault-Tolerant
Systems},
CHAPTER = 5,
EDITOR = {Jan Vytopil},
PAGES = {109--136},
PUBLISHER = {Kluwer},
SERIES = {Kluwer International Series in Engineering and Computer
Science},
YEAR = 1993,
ADDRESS = {Boston, Dordecht, London}
}
@inproceedings{Rushby94:icah,
TITLE = {A Formally Verified Algorithm for Clock Synchronization
Under a Hybrid Fault Model},
AUTHOR = {John Rushby},
BOOKTITLE = {Thirteenth ACM Symposium on Principles of Distributed
Computing},
PAGES = {304--313},
MONTH = aug,
YEAR = 1994,
ORGANIZATION = {Association for Computing Machinery},
ADDRESS = {Los Angeles, CA},
NOTE = {Also available as NASA Contractor Report 198289}
}
@article{Rushby&vonHenke93,
TITLE = {Formal Verification of Algorithms for Critical Systems},
AUTHOR = {John Rushby and Friedrich von Henke},
JOURNAL = {IEEE Transactions on Software Engineering},
PAGES = {13--23},
VOLUME = 19,
NUMBER = 1,
MONTH = jan,
YEAR = 1993
}
@inproceedings{Shankar:clocks:Nijmegen,
TITLE = {Mechanical Verification of a Generalized Protocol for
{Byzantine} Fault-Tolerant Clock Synchronization},
AUTHOR = {Natarajan Shankar},
BOOKTITLE = {Formal Techniques in Real-Time and Fault-Tolerant
Systems},
EDITOR = {J. Vytopil},
PAGES = {217--236},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 571,
MONTH = jan,
YEAR = 1992,
ADDRESS = {Nijmegen, The Netherlands}
}
@article{Butler-Sjogren91,
TITLE = {Formal Design Verification of Digital Circuitry},
AUTHOR = {Ricky W. Butler and Jon A. Sjogren},
JOURNAL = {Reliability Engineering and System Safety},
PAGES = {67--93},
VOLUME = 32,
YEAR = 1991
}
@inproceedings{Joyce&all:compcon,
TITLE = {From Formal Verification to Silicon Compilation},
AUTHOR = {J. Joyce and E. Liu and J. Rushby and N. Shankar and
R. Suaya and F. von Henke},
BOOKTITLE = {IEEE Compcon},
PAGES = {450--455},
MONTH = feb,
YEAR = 1991,
ADDRESS = {San Francisco, CA}
}
@manual{PVS:tutorial,
TITLE = {PVS Tutorial},
AUTHOR = {N. Shankar and S. Owre and J. M. Rushby},
MONTH = feb,
YEAR = 1993,
ORGANIZATION = {Computer Science Laboratory, SRI International},
ADDRESS = {Menlo Park, CA},
NOTE = {Also appears in Tutorial Notes, {\em Formal Methods Europe
'93: Industrial-Strength Formal Methods}, pages 357--406,
Odense, Denmark, April 1993}
}
@inproceedings{PVS96:CAV,
TITLE = {{PVS}: Combining Specification, Proof Checking, and
Model Checking},
AUTHOR = {S. Owre and S. Rajan and J.M. Rushby and N. Shankar
and M.K. Srivas},
BOOKTITLE = {Computer-Aided Verification, CAV '96},
EDITOR = {Rajeev Alur and Thomas A. Henzinger},
PAGES = {411--414},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1102,
MONTH = {July/August},
YEAR = 1996,
ADDRESS = {New Brunswick, NJ}
}
@inproceedings{PVS-CADE92,
TITLE = {{PVS}: A Prototype Verification System},
AUTHOR = {S. Owre and J. M. Rushby and N. Shankar},
BOOKTITLE = {11th International Conference on Automated Deduction
(CADE)},
EDITOR = {Deepak Kapur},
PAGES = {748--752},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = 607,
MONTH = jun,
YEAR = 1992,
ADDRESS = {Saratoga, NY}
}
@inproceedings{Shankar96:FMCAD,
TITLE = {{PVS}: Combining Specification, Proof Checking, and
Model Checking},
AUTHOR = {N. Shankar},
BOOKTITLE = {Formal Methods in Computer-Aided Design (FMCAD '96)},
EDITOR = {Mandayam Srivas and Albert Camilleri},
PAGES = {257--264},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1166,
MONTH = nov,
YEAR = 1996,
ADDRESS = {Palo Alto, CA}
}
@inproceedings{Owre-etal98:FM-TRENDS,
TITLE = {{PVS:} An Experience Report},
AUTHOR = {Sam Owre and John Rushby and N. Shankar and David Stringer-Calvert},
BOOKTITLE = {Applied Formal Methods---FM-Trends 98},
EDITOR = {Dieter Hutter and Werner Stephan and Paolo Traverso
and Markus Ullman},
PAGES = {338--345},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1641,
MONTH = oct,
YEAR = 1998,
ADDRESS = {Boppard, Germany}
}
@manual{PVS:language,
TITLE = {PVS Language Reference},
AUTHOR = {S. Owre and N. Shankar and J. M. Rushby and D. W. J.
Stringer-Calvert},
MONTH = sep,
YEAR = 1999,
ORGANIZATION = {Computer Science Laboratory, SRI International},
ADDRESS = {Menlo Park, CA}
}
@manual{PVS:prover,
TITLE = {PVS Prover Guide},
AUTHOR = {N. Shankar and S. Owre and J. M. Rushby and D. W. J.
Stringer-Calvert},
MONTH = sep,
YEAR = 1999,
ORGANIZATION = {Computer Science Laboratory, SRI International},
ADDRESS = {Menlo Park, CA}
}
@manual{PVS:userguide,
TITLE = {PVS System Guide},
AUTHOR = {S. Owre and N. Shankar and J. M. Rushby and D. W. J.
Stringer-Calvert},
MONTH = sep,
YEAR = 1999,
ORGANIZATION = {Computer Science Laboratory, SRI International},
ADDRESS = {Menlo Park, CA}
}
@techreport{PVS-Semantics:TR,
TITLE = {The Formal Semantics of {PVS}},
AUTHOR = {Sam Owre and Natarajan Shankar},
NUMBER = {SRI-CSL-97-2},
MONTH = aug,
YEAR = 1997,
INSTITUTION = {Computer Science Laboratory, SRI International},
ADDRESS = {Menlo Park, CA}
}
@article{Owre95:prolegomena,
TITLE = {Formal Verification for Fault-Tolerant Architectures:
Prolegomena to the Design of {PVS}},
AUTHOR = {Sam Owre and John Rushby and Natarajan Shankar and
Friedrich von Henke},
JOURNAL = {IEEE Transactions on Software Engineering},
PAGES = {107--125},
VOLUME = 21,
NUMBER = 2,
MONTH = feb,
YEAR = 1995
}
@article{Rushby98:TSE,
TITLE = {Subtypes for Specifications: Predicate Subtyping in
{PVS}},
AUTHOR = {John Rushby and Sam Owre and N. Shankar},
JOURNAL = {IEEE Transactions on Software Engineering},
PAGES = {709--720},
VOLUME = 24,
NUMBER = 9,
MONTH = sep,
YEAR = 1998
}
@inproceedings{Shankar&Owre:WADT99,
TITLE = {Principles and Pragmatics of Subtyping in {PVS}},
AUTHOR = {Natarajan Shankar and Sam Owre},
BOOKTITLE = {Recent Trends in Algebraic Development Techniques,
{WADT '99}},
EDITOR = {Didier Bert and Christine Choppy and Peter Mosses},
PAGES = {37--52},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1827,
MONTH = sep,
YEAR = 1999,
ADDRESS = {Toulouse, France}
}
@techreport{Butler:PVS-tut,
TITLE = {An Elementary Tutorial on Formal Specification and Verification
Using {PVS 2}},
AUTHOR = {Ricky W. Butler},
TYPE = {NASA Technical Memorandum},
NUMBER = 108991,
MONTH = jun,
YEAR = 1993,
INSTITUTION = {NASA Langley Research Center},
ADDRESS = {Hampton, VA},
NOTE = {Revised June 1995. Available, with PVS specification
files, at \url{http://atb-www.larc.nasa.gov/ftp/larc/PVS-tutorial};
use only files marked ``revised.''}
}
@misc{WIFT-Tut,
TITLE = {A Tutorial Introduction to {PVS}},
AUTHOR = {Judy Crow and Sam Owre and John Rushby and Natarajan
Shankar and Mandayam Srivas},
HOWPUBLISHED = {Presented at WIFT '95: Workshop on Industrial-Strength
Formal Specification Techniques, Boca Raton, Florida},
MONTH = apr,
YEAR = 1995,
INSTITUTION = {Computer Science Laboratory, SRI International},
ADDRESS = {Menlo Park, CA},
NOTE = {Available, with specification files, at \url{http://www.csl.sri.com/wift-tutorial.html}}
}
@techreport{Rushby&Stringer-Calvert95,
TITLE = {A Less Elementary Tutorial for the {PVS} Specification
and Verification System},
AUTHOR = {John Rushby and David W. J. Stringer-Calvert},
NUMBER = {SRI-CSL-95-10},
MONTH = jun,
YEAR = 1995,
INSTITUTION = {Computer Science Laboratory, SRI International},
ADDRESS = {Menlo Park, CA},
NOTE = {Revised, July 1996. Available, with specification files,
at \url{http://www.csl.sri.com/csl-95-10.html}}
}
@inproceedings{Owre94:TPCD,
TITLE = {A Tutorial on Using {PVS} for Hardware Verification},
AUTHOR = {S. Owre and J. M. Rushby and N. Shankar and M. K. Srivas},
BOOKTITLE = {Theorem Provers in Circuit Design ({TPCD} '94)},
EDITOR = {Ramayya Kumar and Thomas Kropf},
PAGES = {258--279},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 910,
MONTH = sep,
YEAR = 1994,
ADDRESS = {Bad Herrenalb, Germany}
}
@techreport{PVS-ADT:TR,
TITLE = {Abstract Datatypes in {PVS}},
AUTHOR = {Sam Owre and Natarajan Shankar},
NUMBER = {SRI-CSL-93-9R},
MONTH = dec,
YEAR = 1993,
INSTITUTION = {Computer Science Laboratory, SRI International},
ADDRESS = {Menlo Park, CA},
NOTE = {Extensively revised June 1997; Also available as NASA
Contractor Report CR-97-206264}
}
@techreport{Owre95:tables,
TITLE = {Analyzing Tabular and State-Transition Specifications
in {PVS}},
AUTHOR = {Sam Owre and John Rushby and Natarajan Shankar},
NUMBER = {SRI-CSL-95-12},
MONTH = jul,
YEAR = 1995,
INSTITUTION = {Computer Science Laboratory, SRI International},
ADDRESS = {Menlo Park, CA},
NOTE = {Available, with specification files, at \url{http://www.csl.sri.com/csl-95-12.html}.
Also published as NASA Contractor Report 201729.}
}
@misc{FORTE97-Tut,
TITLE = {Specification, Proof Checking, and Model Checking for
Protocols and Distributed Systems with {PVS}},
AUTHOR = {John Rushby},
HOWPUBLISHED = {Tutorial presented at {FORTE X/PSTV XVII '97}:
Formal Description Techniques and Protocol Specification,
Testing and Verification},
MONTH = nov,
YEAR = 1997,
INSTITUTION = {Computer Science Laboratory, SRI International},
ADDRESS = {Menlo Park, CA},
NOTE = {Available, with specification files, at \url{http://www.csl.sri.com/forte97.html}}
}
@inproceedings{Rushby00:Movep2k,
TITLE = {Theorem Proving for Verification},
AUTHOR = {John Rushby},
BOOKTITLE = {Modelling and Verification of Parallel Processes:
MoVEP 2k},
EDITOR = {Franck Cassez},
MONTH = jun,
YEAR = 2000,
ADDRESS = {Nantes, France},
NOTE = {Tutorial presented at MoVEP: revised version to be published
by Springer LNCS}
}
@manual{NASA-GB1,
TITLE = {NASA Formal Methods Specification and Verification Guidebook
for Software and Computer Systems, Volume I: Planning
and Technology Insertion},
AUTHOR = {Judith Crow and others},
NUMBER = {NASA-GB-002-95},
YEAR = 1995,
ORGANIZATION = {NASA Office of Safety and Mission Assurance},
ADDRESS = {Washington, DC},
NOTE = {Available at \url{http://eis.jpl.nasa.gov/quality/Formal_Methods/}}
}
@manual{NASA-GB2,
TITLE = {NASA Formal Methods Specification and Verification Guidebook
for Software and Computer Systems, Volume II: A Practitioner's
Companion},
AUTHOR = {Judith Crow and others},
NUMBER = {NASA-GB-001-97},
YEAR = 1997,
ORGANIZATION = {NASA Office of Safety and Mission Assurance},
ADDRESS = {Washington, DC},
NOTE = {Available at \url{http://eis.jpl.nasa.gov/quality/Formal_Methods/}}
}
@inproceedings{Cyrluk&Srivas95:iccd,
TITLE = {Theorem Proving: Not an Esoteric Diversion, but the
Unifying Framework for Industrial Verification},
AUTHOR = {David A. Cyrluk and Mandayam K. Srivas},
BOOKTITLE = {International Conference on Computer Design: {VLSI}
in Computers and Processors ({ICCD} '95)},
PAGES = {538--544},
MONTH = oct,
YEAR = 1995,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Austin, TX}
}
@article{Dill&Rushby96,
TITLE = {Acceptance of Formal Methods: Lessons from Hardware
Design},
AUTHOR = {David L. Dill and John Rushby},
JOURNAL = {IEEE Computer},
PAGES = {23--24},
VOLUME = 29,
NUMBER = 4,
MONTH = apr,
YEAR = 1996,
NOTE = {Part of~\cite{Saiedian96}}
}
@inproceedings{Rushby92:repsa,
TITLE = {Formal Methods for Dependable Real-Time Systems},
AUTHOR = {John Rushby},
BOOKTITLE = {International Symposium on Real-Time Embedded Processing
for Space Applications},
PAGES = {355--366},
MONTH = nov,
YEAR = 1992,
ORGANIZATION = {CNES, the French Space Agency},
ADDRESS = {Les Saintes-Maries-de-la-Mer, France},
NOTE = {Published by C\'{e}padu\`{e}s-\'{E}ditions, Toulouse,
France}
}
@inproceedings{Rushby95:ZUM,
TITLE = {Mechanizing Formal Methods: Opportunities and Challenges},
AUTHOR = {John Rushby},
BOOKTITLE = {{ZUM} '95: The {Z} Formal Specification Notation;
9th International Conference of {Z} Users},
EDITOR = {Jonathan P. Bowen and Michael G. Hinchey},
PAGES = {105--113},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 967,
MONTH = sep,
YEAR = 1995,
ADDRESS = {Limerick, Ireland}
}
@inproceedings{Rushby96:CAV,
TITLE = {Automated Deduction and Formal Methods},
AUTHOR = {John Rushby},
BOOKTITLE = {Computer-Aided Verification, CAV '96},
EDITOR = {Rajeev Alur and Thomas A. Henzinger},
PAGES = {169--183},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1102,
MONTH = {July/August},
YEAR = 1996,
ADDRESS = {New Brunswick, NJ}
}
@inproceedings{Rushby96:FSTTCS,
TITLE = {Mechanized Formal Methods: Progress and Prospects},
AUTHOR = {John Rushby},
BOOKTITLE = {16th Conference on the Foundations of Software Technology
and Theoretical Computer Science},
EDITOR = {V. Chandru and V. Vinay},
PAGES = {43--51},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1180,
MONTH = dec,
YEAR = 1996,
ADDRESS = {Hyderabad, India}
}
@inproceedings{Rushby97:isre,
TITLE = {Calculating with Requirements},
AUTHOR = {John Rushby},
BOOKTITLE = {3rd IEEE International Symposium on Requirements
Engineering},
PAGES = {144--146},
MONTH = jan,
YEAR = 1997,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Annapolis, MD}
}
@inproceedings{Rushby:FM99,
TITLE = {Mechanized Formal Methods: Where Next?},
AUTHOR = {John Rushby},
BOOKTITLE = {FM99: The World Congress in Formal Methods},
EDITOR = {Jeannette Wing and Jim Woodcock},
PAGES = {48--51},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1708 and 1709},
MONTH = sep,
YEAR = 1999,
ADDRESS = {Toulouse, France},
NOTE = {Pages 1--938 are in the first volume, 939--1872 in the
second.}
}
@article{Shankar85,
TITLE = {Towards Mechanical Metamathematics},
AUTHOR = {N. Shankar},
JOURNAL = {Journal of Automated Reasoning},
PAGES = {407--434},
VOLUME = 1,
NUMBER = 4,
YEAR = 1985
}
@article{Shankar:notes,
TITLE = {Observations on the Use of Computers in Proof Checking},
AUTHOR = {N. Shankar},
JOURNAL = {Notices of the American Mathematical Society},
PAGES = {804--805},
VOLUME = 35,
NUMBER = 6,
MONTH = {July/August},
YEAR = 1988
}
@book{Shankar:book,
TITLE = {Metamathematics, Machines, and {G{\"o}del's} Proof},
AUTHOR = {N. Shankar},
PUBLISHER = {Cambridge University Press},
SERIES = {Cambridge Tracts in Theoretical Computer Science},
YEAR = 1994,
ADDRESS = {Cambridge, UK}
}
@inproceedings{Shankar:FTRTFT96,
TITLE = {Unifying Verification Paradigms},
AUTHOR = {Natarajan Shankar},
BOOKTITLE = {Formal Techniques in Real-Time and Fault-Tolerant
Systems},
EDITOR = {Bengt Jonsson and Joachim Parrow},
PAGES = {22--39},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1135,
MONTH = sep,
YEAR = 1996,
ADDRESS = {Uppsala, Sweden}
}
@techreport{Rushby:FAA-full,
TITLE = {Formal Methods and the Certification of Critical Systems},
AUTHOR = {John Rushby},
NUMBER = {SRI-CSL-93-7},
MONTH = dec,
YEAR = 1993,
INSTITUTION = {Computer Science Laboratory, SRI International},
ADDRESS = {Menlo Park, CA},
NOTE = {Also issued under the title {\em Formal Methods and Digital
Systems Validation for Airborne Systems\/} as NASA Contractor
Report 4551, December 1993. A book based on this material
will be published by Cambridge University Press in 1998/9}
}
@article{Rushby94:Taxonomy,
TITLE = {Critical System Properties: Survey and Taxonomy},
AUTHOR = {John Rushby},
JOURNAL = {Reliability Engineering and System Safety},
PAGES = {189--219},
VOLUME = 43,
NUMBER = 2,
YEAR = 1994
}
@techreport{Rushby:FAA-short,
TITLE = {Formal Methods and their Role in the Certification of
Critical Systems},
AUTHOR = {John Rushby},
NUMBER = {SRI-CSL-95-1},
MONTH = mar,
YEAR = 1995,
INSTITUTION = {Computer Science Laboratory, SRI International},
ADDRESS = {Menlo Park, CA},
NOTE = {Also available as NASA Contractor Report 4673, August
1995, and issued as part of the {\em FAA Digital Systems
Validation Handbook} (the guide for aircraft certification).
Reprinted in~\cite[pp.~1--42]{Encress95}}
}
@incollection{Srivas97:chapter,
TITLE = {Hardware Verification Using {PVS}},
AUTHOR = {Mandayam Srivas and Harald Rue{\ss} and David Cyrluk},
BOOKTITLE = {Formal Hardware Verification: Methods and Systems
in Comparison},
EDITOR = {Thomas Kropf},
PAGES = {156--205},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1287,
YEAR = 1997
}
@inproceedings{Cyrluk96:DP,
TITLE = {On {Shostak's} Decision Procedure for Combinations of
Theories},
AUTHOR = {David Cyrluk and Patrick Lincoln and N. Shankar},
BOOKTITLE = {Automated Deduction---{CADE-13}},
EDITOR = {M. A. McRobbie and J. K. Slaney},
PAGES = {463--477},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = 1104,
MONTH = {July/August},
YEAR = 1996,
ADDRESS = {New Brunswick, NJ}
}
@inproceedings{Cyrluk-etal97:CAV,
TITLE = {An Efficient Decision Procedure for the Theory of Fixed-Sized
Bit-Vectors},
AUTHOR = {David Cyrluk and Harald Rue{\ss} and Oliver M{\"o}ller},
BOOKTITLE = {Computer-Aided Verification, CAV '97},
EDITOR = {Orna Grumberg},
PAGES = {60--71},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1254,
MONTH = jun,
YEAR = 1997,
ADDRESS = {Haifa, Israel}
}
@inproceedings{Cyrluk94:gtl,
TITLE = {Ground Temporal Logic---A Logic for Hardware Verification},
AUTHOR = {D. Cyrluk and P. Narendran},
BOOKTITLE = {Computer-Aided Verification, CAV '94},
EDITOR = {David Dill},
PAGES = {247--259},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 818,
MONTH = jun,
YEAR = 1994,
ADDRESS = {Stanford, CA}
}
@inproceedings{Cyrluk94:TPCD,
TITLE = {Effective Theorem Proving for Hardware Verification},
AUTHOR = {D. Cyrluk and S. Rajan and N. Shankar and M. K. Srivas},
BOOKTITLE = {Theorem Provers in Circuit Design ({TPCD} '94)},
EDITOR = {Ramayya Kumar and Thomas Kropf},
PAGES = {203--222},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 910,
MONTH = sep,
YEAR = 1994,
ADDRESS = {Bad Herrenalb, Germany}
}
@inproceedings{Moeller98:FMCAD,
TITLE = {Solving Bit-Vector Equations},
AUTHOR = {Oliver M{\"o}ller and Harald Rue{\ss}},
BOOKTITLE = {Formal Methods in Computer-Aided Design (FMCAD '98)},
EDITOR = {Ganesh Gopalakrishnan and Phillip Windley},
PAGES = {36--48},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1522,
MONTH = nov,
YEAR = 1998,
ADDRESS = {Palo Alto, CA}
}
@inproceedings{Tiwari-etal00:CADE,
TITLE = {Rigid E-Unification Revisited},
AUTHOR = {Ashish Tiwari and Leo Bachmair and Harald Rue{\ss}},
BOOKTITLE = {Automated Deduction---{CADE-17}},
EDITOR = {David McAllester},
PAGES = {220--234},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = 1831,
MONTH = jun,
YEAR = 2000,
ADDRESS = {Pittsburgh, PA}
}
@inproceedings{Rajan95:CAV,
TITLE = {An Integration of Model-Checking with Automated Proof
Checking},
AUTHOR = {S. Rajan and N. Shankar and M.K. Srivas},
BOOKTITLE = {Computer-Aided Verification, CAV '95},
EDITOR = {Pierre Wolper},
PAGES = {84--97},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 939,
MONTH = jun,
YEAR = 1995,
ADDRESS = {Liege, Belgium}
}
@inproceedings{pvs-tables:tacas97,
TITLE = {Integration in {PVS}: Tables, Types, and Model Checking},
AUTHOR = {Sam Owre and John Rushby and N. Shankar},
BOOKTITLE = {Tools and Algorithms for the Construction and Analysis
of Systems {(TACAS '97)}},
EDITOR = {Ed Brinksma},
PAGES = {366-383},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1217,
MONTH = apr,
YEAR = 1997,
ADDRESS = {Enschede, The Netherlands}
}
@inproceedings{Owre&Ruess00:CAV,
TITLE = {Integrating {WS1S} with {PVS}},
AUTHOR = {Sam Owre and Harald Rue{\ss}},
BOOKTITLE = {Computer-Aided Verification, CAV '2000},
EDITOR = {E. A. Emerson and A. P. Sistla},
PAGES = {548--551},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1855,
MONTH = jul,
YEAR = 2000,
ADDRESS = {Chicago, IL}
}
@inproceedings{Pfab98:tools,
TITLE = {Towards Light-Weight Verification and Heavy-Weight Testing},
AUTHOR = {Friedrich von Henke and Stephan Pfab and Harald Rue{\ss}
and Sam Owre},
BOOKTITLE = {Tool Support for System Specification, Development,
and Verification},
EDITOR = {Rudolph Berghammer and Yassine Lakhnech},
PAGES = {189--200},
PUBLISHER = {Springer-Verlag},
SERIES = {Advances in Computing Science},
MONTH = jun,
YEAR = 1998,
ADDRESS = {Malente, Germany},
NOTE = {Proceedings published in May 1999}
}
@inproceedings{vonHenke98:tphols,
TITLE = {Case Studies in Meta-Level Theorem Proving},
AUTHOR = {Friedrich von Henke and Stephan Pfab and Holger Pfeifer
and Harald Rue{\ss}},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 11th International
Conference, {TPHOLs '98}},
EDITOR = {Jim Grundy and Malcolm Newey},
PAGES = {461--478},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1479,
MONTH = sep,
YEAR = 1998,
ADDRESS = {Canberra, Australia}
}
@techreport{shankar99:eval,
TITLE = {Efficiently Executing {PVS}},
AUTHOR = {N. Shankar},
TYPE = {Project report},
MONTH = nov,
YEAR = 1999,
INSTITUTION = {Computer Science Laboratory, SRI International},
ADDRESS = {Menlo Park, CA},
NOTE = {Available at \url{http://www.csl.sri.com/shankar/PVSeval.ps.gz}}
}
@inproceedings{Bensalem96:CAV,
TITLE = {Powerful Techniques for the Automatic Generation of
Invariants},
AUTHOR = {Saddek Bensalem and Yassine Lakhnech and Hassen Sa{\"\i}di},
BOOKTITLE = {Computer-Aided Verification, CAV '96},
EDITOR = {Rajeev Alur and Thomas A. Henzinger},
PAGES = {323--335},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1102,
MONTH = {July/August},
YEAR = 1996,
ADDRESS = {New Brunswick, NJ}
}
@inproceedings{Bensalem98:CAV,
TITLE = {Computing Abstractions of Infinite State Systems Compositionally
and Automatically},
AUTHOR = {Saddek Bensalem and Yassine Lakhnech and Sam Owre},
BOOKTITLE = {Computer-Aided Verification, CAV '98},
EDITOR = {Alan J. Hu and Moshe Y. Vardi},
PAGES = {319--331},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1427,
MONTH = jun,
YEAR = 1998,
ADDRESS = {Vancouver, Canada}
}
@inproceedings{Abdulla:CAV99,
TITLE = {Verification of Infinite-State Systems by Combining
Abstraction and Reachability Analysis},
AUTHOR = {Parosh Aziz Abdulla and Aurore Annichini and Saddek
Bensalem and Ahmed Bouajjani and Peter Habermehl and
Yassine Lakhnech},
BOOKTITLE = {Computer-Aided Verification, CAV '99},
EDITOR = {Nicolas Halbwachs and Doron Peled},
PAGES = {146--159},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1633,
MONTH = jul,
YEAR = 1999,
ADDRESS = {Trento, Italy}
}
@inproceedings{Rusu&Singerman99,
TITLE = {On Proving Safety Properties by Integrating Static Analysis,
Theorem Proving and Abstraction},
AUTHOR = {Vlad Rusu and Eli Singerman},
BOOKTITLE = {Tools and Algorithms for the Construction and Analysis
of Systems {(TACAS '99)}},
EDITOR = {W. Rance Cleaveland},
PAGES = {178--192},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1579,
MONTH = mar,
YEAR = 1999,
ADDRESS = {Amsterdam, The Netherlands}
}
@inproceedings{Graf96:CAV,
TITLE = {Verifying Invariants Using Theorem Proving},
AUTHOR = {Susanne Graf and Hassen Sa{\"\i}di},
BOOKTITLE = {Computer-Aided Verification, CAV '96},
EDITOR = {Rajeev Alur and Thomas A. Henzinger},
PAGES = {196--207},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1102,
MONTH = {July/August},
YEAR = 1996,
ADDRESS = {New Brunswick, NJ}
}
@inproceedings{Saidi96,
TITLE = {A Tool for Proving Invariance Properties of Concurrent
Systems Automatically},
AUTHOR = {Hassen Sa{\"\i}di},
BOOKTITLE = {Tools and Algorithms for the Construction and Analysis
of Systems {TACAS '96}},
PAGES = {412--416},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1055,
MONTH = mar,
YEAR = 1996,
ADDRESS = {Passau, Germany}
}
@inproceedings{Saidi97:CAV,
TITLE = {{The Invariant Checker}: Automated Deductive Verification
of Reactive Systems},
AUTHOR = {Hassen Sa{\"\i}di},
BOOKTITLE = {Computer-Aided Verification, CAV '97},
EDITOR = {Orna Grumberg},
PAGES = {436--439},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1254,
MONTH = jun,
YEAR = 1997,
ADDRESS = {Haifa, Israel}
}
@inproceedings{Saidi&Graf97:CAV,
TITLE = {Construction of Abstract State Graphs with {PVS}},
AUTHOR = {Hassen Sa{\"\i}di and Susanne Graf},
BOOKTITLE = {Computer-Aided Verification, CAV '97},
EDITOR = {Orna Grumberg},
PAGES = {72--83},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1254,
MONTH = jun,
YEAR = 1997,
ADDRESS = {Haifa, Israel}
}
@inproceedings{Saidi97:LFM,
TITLE = {Automated Deductive Verification of Parallel Systems},
AUTHOR = {Hassen Sa{\"\i}di},
BOOKTITLE = {LFM' 97: Fourth NASA Langley Formal Methods Workshop},
EDITOR = {C. Michael Holloway and Kelly J. Hayhurst},
PAGES = {163--176},
SERIES = {NASA Conference Publication 3356},
MONTH = sep,
YEAR = 1997,
ORGANIZATION = {NASA Langley Research Center},
ADDRESS = {Hampton, VA},
NOTE = {Available at \url{http://atb-www.larc.nasa.gov/Lfm97/proceedings/}}
}
@inproceedings{Saidi&Shankar:CAV99,
TITLE = {Abstract and Model Check While You Prove},
AUTHOR = {Hassen Sa{\"\i}di and N. Shankar},
BOOKTITLE = {Computer-Aided Verification, CAV '99},
EDITOR = {Nicolas Halbwachs and Doron Peled},
PAGES = {443--454},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1633,
MONTH = jul,
YEAR = 1999,
ADDRESS = {Trento, Italy}
}
@inproceedings{Saidi00:SAS,
TITLE = {Model Checking Guided Abstraction and Analysis},
AUTHOR = {Hassen Sa\"{\i}di},
BOOKTITLE = {Seventh International Static Analysis Symposium
{(SAS'00)}},
EDITOR = {Jens Palsberg},
PAGES = {377--396},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1824,
MONTH = jun,
YEAR = 2000,
ADDRESS = {Santa Barbara CA}
}
@inproceedings{Shankar00:ASM,
TITLE = {Symbolic Analysis of Transition Systems},
AUTHOR = {Natarajan Shankar},
BOOKTITLE = {Abstract State Machines: Theory and Applications
({ASM} 2000)},
EDITOR = {Yuri Gurevich and Phillip W. Kutter and Martin Odersky
and Lothar Thiele},
PAGES = {287--302},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
NUMBER = 1912,
MONTH = mar,
YEAR = 2000,
ADDRESS = {Monte Verit\`{a}, Switzerland}
}
@inproceedings{Shankar00:CONCUR,
TITLE = {Combining Theorem Proving and Model Checking through
Symbolic Analysis},
AUTHOR = {Natarajan Shankar},
BOOKTITLE = {{CONCUR 2000}: Concurrency Theory},
PAGES = {1--16},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
NUMBER = 1877,
MONTH = aug,
YEAR = 2000,
ADDRESS = {State College, PA}
}
@inproceedings{Bensalem98:InVeSt,
TITLE = {{InVeSt: A} Tool for the Verification of Invariants},
AUTHOR = {Saddek Bensalem and Yassine Lakhnech and Sam Owre},
BOOKTITLE = {Computer-Aided Verification, CAV '98},
EDITOR = {Alan J. Hu and Moshe Y. Vardi},
PAGES = {505--510},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1427,
MONTH = jun,
YEAR = 1998,
ADDRESS = {Vancouver, Canada}
}
@inproceedings{SALoverview00:LFM,
TITLE = {An Overview of {SAL}},
AUTHOR = {Saddek Bensalem and Vijay Ganesh and Yassine Lakhnech
and C\'{e}sar Mu{\~{n}}oz and Sam Owre and Harald Rue{\ss}
and John Rushby and Vlad Rusu and Hassen Sa{\"\i}di and
N. Shankar and Eli Singerman and Ashish Tiwari},
BOOKTITLE = {LFM 2000: Fifth NASA Langley Formal Methods Workshop},
EDITOR = {C. Michael Holloway},
PAGES = {187--196},
MONTH = jun,
YEAR = 2000,
ORGANIZATION = {NASA Langley Research Center},
ADDRESS = {Hampton, VA},
NOTE = {Proceedings available at \url{http://shemesh.larc.nasa.gov/fm/Lfm2000/Proc/}}
}
@inproceedings{Rushby98:ICFEM,
TITLE = {Ubiquitous Abstraction: A New Approach for Mechanized
Formal Verification (Extended Abstract)},
AUTHOR = {John Rushby},
BOOKTITLE = {Second International Conference on Formal Engineering
Methods (ICFEM '98)},
EDITOR = {John Staples and Michael G. Hinchey and Shaoying Liu},
PAGES = {176--178},
MONTH = dec,
YEAR = 1998,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Brisbane, Australia}
}
@inproceedings{Rushby:SPIN99,
TITLE = {Integrated Formal Verification: Using Model Checking
With Automated Abstraction, Invariant Generation, and
Theorem Proving},
AUTHOR = {John Rushby},
BOOKTITLE = {Theoretical and Practical Aspects of SPIN Model
Checking: 5th and 6th International SPIN Workshops},
EDITOR = {D. Dams and R. Gerth and S. Leue and M. Massink},
PAGES = {1--11},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1680,
MONTH = {July and September},
YEAR = 1999,
ADDRESS = {Trento, Italy, and Toulouse, France}
}
@inproceedings{Rushby00:Forte,
TITLE = {From Refutation to Verification},
AUTHOR = {John Rushby},
BOOKTITLE = {Formal Description Techniques and Protocol Specification,
Testing and Verification {FORTE XIII/PSTV XX 2000}},
EDITOR = {Tommaso Bolognesi and Diego Latella},
PAGES = {369--374},
PUBLISHER = {Kluwer Academic Publishers},
MONTH = oct,
YEAR = 2000,
ADDRESS = {Pisa, Italy}
}
@inproceedings{Rushby00:HASE,
TITLE = {Disappearing Formal Methods},
AUTHOR = {John Rushby},
BOOKTITLE = {High-Assurance Systems Engineering Symposium},
PAGES = {95--96},
MONTH = nov,
YEAR = 2000,
ORGANIZATION = {Association for Computing Machinery},
ADDRESS = {Albuquerque, NM}
}
@article{Young97:IC,
TITLE = {Comparing Verification Systems: {Interactive Consistency}
in {ACL2}},
AUTHOR = {William D. Young},
JOURNAL = {IEEE Transactions on Software Engineering},
PAGES = {214--223},
VOLUME = 23,
NUMBER = 4,
MONTH = apr,
YEAR = 1997
}
@inproceedings{Miner95:HOL,
TITLE = {Specification of the {IEEE-854} Floating-Point Standard
in {HOL} and {PVS}},
AUTHOR = {Victor A. {Carre{\~{n}}o} and Paul S. Miner},
BOOKTITLE = {{HOL95}: Eighth International Workshop on Higher-Order
Logic Theorem Proving and Its Applications},
MONTH = sep,
YEAR = 1995,
ADDRESS = {Aspen Grove, UT},
NOTE = {Category B proceedings, available at \url{http://lal.cs.byu.edu/lal/hol95/Bprocs/indexB.html}}
}
@misc{Gordon95:PVS,
TITLE = {Notes on {PVS} from a {HOL} Perspective},
AUTHOR = {Mike Gordon},
HOWPUBLISHED = {Available at \url{http://www.cl.cam.ac.uk/users/mjcg/PVS.html}},
MONTH = aug,
YEAR = 1995,
INSTITUTION = {Cambridge University}
}
@inproceedings{Griffioen98:tphols,
TITLE = {A Comparison of {PVS} and {Isabelle/HOL}},
AUTHOR = {David Griffioen and Marieke Huisman},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 11th International
Conference, {TPHOLs '98}},
EDITOR = {Jim Grundy and Malcolm Newey},
PAGES = {123--142},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1479,
MONTH = sep,
YEAR = 1998,
ADDRESS = {Canberra, Australia}
}
@inproceedings{Groote-etal98:CONCUR,
TITLE = {Checking Verifications of Protocols and Distributed
Systems by Computer},
AUTHOR = {Jan Friso Groote and Fran\,{c}ois Monin and Jaco van
de Pol},
BOOKTITLE = {{CONCUR'98}: Concurrency Theory},
EDITOR = {Davide Sangiorgi and Robert de Simone},
PAGES = {629--655},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1466,
MONTH = sep,
YEAR = 1998,
ADDRESS = {Nice, France}
}
@article{Kern99:todaes,
TITLE = {Formal Verification in Hardware Design: A Survey},
AUTHOR = {Christoph Kern and Mark R. Greenstreet},
JOURNAL = {ACM Transactions on Design Automation of Electronic
Systems (TODAES)},
PAGES = {123--193},
VOLUME = 4,
NUMBER = 2,
MONTH = apr,
YEAR = 1999
}
@inproceedings{Rust98,
TITLE = {A {PVS} Specification of an Invoicing System},
AUTHOR = {Heinrich Rust},
BOOKTITLE = {Proceedings of an International Workshop on Specification
Techniques and Formal Methods},
EDITOR = {M. Allemand and C. Attiogb\'{e} and H. Habrias},
PAGES = {51--65},
MONTH = mar,
YEAR = 1998,
ORGANIZATION = {University of Nantes, France},
NOTE = {Available at \url{http://www.informatik.tu-cottbus.de/~rust/publications/a_pvs_specificat%
ion_of_an_invoicing_system.ps.gz}}
}
@inproceedings{Wilding97:LFM,
TITLE = {Robust Computer System Proofs in {PVS}},
AUTHOR = {Matthew Wilding},
BOOKTITLE = {LFM' 97: Fourth NASA Langley Formal Methods Workshop},
EDITOR = {C. Michael Holloway and Kelly J. Hayhurst},
PAGES = {177--184},
SERIES = {NASA Conference Publication 3356},
MONTH = sep,
YEAR = 1997,
ORGANIZATION = {NASA Langley Research Center},
ADDRESS = {Hampton, VA},
NOTE = {Available at \url{http://atb-www.larc.nasa.gov/Lfm97/proceedings/}}
}
@inproceedings{Droschl:IFMW99,
TITLE = {On the Integration of Formal Methods: Events and Scenarios
in {PVS} and {VDM}},
AUTHOR = {Georg Droschl},
BOOKTITLE = {Proceedings, 3rd. Irish Workshop in Formal Methods},
PUBLISHER = {Electronic Workshops in Computing (\url{http://ewic.org.uk/ewic/})},
MONTH = jul,
YEAR = 1999,
ADDRESS = {Galway, Ireland}
}
@inproceedings{Droschl:FM99,
TITLE = {Analyzing the Requirements of an Access Control Using
{VDMTools} and {PVS}},
AUTHOR = {Georg Droschl},
BOOKTITLE = {FM99: The World Congress in Formal Methods},
EDITOR = {Jeannette Wing and Jim Woodcock},
PAGES = 1807,
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1708 and 1709},
MONTH = sep,
YEAR = 1999,
ADDRESS = {Toulouse, France},
NOTE = {Pages 1--938 are in the first volume, 939--1872 in the
second.}
}
@inproceedings{Merriam96,
TITLE = {Evaluating the Interfaces of Three Theorem Proving Assistants},
AUTHOR = {Nicholas A. Merriam and Michael D. Harrison},
BOOKTITLE = {Proceedings of the 3rd International {Eurographics}
Workshop on Design, Specification, and Verification of
Interactive Systems},
EDITOR = {F. Bodart and J. Vanderdonckt},
YEAR = 1996
}
@inproceedings{Archer&Heitmeyer97:TPHOLS,
TITLE = {Human-Style Theorem Proving Using {PVS}},
AUTHOR = {Myla Archer and Constance Heitmeyer},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 10th International
Conference, {TPHOLs '97}},
EDITOR = {Elsa Gunter and Amy Felty},
PAGES = {33--48},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1275,
MONTH = aug,
YEAR = 1997,
ADDRESS = {Murray Hill, NJ}
}
@inproceedings{Archer98:UITP,
TITLE = {{TAME: A PVS} Interface to Simplify Proofs for Automata
Models},
AUTHOR = {Myla Archer and Constance Heitmeyer and Steve Sims},
BOOKTITLE = {User Interfaces for Theorem Provers},
MONTH = jul,
YEAR = 1998,
ADDRESS = {Eindhoven, The Netherlands},
NOTE = {Informal proceedings available at \url{http://www.win.tue.nl/cs/ipa/uitp/proceedings.html}}
}
@inproceedings{Knight97:LFM,
TITLE = {Why Are Formal Methods Not Used More Widely?},
AUTHOR = {John Knight and Colleen DeJong and Matthew Gibble and
Lu{\'\i}s Nakano},
BOOKTITLE = {LFM' 97: Fourth NASA Langley Formal Methods Workshop},
EDITOR = {C. Michael Holloway and Kelly J. Hayhurst},
PAGES = {1--12},
SERIES = {NASA Conference Publication 3356},
MONTH = sep,
YEAR = 1997,
ORGANIZATION = {NASA Langley Research Center},
ADDRESS = {Hampton, VA},
NOTE = {Available at \url{http://atb-www.larc.nasa.gov/Lfm97/proceedings/}}
}
@inproceedings{Dutertre96,
TITLE = {Elements of Mathematical Analysis in {PVS}},
AUTHOR = {Bruno Dutertre},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 9th International
Conference, {TPHOLs '96}},
EDITOR = {Joakim von Wright and Jim Grundy and John Harrison},
PAGES = {141--156},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1125,
MONTH = aug,
YEAR = 1996,
ADDRESS = {Turku, Finland}
}
@inproceedings{Gottliebsen00:TPHOLS,
TITLE = {Transcendental Functions and Continuity Checking in
{PVS}},
AUTHOR = {Hanne Gottliebsen},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 13th International
Conference, {TPHOLs 2000}},
EDITOR = {Mark Aargaard and John Harrison},
PAGES = {197--214},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1869,
MONTH = aug,
YEAR = 2000,
ADDRESS = {Portland, OR}
}
@inproceedings{Basten&Hooman99,
TITLE = {Process Algebra in {PVS}},
AUTHOR = {Twan Basten and Jozef Hooman},
BOOKTITLE = {Tools and Algorithms for the Construction and Analysis
of Systems {(TACAS '99)}},
EDITOR = {W. Rance Cleaveland},
PAGES = {270--284},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1579,
MONTH = mar,
YEAR = 1999,
ADDRESS = {Amsterdam, The Netherlands}
}
@inproceedings{Schamschurko98,
TITLE = {Modeling Process Calculi With {PVS}},
AUTHOR = {Dmitri Schamschurko},
BOOKTITLE = {First Workshop on Coalgebraic Methods in Computer
Science {(CMCS'98)}},
EDITOR = {B. Jacobs and L. Moss and H. Reichel and J. Rutten},
PAGES = {197--214},
PUBLISHER = {Elsevier},
SERIES = {Electronic Notes in Theoretical Computer Science},
VOLUME = 11,
MONTH = mar,
YEAR = 1998,
ADDRESS = {Lisbon, Portugal},
NOTE = {Available at \url{http://www.elsevier.nl/cas/tree/store/tcs/free/entcs/store/tcs11/tcs110%
11.ps}}
}
@inproceedings{Griffioen98:CAV,
TITLE = {Normed Simulations},
AUTHOR = {David Griffioen and Frits Vaandrager},
BOOKTITLE = {Computer-Aided Verification, CAV '98},
EDITOR = {Alan J. Hu and Moshe Y. Vardi},
PAGES = {332--344},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1427,
MONTH = jun,
YEAR = 1998,
ADDRESS = {Vancouver, Canada}
}
@inproceedings{Pnueli98:FTRTFT,
TITLE = {Fair Synchronous Transition Systems and their Liveness
Proofs},
AUTHOR = {Amir Pnueli and N. Shankar and Eli Singerman},
BOOKTITLE = {Formal Techniques in Real-Time and Fault-Tolerant
Systems},
PAGES = {198--209},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1486,
MONTH = sep,
YEAR = 1998,
ADDRESS = {Lyngby, Denmark}
}
@inproceedings{Devillers-etal97,
TITLE = {Possibly Infinite Sequences in Theorem Provers: A Comparative
Study},
AUTHOR = {M. Devillers and D. Griffioen and O. Mueller},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 10th International
Conference, {TPHOLs '97}},
EDITOR = {Elsa Gunter and Amy Felty},
PAGES = {89--104},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1275,
MONTH = aug,
YEAR = 1997,
ADDRESS = {Murray Hill, NJ}
}
@inproceedings{Hensel&Jacobs97,
TITLE = {Proof Principles for Datatypes with Iterated Recursion},
AUTHOR = {Ulrich Hensel and Bart Jacobs},
BOOKTITLE = {Category Theory and Computer Science},
EDITOR = {Eugenio Moggi and Giuseppe Rosolini},
PAGES = {220--241},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1290,
MONTH = sep,
YEAR = 1997,
ADDRESS = {Santa Margherita Ligure, Italy}
}
@article{Hensel98:JLC,
TITLE = {Coalgebraic Theories of Sequences in {PVS}},
AUTHOR = {Ulrich Hensel and Bart Jacobs},
JOURNAL = {Journal of Logic and Computation},
PAGES = {463--500},
VOLUME = 9,
NUMBER = 4,
YEAR = 1999
}
@inproceedings{Hensel-etal98,
TITLE = {Reasoning About Classes in Object-Oriented Languages:
Logical Models and Tools},
AUTHOR = {Ulrich Hensel and Marieke Huisman and Bart Jacobs and
Hendrik Tews},
BOOKTITLE = {Programming Languages and Systems: 7th European
Symposium On Programming {(ESOP)}},
EDITOR = {Chris Hankin},
PAGES = {105--121},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1381,
MONTH = mar,
YEAR = 1998,
ADDRESS = {Lisbon, Portugal}
}
@inproceedings{Huisman-etal99:ECOOP,
TITLE = {A Case Study in Class Library Verification: {Java's}
Vector Class},
AUTHOR = {Marieke Huisman and Bart Jacobs and Joachim van den
Berg},
BOOKTITLE = {Object-Oriented Technology: ECOOP'99 Workshop Reader},
EDITOR = {A. Moreira and D. Demeyer},
PAGES = {109---110},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1743,
MONTH = jun,
YEAR = 1999,
ADDRESS = {Lisbon, Portugal}
}
@inproceedings{Jacobs98:OOPSLA,
TITLE = {Reasoning about {Java} Classes},
AUTHOR = {Bart Jacobs and Joachim van den Berg and Marieke Huisman
and Martijn van Berkum and Ulrich Hensel and Hendrick
Tews},
BOOKTITLE = {Proceedings, Object-Oriented Programming Systems,
Languages and Applications (OOPSLA'98)},
PAGES = {329--340},
MONTH = oct,
YEAR = 1998,
ORGANIZATION = {Association for Computing Machinery},
ADDRESS = {Vancouver, Canada},
NOTE = {Proceedings issued as ACM SIGPLAN Notices Vol.~33, No.~10,
October 1998.}
}
@inproceedings{Huisman&Jacobs00:TPHOLS,
TITLE = {Inheritance in Higher Order Logic: Modeling and Reasoning},
AUTHOR = {Marieke Huisman and Bart Jacobs},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 13th International
Conference, {TPHOLs 2000}},
EDITOR = {Mark Aargaard and John Harrison},
PAGES = {301--319},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1869,
MONTH = aug,
YEAR = 2000,
ADDRESS = {Portland, OR}
}
@phdthesis{Huisman:PhD,
TITLE = {Java Program Verification in {Higher}-Order Logic with
{PVS} and {Isabelle}},
AUTHOR = {Marieke Huisman},
YEAR = 2001,
SCHOOL = {University of Nijmegen, The Netherlands}
}
@inproceedings{Huisman&Jacobs00:FASE,
TITLE = {Java Program Verfication via a Hoare Logic with Abrupt
Termination},
AUTHOR = {Marieke Huisman and Bart Jacobs},
BOOKTITLE = {Fundamental Approaches to Software Engineering,
{FASE} 2000},
EDITOR = {Tom Maibaum},
PAGES = {284--303},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
NUMBER = 1783,
MONTH = {March/April},
YEAR = 2000,
ADDRESS = {Berlin, Germany}
}
@inproceedings{vandenBerg-etal00:WADT,
TITLE = {A Type-Theoretic Memory Model for Verification of Sequential
{Java} Programs},
AUTHOR = {Joachim van den Berg and Marieke Huisman and Bart Jacobs
and Erik Poll},
BOOKTITLE = {Recent Trends in Algebraic Development Techniques,
{WADT '99}},
EDITOR = {Didier Bert and Christine Choppy and Peter Mosses},
PAGES = {1--21},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
NUMBER = 1827,
MONTH = sep,
YEAR = 1999,
ADDRESS = {Toulouse, France}
}
@inproceedings{Lincoln&Rushby93:CAV,
TITLE = {Formal Verification of an Algorithm for Interactive
Consistency under a Hybrid Fault Model},
AUTHOR = {Patrick Lincoln and John Rushby},
BOOKTITLE = {Computer-Aided Verification, CAV '93},
EDITOR = {Costas Courcoubetis},
PAGES = {292--304},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 697,
MONTH = {June/July},
YEAR = 1993,
ADDRESS = {Elounda, Greece}
}
@inproceedings{Lincoln&Rushby93:FTCS,
TITLE = {A Formally Verified Algorithm for Interactive Consistency
under a Hybrid Fault Model},
AUTHOR = {Patrick Lincoln and John Rushby},
BOOKTITLE = {Fault Tolerant Computing Symposium 23},
PAGES = {402--411},
MONTH = jun,
YEAR = 1993,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Toulouse, France},
NOTE = {Reprinted in~\cite[pp.\ 438--447]{FTCS-highlights}}
}
@inproceedings{Lincoln&Rushby94:FTP,
TITLE = {Formal Verification of an Interactive Consistency Algorithm
for the {Draper FTP} Architecture Under a Hybrid Fault
Model},
AUTHOR = {Patrick Lincoln and John Rushby},
BOOKTITLE = {COMPASS '94 (Proceedings of the Ninth Annual Conference
on Computer Assurance)},
PAGES = {107--120},
MONTH = jun,
YEAR = 1994,
ORGANIZATION = {IEEE Washington Section},
ADDRESS = {Gaithersburg, MD}
}
@inproceedings{Pfeifer99:DCCA,
TITLE = {Formal Verification for Time-Triggered Clock Synchronization},
AUTHOR = {Holger Pfeifer and Detlef Schwier and Friedrich W.
von Henke},
BOOKTITLE = {Dependable Computing for Critical Applications---7},
EDITOR = {Charles B. Weinstock and John Rushby},
PAGES = {207--226},
PUBLISHER = {IEEE Computer Society},
SERIES = {Dependable Computing and Fault Tolerant Systems},
VOLUME = 12,
MONTH = jan,
YEAR = 1999,
ADDRESS = {San Jose, CA}
}
@inproceedings{Pfeifer00:FORTE,
TITLE = {Formal Verification of the {TTA} Group Membership Algorithm},
AUTHOR = {Holger Pfeifer},
BOOKTITLE = {Formal Description Techniques and Protocol Specification,
Testing and Verification {FORTE XIII/PSTV XX 2000}},
EDITOR = {Tommaso Bolognesi and Diego Latella},
PAGES = {3--18},
PUBLISHER = {Kluwer Academic Publishers},
MONTH = oct,
YEAR = 2000,
ADDRESS = {Pisa, Italy}
}
@article{Rushby99:TSE,
TITLE = {Systematic Formal Verification for Fault-Tolerant Time-Triggered
Algorithms},
AUTHOR = {John Rushby},
JOURNAL = {IEEE Transactions on Software Engineering},
PAGES = {651--660},
VOLUME = 25,
NUMBER = 5,
MONTH = {September/October},
YEAR = 1999
}
@inproceedings{Rushby00:CAV,
TITLE = {Verification Diagrams Revisited: Disjunctive Invariants
for Easy Verification},
AUTHOR = {John Rushby},
BOOKTITLE = {Computer-Aided Verification, CAV '2000},
EDITOR = {E. A. Emerson and A. P. Sistla},
PAGES = {508--520},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1855,
MONTH = jul,
YEAR = 2000,
ADDRESS = {Chicago, IL}
}
@inproceedings{Schwier98:FTRTFT,
TITLE = {Mechanical Verification of Clock Synchronization Algorithms},
AUTHOR = {D. Schwier and F. von Henke},
BOOKTITLE = {Formal Techniques in Real-Time and Fault-Tolerant
Systems},
PAGES = {262--271},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1486,
MONTH = sep,
YEAR = 1998,
ADDRESS = {Lyngby, Denmark}
}
@article{WalterLincolnSuri97,
TITLE = {Formally Verified On-Line Diagnosis},
AUTHOR = {Chris J. Walter and Patrick Lincoln and Neeraj Suri},
JOURNAL = {IEEE Transactions on Software Engineering},
PAGES = {684--721},
VOLUME = 23,
NUMBER = 11,
MONTH = nov,
YEAR = 1997
}
@techreport{DiVito:partitioningCR,
TITLE = {A Formal Model of Partitioning for Integrated Modular
Avionics},
AUTHOR = {Ben L. {Di Vito}},
TYPE = {NASA Contractor Report},
NUMBER = {CR-1998-208703},
MONTH = aug,
YEAR = 1998,
INSTITUTION = {NASA Langley Research Center}
}
@inproceedings{diVito99:DCCA,
TITLE = {A Model of Cooperative Noninterference for Integrated
Modular Avionics},
AUTHOR = {Ben L. {Di Vito}},
BOOKTITLE = {Dependable Computing for Critical Applications---7},
EDITOR = {Charles B. Weinstock and John Rushby},
PAGES = {269--286},
PUBLISHER = {IEEE Computer Society},
SERIES = {Dependable Computing and Fault Tolerant Systems},
VOLUME = 12,
MONTH = jan,
YEAR = 1999,
ADDRESS = {San Jose, CA}
}
@inproceedings{Wilding99:DCCA,
TITLE = {Invariant Performance: A Statement of Task Isolation
Useful for Embedded Application Integration},
AUTHOR = {Matthew M. Wilding and David S. Hardin and David A.
Greve},
BOOKTITLE = {Dependable Computing for Critical Applications---7},
EDITOR = {Charles B. Weinstock and John Rushby},
PAGES = {287--300},
PUBLISHER = {IEEE Computer Society},
SERIES = {Dependable Computing and Fault Tolerant Systems},
VOLUME = 12,
MONTH = jan,
YEAR = 1999,
ADDRESS = {San Jose, CA}
}
@techreport{Butler96:rqts,
TITLE = {An Introduction to Requirements Capture Using {PVS}:
Specification of a Simple Autopilot},
AUTHOR = {Ricky W. Butler},
TYPE = {NASA Technical Memorandum},
NUMBER = 110255,
MONTH = may,
YEAR = 1996,
INSTITUTION = {NASA Langley Research Center},
ADDRESS = {Hampton, VA}
}
@article{Dutertre&Stavridou97,
TITLE = {Formal Requirements Analysis of an Avionics Control
System},
AUTHOR = {Bruno Dutertre and Victoria Stavridou},
JOURNAL = {IEEE Transactions on Software Engineering},
PAGES = {267--278},
VOLUME = 23,
NUMBER = 5,
MONTH = may,
YEAR = 1997
}
@inproceedings{Dutertre97:LFM,
TITLE = {Requirements Analysis of Real-Time Control Systems Using
{PVS}},
AUTHOR = {Bruno Dutertre and Victoria Stavridou},
BOOKTITLE = {LFM' 97: Fourth NASA Langley Formal Methods Workshop},
EDITOR = {C. Michael Holloway and Kelly J. Hayhurst},
PAGES = {65--74},
SERIES = {NASA Conference Publication 3356},
MONTH = sep,
YEAR = 1997,
ORGANIZATION = {NASA Langley Research Center},
ADDRESS = {Hampton, VA},
NOTE = {Available at \url{http://atb-www.larc.nasa.gov/Lfm97/proceedings/}}
}
@article{Crow&DiVito98:tosem,
TITLE = {Formalizing {Space Shuttle} Software Requirements: Four
Case Studies},
AUTHOR = {Judith Crow and Ben L. {Di Vito}},
JOURNAL = {ACM Transactions on Software Engineering and Methodology},
PAGES = {296--332},
VOLUME = 7,
NUMBER = 3,
MONTH = jul,
YEAR = 1998
}
@article{Easterbrook-etal98,
TITLE = {Experiences Using Lightweight Formal Methods for Requirements
Modeling},
AUTHOR = {Steve Easterbrook and Robyn Lutz and Richard Covington
and John Kelly and Yoko Ampo and David Hamilton},
JOURNAL = {IEEE Transactions on Software Engineering},
PAGES = {4--14},
VOLUME = 24,
NUMBER = 1,
MONTH = jan,
YEAR = 1998
}
@techreport{HAC-study,
TITLE = {Using Formal Methods to Assist in the Requirements Analysis
of the {Space Shuttle HAC Change Request (CR 90960E)}},
AUTHOR = {Larry W. Roberts and Mike Beims},
NUMBER = {JSC-27599},
MONTH = sep,
YEAR = 1996,
INSTITUTION = {NASA Johnson Space Center},
ADDRESS = {Houston, TX}
}
@inproceedings{DiVito96,
TITLE = {Formalizing New Navigation Requirements for {NASA's
Space Shuttle}},
AUTHOR = {Ben L. {Di Vito}},
BOOKTITLE = {Formal Methods Europe {FME '96}},
PAGES = {160--178},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1051,
MONTH = mar,
YEAR = 1996,
ADDRESS = {Oxford, UK}
}
@article{DiVito00:STTT,
TITLE = {High-Automation Proofs for Properties of Requirements
Models},
AUTHOR = {Ben L. {Di Vito}},
JOURNAL = {Software Tools for Technology Transfer},
VOLUME = 3,
NUMBER = 1,
YEAR = 2000,
NOTE = {To appear; available at \url{http://shemesh.larc.nasa.gov/people/bld/ftp/sttt-bld.ps}}
}
@techreport{GPS-study,
TITLE = {Using Formal Methods to Assist in the Requirements Analysis
of the {Space Shuttle GPS Change Request}},
AUTHOR = {Ben L. {Di Vito} and Larry W. Roberts},
TYPE = {NASA Contractor Report},
NUMBER = 4752,
MONTH = aug,
YEAR = 1996,
INSTITUTION = {NASA Langley Research Center}
}
@inproceedings{Hamilton-etal95,
TITLE = {Experiences in Applying Formal Methods to the Analysis
of Software and System Requirements},
AUTHOR = {David Hamilton and Rick Covington and John Kelly},
BOOKTITLE = {WIFT '95: Workshop on Industrial-Strength Formal
Specification Techniques},
PAGES = {30--43},
YEAR = 1995,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Boca Raton, FL}
}
@inproceedings{Hamilton-etal95-2,
TITLE = {An Experience Report on Requirements Reliability Engineering
Using Formal Methods},
AUTHOR = {David Hamilton and Rick Covington and Alice Lee},
BOOKTITLE = {Sixth International Conference on Software Reliability
Engineering, {ISSRE '95}},
PAGES = {52--57},
YEAR = 1995,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Toulouse, France}
}
@inproceedings{Ampo&Lutz95,
TITLE = {Evaluation of Software Safety Analysis Using Formal
Methods},
AUTHOR = {Yoko Ampo and Robyn Lutz},
BOOKTITLE = {Workshop for Foundation of Software Engineering
{(FOSE)}},
MONTH = dec,
YEAR = 1995,
ADDRESS = {Hamana-Ko, Japan},
NOTE = {In Japanese}
}
@inproceedings{Lutz&Ampo94,
TITLE = {Experience Report: Using Formal Methods for Requirements
Analysis of Critical Spacecraft Software},
AUTHOR = {Robyn Lutz and Yoko Ampo},
BOOKTITLE = {Proceedings of the 19th Annual Software Engineering
Workshop},
PAGES = {231--248},
MONTH = dec,
YEAR = 1994,
ORGANIZATION = {NASA Goddard Space Flight Center},
ADDRESS = {Greenbelt, MD}
}
@inproceedings{Lutz97:LFM,
TITLE = {Reuse of a Formal Model for Requirements Validation},
AUTHOR = {Robyn Lutz},
BOOKTITLE = {LFM' 97: Fourth NASA Langley Formal Methods Workshop},
EDITOR = {C. Michael Holloway and Kelly J. Hayhurst},
PAGES = {75--86},
SERIES = {NASA Conference Publication 3356},
MONTH = sep,
YEAR = 1997,
ORGANIZATION = {NASA Langley Research Center},
ADDRESS = {Hampton, VA},
NOTE = {Available at \url{http://atb-www.larc.nasa.gov/Lfm97/proceedings/}}
}
@inproceedings{Carreno&Munoz00:TPHOLS,
TITLE = {Aircraft Trajectory Modeling and Alerting Algorithm
Verification},
AUTHOR = {Victor Carre{\~{n}}o and C\'{e}sar Mu{\~{n}}oz},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 13th International
Conference, {TPHOLs 2000}},
EDITOR = {Mark Aargaard and John Harrison},
PAGES = {90--105},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1869,
MONTH = aug,
YEAR = 2000,
ADDRESS = {Portland, OR}
}
@inproceedings{Carreno&Munoz00:DASC,
TITLE = {Formal Analysis of Parallel Landing Scenarios},
AUTHOR = {Victor Carre{\~{n}}o and C\'{e}sar Mu{\~{n}}oz},
BOOKTITLE = {19th AIAA/IEEE Digital Avionics Systems Conference},
MONTH = oct,
YEAR = 2000,
ADDRESS = {Philadelphia, PA}
}
@inproceedings{Lawford-etal00:AMAST,
TITLE = {Practical Application of Functional and Relational Methods
for the Specification and Verification of Safety Critical
Software},
AUTHOR = {Mark Lawford and Jeff McDougall and Peter Froebel and
Greg Moum},
BOOKTITLE = {Algebraic Methodology and Software Technology, {AMAST}
2000},
EDITOR = {Teodor Rus},
PAGES = {73--88},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1816,
MONTH = may,
YEAR = 2000,
ADDRESS = {Iowa City, IA}
}
@article{Koo-etal99,
TITLE = {Mathematical Verification of a Nuclear Power Plant Protection
System Function With Combined {CPN} and {PVS}},
AUTHOR = {S. Koo and H. Son and P. Seong},
JOURNAL = {Journal of the Korean Nuclear Society},
PAGES = {157--171},
VOLUME = 31,
MONTH = apr,
YEAR = 1999
}
@inproceedings{vandePol98,
TITLE = {Formal Requirements Specification for Command and Control
Systems},
AUTHOR = {Jaco van de Pol and Jozef Hooman and Edwin de Jong},
BOOKTITLE = {Engineering of Computer Based Systems {(ECBS)}},
PAGES = {37--44},
MONTH = {March--April},
YEAR = 1998,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Jerusalem, Israel},
NOTE = {Available at \url{http://www.win.tue.nl/cs/tt/hooman/ECBS98.html}}
}
@inproceedings{Dean97,
TITLE = {Static Typing with Dynamic Linking},
AUTHOR = {Drew Dean},
BOOKTITLE = {Fourth ACM Conference on Computer and Communications
Security},
PAGES = {18--27},
MONTH = apr,
YEAR = 1997,
ORGANIZATION = {Association for Computing Machinery},
ADDRESS = {Zurich, Switzerland}
}
@inproceedings{Hoffman98:CAV,
TITLE = {A Formal Experience at {Secure Computing Corporation}},
AUTHOR = {John Hoffman and Charlie Payne},
BOOKTITLE = {Computer-Aided Verification, CAV '98},
EDITOR = {Alan J. Hu and Moshe Y. Vardi},
PAGES = {49--56},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1427,
MONTH = jun,
YEAR = 1998,
ADDRESS = {Vancouver, Canada}
}
@inproceedings{Peri96,
TITLE = {A Logic of Composition for Information Flow Predicates},
AUTHOR = {Ramesh V. Peri and William A. Wulf and Darrell M. Kienzle},
BOOKTITLE = {9th Computer Security Foundations Workshop},
PAGES = {82--94},
MONTH = jun,
YEAR = 1996,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Kenmare, Ireland}
}
@inproceedings{Dieckman98,
TITLE = {{ActiveSPEC}: A Framework for the Specification and
Verification of Active Network Services and Security
Policies},
AUTHOR = {Darryl Dieckman and Perry Alexander and Philip A. Wilsey},
BOOKTITLE = {Workshop on Formal Methods and Security Protocols},
EDITOR = {Nevin Heintze and Jeannette Wing},
MONTH = jun,
YEAR = 1998,
ADDRESS = {Indianapolis, IN},
NOTE = {Informal proceedings available at \url{http://www.cs.bell-labs.com/who/nch/fmsp/program.html}}
}
@inproceedings{Dutertre&Schneider97,
TITLE = {Embedding {CSP} in {PVS}. An Application to Authentication
Protocols},
AUTHOR = {Bruno Dutertre and Steve Schneider},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 10th International
Conference, {TPHOLs '97}},
EDITOR = {Elsa Gunter and Amy Felty},
PAGES = {121--136},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1275,
MONTH = aug,
YEAR = 1997,
ADDRESS = {Murray Hill, NJ}
}
@inproceedings{Millen:FMSP99,
TITLE = {A Necessarily Parallel Attack},
AUTHOR = {Jonathan K. Millen},
BOOKTITLE = {Workshop on Formal Methods and Security Protocols,
Part of the Federated Logic Conference},
EDITOR = {Nevin Heintze and Edmund Clarke},
MONTH = jul,
YEAR = 1999,
ADDRESS = {Trento, Italy}
}
@inproceedings{Monniaux99:CSFW,
TITLE = {Decision Procedures for the Analysis of Cryptographic
Protocols by Logics of Belief},
AUTHOR = {David Monniaux},
BOOKTITLE = {12th Computer Security Foundations Workshop},
PAGES = {44--54},
MONTH = jun,
YEAR = 1999,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Mordano, Italy}
}
@inproceedings{Ruess&Millen00:FMCS,
TITLE = {Local Secrecy for State-Based Models},
AUTHOR = {Harald Rue{\ss} and Jonathan Millen},
BOOKTITLE = {Formal Methods and Computer Security (FMCS)},
MONTH = jul,
YEAR = 2000,
ADDRESS = {Chicago, IL}
}
@inproceedings{Gopi98:FSTTCS,
TITLE = {Formal Verification of an {O.S.} Submodule},
AUTHOR = {N.S. Pendharkar and K. Gopinath},
BOOKTITLE = {18th Conference on the Foundations of Software Technology
and Theoretical Computer Science},
EDITOR = {V. Arvind and R. Ramanujin},
PAGES = {197--208},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1530,
MONTH = dec,
YEAR = 1998,
ADDRESS = {Madras, India}
}
@inproceedings{Couturier98:CAV,
TITLE = {An Experiment in Parallelizing an Application Using
Formal Methods},
AUTHOR = {Rapha\"{e}l Couturier and Dominique M\'{e}ry},
BOOKTITLE = {Computer-Aided Verification, CAV '98},
EDITOR = {Alan J. Hu and Moshe Y. Vardi},
PAGES = {345--356},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1427,
MONTH = jun,
YEAR = 1998,
ADDRESS = {Vancouver, Canada}
}
@inproceedings{Chkliaev99,
TITLE = {Mechanical Verification of a Non-Blocking Atomic Commitment
Protocol},
AUTHOR = {Dmitri Chkliaev and Jozef Hooman and Peter van der
Stok},
BOOKTITLE = {International Workshop on Distributed System Validation
and Verification (DSVV'2000)},
PAGES = {E96--E103},
MONTH = apr,
YEAR = 2000,
ADDRESS = {Taipei, Taiwan}
}
@inproceedings{Chkliaev99:AE,
TITLE = {Serializability Preserving Extensions of Concurrency
Control Protocols},
AUTHOR = {Dmitri Chkliaev and Jozef Hooman and Peter van der
Stok},
BOOKTITLE = {Third International {Andrei Ershov} Memorial Conference:
Perspectives of System Informatics, {PSI'99}},
EDITOR = {D. Bj{\o}rner and M. Broy and A.V. Zamulin},
PAGES = {180--193},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1755,
MONTH = jul,
YEAR = 1999,
ADDRESS = {Novosibirsk, Russia}
}
@inproceedings{Chkliaev00:ICFEM,
TITLE = {Mechanical Verification of Transaction Processing Systems},
AUTHOR = {Dmitri Chkliaev and Jozef Hooman and Peter van der
Stok},
BOOKTITLE = {Third International Conference on Formal Engineering
Methods (ICFEM 2000)},
PAGES = {89--97},
MONTH = nov,
YEAR = 200,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {York, England}
}
@inproceedings{Couturier98:IFMW,
TITLE = {Formal Engineering of the Bitonic Sort using {PVS}},
AUTHOR = {Rapha\"{e}l Couturier},
BOOKTITLE = {Proceedings, 2nd. Irish Workshop in Formal Methods},
PUBLISHER = {Electronic Workshops in Computing (\url{http://ewic.org.uk/ewic/})},
MONTH = jul,
YEAR = 1998,
ADDRESS = {Cork, Ireland}
}
@article{Devillers00:FMSD,
TITLE = {Verification of a Leader Election Protocol: Formal Methods
Applied to {IEEE 1394}},
AUTHOR = {Marco Devillers and David Griffioen and Judi Romijn
and Frits Vaandrager},
JOURNAL = {Formal Methods in Systems Design},
PAGES = {307--320},
VOLUME = 16,
NUMBER = 3,
MONTH = jun,
YEAR = 2000
}
@inproceedings{Glusman&Katz:CAV99,
TITLE = {Mechanizing Proofs of Computation Equivalence},
AUTHOR = {Marcelo Glusman and Shmuel Katz},
BOOKTITLE = {Computer-Aided Verification, CAV '99},
EDITOR = {Nicolas Halbwachs and Doron Peled},
PAGES = {354--367},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1633,
MONTH = jul,
YEAR = 1999,
ADDRESS = {Trento, Italy}
}
@inproceedings{Havelund:FMPPTA99,
TITLE = {Mechanical Verification of a Garbage Collector},
AUTHOR = {Klaus Havelund},
BOOKTITLE = {Parallel and Distributed Processing (Combined Proceedings
of 11 Workshops)},
EDITOR = {Jos\'{e} Rolim and others},
PAGES = {1258--1283},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1586,
MONTH = apr,
YEAR = 1999,
ADDRESS = {San Juan, Puerto Rico},
NOTE = {Presented at the Workshop on Formal Methods for Parallel
Programming: Theory and Applications {(FMPPTA)}}
}
@article{Hooman98:EAS,
TITLE = {Formal Verification of the Binary Exponential Backoff
Protocol},
AUTHOR = {Jozef Hooman},
JOURNAL = {Proceedings of the Estonian Academy of Sciences (Special
issue on the 9th Nordic Workshop on Programming Theory)},
PAGES = {89--105},
VOLUME = 4,
NUMBER = 2,
YEAR = 1998,
NOTE = {Also available at \url{http://www.win.tue.nl/cs/tt/hooman/BEB.html}}
}
@inproceedings{Jackson98:tphols,
TITLE = {Verifying a Garbage Collection Algorithm},
AUTHOR = {Paul Jackson},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 11th International
Conference, {TPHOLs '98}},
EDITOR = {Jim Grundy and Malcolm Newey},
PAGES = {225--244},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1479,
MONTH = sep,
YEAR = 1998,
ADDRESS = {Canberra, Australia}
}
@article{Mokkedem00:FMSD,
TITLE = {Formalization and Analysis of a Solution to the {PCI}
2.1 Bus Transaction Ordering Problem},
AUTHOR = {Abdel Mokkedem and Ravi M. Hosabettu and Michael D.
Jones and Ganesh C. Gopalakrishnan},
JOURNAL = {Formal Methods in Systems Design},
PAGES = {93--119},
VOLUME = 16,
NUMBER = 1,
MONTH = jan,
YEAR = 2000
}
@inproceedings{Penix98:fmsp,
TITLE = {Experiences in Verifying Parallel Simulation Algorithms},
AUTHOR = {John Penix and Dale Martin and Peter Frey and Radharamanan
Radhakrishnan and Perry Alexander and Phillip A. Wilsey},
BOOKTITLE = {Second Workshop on Formal Methods in Software Practice
(FMSP '98)},
EDITOR = {Mark Ardis},
PAGES = {16--23},
MONTH = mar,
YEAR = 1998,
ORGANIZATION = {Association for Computing Machinery},
ADDRESS = {Clearwater Beach, FL}
}
@article{Umamageswaran98:JSA,
TITLE = {Formal Verification and Empirical Analysis of Rollback
Relaxation},
AUTHOR = {Kothanda Umamageswaran and Krishnan Subramani and Philip
A. Wilsey and Perry Alexander},
JOURNAL = {Journal of Systems Architecture (formerly published
as Microprocessing and Microprogramming: the Euromicro
Journal)},
PAGES = {473--495},
VOLUME = 44,
NUMBER = {6--7},
MONTH = mar,
YEAR = 1998
}
@inproceedings{Alagar-etal99:RTAS,
TITLE = {From Behavioral Specification to Axiomatic Description
of Real-Time Reactive Systems},
AUTHOR = {V. S. Alagar and D. Muthiayen and F. Pompeo},
BOOKTITLE = {Fifth IEEE Real-Time Technology and Applications
Symposium, Work-In-Progress Session},
MONTH = jun,
YEAR = 1999,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Vancouver, British Columbia, Canada},
NOTE = {Available at \url{http://www.cs.concordia.ca/~faculty/manas/rtas99wip/}}
}
@inproceedings{Alborghetti97:FSE,
TITLE = {Providing Automated Support to Deductive Analysis of
Time Critical Systems},
AUTHOR = {Andren Alborghetti and Angelo Gargantini and Angelo
Morzenti},
BOOKTITLE = {Software Engineering---ESEC/FSE '97: Sixth European
Software Engineering Conference and Fifth ACM SIGSOFT
Symposium on the Foundations of Software Engineering},
EDITOR = {Mehdi Jazayeri and Helmut Schauer},
PAGES = {211--226},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1301,
MONTH = sep,
YEAR = 1997,
ADDRESS = {Zurich, Switzerland}
}
@inproceedings{Archer&Heitmeyer96,
TITLE = {Mechanical Verification of Timed Automata: A Case Study},
AUTHOR = {Myla Archer and Constance Heitmeyer},
BOOKTITLE = {IEEE Real-Time Technology and Applications Symposium
(RTAS'96)},
PAGES = {192--203},
PUBLISHER = {IEEE Computer Society},
MONTH = jun,
YEAR = 1996,
ADDRESS = {Brookline, MA}
}
@inproceedings{AHrtssWIP96,
TITLE = {{TAME}: A Specialized Specification and Verification
System for Timed Automata},
AUTHOR = {M. Archer and C. Heitmeyer},
BOOKTITLE = {Work In Progress (WIP) Proceedings of the 17th IEEE
Real-Time Systems Symposium (RTSS'96)},
EDITOR = {Azer Bestavros},
PAGES = {3--6},
MONTH = dec,
YEAR = 1996,
ADDRESS = {Washington, DC},
NOTE = {The WIP Proceedings is available at \url{http://www.cs.bu.edu/pub/ieee-rts/rtss96/wip/proceedings}}
}
@inproceedings{Bun96:ASCI,
TITLE = {Checking Properties of {ASTRAL} Specifications with
{PVS}},
AUTHOR = {Leon Bun},
BOOKTITLE = {Proceedings of 2nd Annual Conference of the Advanced
School for Computing and Imaging {(ASCI'96)}},
PAGES = {102--107},
MONTH = jun,
YEAR = 1996,
ADDRESS = {Lommel, Belgium},
NOTE = {Available at \url{http://sepc.twi.tudelft.nl/~leonbun/papers/asci96.ps}}
}
@inproceedings{Bun97:ASCI,
TITLE = {Embedding {Astral} in {PVS}},
AUTHOR = {Leon Bun},
BOOKTITLE = {Proceedings of 3rd Annual Conference of the Advanced
School for Computing and Imaging {(ASCI'97)}},
PAGES = {130--136},
MONTH = jun,
YEAR = 1997,
ADDRESS = {Lommel, Belgium},
NOTE = {Available at \url{http://sepc.twi.tudelft.nl/~leonbun/papers/asci97.ps}}
}
@inproceedings{deBoer96:ftrtft,
TITLE = {Compositionality in Real-Time Shared Variable Concurrency},
AUTHOR = {F. S. de Boer and H. Tej and W.-P. de Roever and M.
van Hulst},
BOOKTITLE = {Formal Techniques in Real-Time and Fault-Tolerant
Systems},
EDITOR = {Bengt Jonsson and Joachim Parrow},
PAGES = {420--439},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1135,
MONTH = sep,
YEAR = 1996,
ADDRESS = {Uppsala, Sweden}
}
@inproceedings{DuBois97:isre,
TITLE = {On the Use of a Formal {RE} Language: The Generalized
Railroad Crossing Problem},
AUTHOR = {Philippe Du Bois and Eric Dubois and Jean-Marc Zeippen},
BOOKTITLE = {3rd IEEE International Symposium on Requirements
Engineering},
PAGES = {128--137},
MONTH = jan,
YEAR = 1997,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Annapolis, MD}
}
@techreport{dutertre99b,
TITLE = {The {Priority Ceiling Protocol}: Formalization and Analysis
Using {PVS}},
AUTHOR = {Bruno Dutertre},
MONTH = oct,
YEAR = 1999,
INSTITUTION = {System Design Laboratory, SRI International},
ADDRESS = {Menlo Park, CA},
NOTE = {Available at \url{http://www.sdl.sri.com/dsa/publis/prio-ceiling.html}}
}
@inproceedings{Dutertre&Stavridou00:DASC,
TITLE = {Formal Analysis for Realtime Scheduling},
AUTHOR = {Bruno Dutertre and Victoria Stavridou},
BOOKTITLE = {19th AIAA/IEEE Digital Avionics Systems Conference},
MONTH = oct,
YEAR = 2000,
ADDRESS = {Philadelphia, PA}
}
@inproceedings{Dutertre00:RTSS,
TITLE = {Formal Analysis of the Priority Ceiling Protocol},
AUTHOR = {Bruno Dutertre},
BOOKTITLE = {Real Time Systems Symposium},
MONTH = dec,
YEAR = 2000,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Orlando, FL},
NOTE = {To appear}
}
@inproceedings{Fowler&Wellings96,
TITLE = {Formal Analysis of a Real-Time Kernel Specification},
AUTHOR = {Simon Fowler and Andy Wellings},
BOOKTITLE = {Formal Techniques in Real-Time and Fault-Tolerant
Systems},
EDITOR = {Bengt Jonsson and Joachim Parrow},
PAGES = {440--458},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1135,
MONTH = sep,
YEAR = 1996,
ADDRESS = {Uppsala, Sweden}
}
@inproceedings{Fowler97:RTSS,
TITLE = {Formal Development Of A Real-Time Kernel},
AUTHOR = {Simon Fowler and Andy Wellings},
BOOKTITLE = {Real Time Systems Symposium},
PAGES = {220--229},
MONTH = dec,
YEAR = 1997,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {San Francisco, CA}
}
@inproceedings{Hooman94,
TITLE = {Correctness of Real Time Systems by Construction},
AUTHOR = {Jozef Hooman},
BOOKTITLE = {Formal Techniques in Real-Time and Fault-Tolerant
Systems},
EDITOR = {H. Langmaack and W.-P. {de Roever} and J. Vytopil},
PAGES = {19--40},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 863,
MONTH = sep,
YEAR = 1994,
ADDRESS = {L\"{u}beck, Germany}
}
@inproceedings{Hooman96:RPC,
TITLE = {Using {PVS} for an Assertional Verification of the {RPC-Memory}
Specification Problem},
AUTHOR = {Jozef Hooman},
BOOKTITLE = {Formal Systems Specification: The {RPC-Memory} Specification
Case Study},
EDITOR = {Manfred Broy and Stephan Merz and Katharina Spies},
PAGES = {275--304},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1169,
YEAR = 1996
}
@inproceedings{Hooman97:AMAST,
TITLE = {Verification of Distributed Real-Time and Fault-Tolerant
Protocols},
AUTHOR = {Jozef Hooman},
BOOKTITLE = {Algebraic Methodology and Software Technology, {AMAST}'97},
EDITOR = {Michael Johnson},
PAGES = {261--275},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1349,
MONTH = dec,
YEAR = 1997,
ADDRESS = {Sydney, Australia}
}
@inproceedings{Hooman97:compos,
TITLE = {Compositional Verification of Real-Time Applications},
AUTHOR = {Jozef Hooman},
BOOKTITLE = {Compositionality: The Significant Difference (Revised
lectures from International Symposium {COMPOS'97})},
EDITOR = {Willem-Paul de Roever and Hans Langmaack and Amir Pnueli},
PAGES = {276--300},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1536,
MONTH = sep,
YEAR = 1997,
ADDRESS = {Bad Malente, Germany}
}
@inproceedings{Kolano99:ARTS,
TITLE = {Proof Assistance for Real-Time Systems Using an Interactive
Theorem Prover},
AUTHOR = {Paul Z. Kolano},
BOOKTITLE = {Formal Methods for Real-Time and Probabilistic Systems
(Proceedings 5th International {AMAST} Workshop, {ARTS'99})},
EDITOR = {J.-P. Katoen},
PAGES = {315--333},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1601,
MONTH = may,
YEAR = 1999,
ADDRESS = {Bamberg, Germany}
}
@inproceedings{Kolano-etal00:FASE,
TITLE = {Parallel Refinement Mechanisms for Real-Time Systems},
AUTHOR = {Paul Kolano and Richard Kemmerer and Dino Mandrioli},
BOOKTITLE = {Fundamental Approaches to Software Engineering,
{FASE} 2000},
EDITOR = {Tom Maibaum},
PAGES = {35--50},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
NUMBER = 1783,
MONTH = {March/April},
YEAR = 2000,
ADDRESS = {Berlin, Germany}
}
@phdthesis{Muthiayen00,
TITLE = {Real-Time Reactive System Development---A Formal Approach
Based on {UML} and {PVS}},
AUTHOR = {Darmalingum Muthiayen},
MONTH = jan,
YEAR = 2000,
SCHOOL = {Department of Computer Science at Concordia University},
ADDRESS = {Montreal, Canada}
}
@inproceedings{Shankar93:CAV,
TITLE = {Verification of Real-Time Systems Using {PVS}},
AUTHOR = {Natarajan Shankar},
BOOKTITLE = {Computer-Aided Verification, CAV '93},
EDITOR = {Costas Courcoubetis},
PAGES = {280--291},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 697,
MONTH = {June/July},
YEAR = 1993,
ADDRESS = {Elounda, Greece}
}
@phdthesis{Skakkebaek94:thesis,
TITLE = {A Verification Assistant for a Real-Time Logic},
AUTHOR = {Jens Ulrik Skakkeb{\ae}k},
MONTH = nov,
YEAR = 1994,
SCHOOL = {Department of Computer Science, Technical University
of Denmark},
ADDRESS = {Lyngby, Denmark}
}
@inproceedings{Skakkebaek&Shankar94,
TITLE = {Towards a {Duration Calculus} Proof Assistant in {PVS}},
AUTHOR = {Jens U. Skakkeb{\ae}k and N. Shankar},
BOOKTITLE = {Formal Techniques in Real-Time and Fault-Tolerant
Systems},
EDITOR = {H. Langmaack and W.-P. {de Roever} and J. Vytopil},
PAGES = {660--679},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 863,
MONTH = sep,
YEAR = 1994,
ADDRESS = {L\"{u}beck, Germany}
}
@inproceedings{Kellomaki97,
TITLE = {Verification of Reactive Systems Using {DisCo} and {PVS}},
AUTHOR = {Pertti Kellom\"{a}ki},
BOOKTITLE = {Formal Methods Europe {FME '97}},
PAGES = {589--604},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1313,
MONTH = sep,
YEAR = 1997,
ADDRESS = {Graz, Austria}
}
@inproceedings{AHhart97,
TITLE = {Verifying Hybrid Systems Modeled as Timed Automata:
A Case Study},
AUTHOR = {M. Archer and C. Heitmeyer},
BOOKTITLE = {Proceedings of the International Workshop on Hybrid
and Real-Time Systems (HART'97)},
EDITOR = {Oded Maler},
PAGES = {171--185},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1201,
MONTH = mar,
YEAR = 1997,
ADDRESS = {Grenoble, France}
}
@inproceedings{Henzinger&Rusu98,
TITLE = {Reachability Verification for Hybrid Automata},
AUTHOR = {Thomas A. Henzinger and Vlad Rusu},
BOOKTITLE = {Hybrid Systems: Computation and Control (First International
Workshop, {HSCC'98})},
EDITOR = {Thomas A. Henzinger and Shankar Sastry},
PAGES = {190--204},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1386,
MONTH = apr,
YEAR = 1998,
ADDRESS = {Berkeley, CA}
}
@inproceedings{Hooman96:boiler,
TITLE = {Assertional Specification and Verification Using {PVS}
of the Steam Boiler Control System},
AUTHOR = {Jan Vitt and Jozef Hooman},
BOOKTITLE = {Formal Methods for Industrial Applications: Specifying
and Programming the Steam Boiler Control},
EDITOR = {Jean-Raymond Abrial and Egon Boerger and Hans Langmaack},
PAGES = {453--472},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1165,
YEAR = 1996
}
@inproceedings{Bloo-etal00:SAC,
TITLE = {Semantical Aspects of an Architecture for Distributed
Embedded Systems},
AUTHOR = {Roel Bloo and Jozef Hooman and Edwin de Jong},
BOOKTITLE = {Proceedings of the 2000 ACM Symposium on Applied
Computing {(SAC 2000)}},
PAGES = {149-155},
VOLUME = 1,
MONTH = mar,
YEAR = 2000,
ORGANIZATION = {Association for Computing Machinery},
ADDRESS = {Como, Italy}
}
@inproceedings{deJong00:ECBS,
TITLE = {Refinement in Requirements Specification and Analysis:
A Case Study},
AUTHOR = {Edwin de Jong and Jaco van de Pol and Jozef Hooman},
BOOKTITLE = {7th IEEE International Conference and Workshop on
the Engineering of Computer Based Systems {(ECBS)}},
PAGES = {290--298},
MONTH = apr,
YEAR = 2000,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Edinburgh, Scotland}
}
@inproceedings{vandePol-etal99:IFM,
TITLE = {Modular Formal Specification of Data and Behaviour},
AUTHOR = {Jaco van de Pol and Jozef Hooman and Edwin de Jong},
BOOKTITLE = {Proceedings 1st Conference on Integrated Formal
Methods {(IFM'99)}},
EDITOR = {K. Araki and A. Galloway and K. Taguchi},
PAGES = {109--128},
PUBLISHER = {Springer},
MONTH = jun,
YEAR = 1999,
ADDRESS = {York, UK}
}
@inproceedings{deBoer&Hulst96,
TITLE = {Local Nondeterminism in Asynchronously Communicating
Processes},
AUTHOR = {Frank S. de Boer and Marten van Hulst},
BOOKTITLE = {Formal Methods Europe {FME '96}},
PAGES = {367--384},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1051,
MONTH = mar,
YEAR = 1996,
ADDRESS = {Oxford, UK}
}
@inproceedings{Chernyskhovsky:FMPPTA99,
TITLE = {A Formal Framework for Specifying and Verifying Time
Warp Optimizations},
AUTHOR = {Victoria Chernyakhovsky and Peter Frey and Radharamanan
Radhakrihnan and Philip A. Wilsey and Perry Alexander
and Harold W. Carter},
BOOKTITLE = {Parallel and Distributed Processing (Combined Proceedings
of 11 Workshops)},
EDITOR = {Jos\'{e} Rolim and others},
PAGES = {1228--1242},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1586,
MONTH = apr,
YEAR = 1999,
ADDRESS = {San Juan, Puerto Rico},
NOTE = {Presented at the Workshop on Formal Methods for Parallel
Programming: Theory and Applications {(FMPPTA)}}
}
@inproceedings{Frey99:HICSS,
TITLE = {An Extensible Formal Framework for the Specification
and Verification of an Optimistic Simulation Protocol},
AUTHOR = {Peter Frey and Radharamanan Radhakrishnan and Philip
A. Wilsey and Perry Alexander and Harold W. Carter},
BOOKTITLE = {Proceedings of the 32nd Annual Hawaii International
Conference on System Sciences},
MONTH = jan,
YEAR = 1999,
ORGANIZATION = {IEEE Computer Society},
NOTE = {Available at \url{http://computer.org/conferen/proceed/hicss/0001/00013/00013049abs.htm}}
}
@inproceedings{Hooman98:TOOLS96,
TITLE = {Developing Proof Rules for Distributed Real-Time Systems
with {PVS}},
AUTHOR = {Jozef Hooman},
BOOKTITLE = {Tools for System Development and Verification},
EDITOR = {Bettina Buth and Rudolf Berghammer and Jan Peleska},
PAGES = {120--139},
PUBLISHER = {Shaker Verlag},
SERIES = {BISS Monographs},
YEAR = 1998,
ADDRESS = {Aachen, Germany},
NOTE = {Proceedings of a workshop held at Bremen in 1996}
}
@inproceedings{Kellomaki95,
TITLE = {Mechanizing Invariant Proofs of Joint Action Systems},
AUTHOR = {Pertti Kellom\"{a}ki},
BOOKTITLE = {Fourth Symposium on Programming Languages and Software
Tools},
PAGES = {141--152},
MONTH = jun,
YEAR = 1995,
ADDRESS = {Visegrad, Hungary},
NOTE = {Available at \url{http://www.cs.tut.fi/~pk/papers/visegrad-95/visegrad.ps.gz}}
}
@inproceedings{Kellomaki96:tphols,
TITLE = {Using Auxiliary Knowledge in Automating Invariant Proofs},
AUTHOR = {Pertti Kellom\"{a}ki},
BOOKTITLE = {International Conference on Theorem Proving in Higher
Order Logics},
PAGES = {57--68},
MONTH = aug,
YEAR = 1996,
ADDRESS = {Turku, Finland},
NOTE = {Supplementary proceedings, available at \url{http://www.tucs.abo.fi/publications/general/G1.html}}
}
@inproceedings{Lesens&Saidi97,
TITLE = {Automatic Verification of Parameterized Networks of
Processes by Abstraction},
AUTHOR = {David Lesens and Hassen Sa{\"\i}di},
BOOKTITLE = {2nd International Workshop on Verification of Infinite
State Systems: Infinity '97},
EDITOR = {Faron Moller},
PUBLISHER = {Elsevier},
SERIES = {Electronic Notes in Theoretical Computer Science},
VOLUME = 9,
MONTH = jul,
YEAR = 1997,
ADDRESS = {Bologna, Italy},
NOTE = {Available at \url{http://www.elsevier.nl/cas/tree/store/tcs/free/entcs/store/tcs9/tcs9009%
.ps}}
}
@techreport{Shankar93:lazy,
TITLE = {A Lazy Approach to Compositional Verification},
AUTHOR = {N. Shankar},
NUMBER = {SRI-CSL-93-8},
MONTH = dec,
YEAR = 1993,
INSTITUTION = {Computer Science Laboratory, SRI International},
ADDRESS = {Menlo Park, CA}
}
@phdthesis{vanHulst:thesis,
TITLE = {Compositional Verification of Parallel Programs using
Epistemic Logic and Abstract Assertional Languages},
AUTHOR = {Marten van Hulst},
MONTH = jun,
YEAR = 1995,
SCHOOL = {Faculteit Wiskunde en Informatica, Universiteit Utrecht},
ADDRESS = {The Netherlands}
}
@inproceedings{Hooman95,
TITLE = {Verifying Part of the {ACCESS.bus} Protocol Using {PVS}},
AUTHOR = {Jozef Hooman},
BOOKTITLE = {15th Conference on the Foundations of Software Technology
and Theoretical Computer Science},
EDITOR = {P. S. Thiagarajan},
PAGES = {96--110},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1026,
MONTH = dec,
YEAR = 1995,
ADDRESS = {Bangalore, India}
}
@inproceedings{Havelund&Shankar96,
TITLE = {Experiments in Theorem Proving and Model Checking for
Protocol Verification},
AUTHOR = {Klaus Havelund and N. Shankar},
BOOKTITLE = {Formal Methods Europe {FME '96}},
PAGES = {662--681},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1051,
MONTH = mar,
YEAR = 1996,
ADDRESS = {Oxford, UK}
}
@inproceedings{Khune-etal97,
TITLE = {Towards Mechanical Verification of Parts of the {IEEE
P1394} Serial Bus},
AUTHOR = {Lars Kh\"{u}ne and Jozef Hooman and Willem-Paul de
Roever},
BOOKTITLE = {2nd International Workshop on Applied Formal Methods
in System Design},
MONTH = jun,
YEAR = 1997,
ADDRESS = {Zagreb, Croatia},
NOTE = {Available at \url{http://www.win.tue.nl/cs/tt/hooman/P1394.html}}
}
@inproceedings{Mokkedem&Leonard00:TPHOLS,
TITLE = {Formal Verification of the {Alpha} 21364 Network Protocol},
AUTHOR = {Abdel Mokkedem and Tim Leonard},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 13th International
Conference, {TPHOLs 2000}},
EDITOR = {Mark Aargaard and John Harrison},
PAGES = {443--461},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1869,
MONTH = aug,
YEAR = 2000,
ADDRESS = {Portland, OR}
}
@inproceedings{Rusinowitch-etal00:CAV,
TITLE = {Mechanical Verification of a Generic Incremental {ABR}
Conformance Algorithm},
AUTHOR = {Micha\"{e}l Rusinowitch and Sorin Stratulat and Francis
Klay},
BOOKTITLE = {Computer-Aided Verification, CAV '2000},
EDITOR = {E. A. Emerson and A. P. Sistla},
PAGES = {344--357},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1855,
MONTH = jul,
YEAR = 2000,
ADDRESS = {Chicago, IL}
}
@inproceedings{Herbert-etal:FM99,
TITLE = {A Formalization of Software Architecture},
AUTHOR = {John Herbert and Bruno Dutertre and Robert Riemenschneider
and Victoria Stavridou},
BOOKTITLE = {FM99: The World Congress in Formal Methods},
EDITOR = {Jeannette Wing and Jim Woodcock},
PAGES = {116--133},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1708 and 1709},
MONTH = sep,
YEAR = 1999,
ADDRESS = {Toulouse, France},
NOTE = {Pages 1--938 are in the first volume, 939--1872 in the
second.}
}
@inproceedings{Hooman97,
TITLE = {Program Design in {PVS}},
AUTHOR = {Jozef Hooman},
BOOKTITLE = {Workshop on Tool Support for System Development
and Verification},
EDITOR = {K.Berghammer and J.Peleska and B. Buth},
YEAR = 1997,
ADDRESS = {Bremen, Germany},
NOTE = {Available at \url{http://www.win.tue.nl/cs/tt/hooman/PDPVS.html}}
}
@inproceedings{Levy&Trilling:FM99,
TITLE = {A {PVS}-Based Approach for Teaching Constructing Correct
Iterations},
AUTHOR = {Michel L\'{e}vy and Laurent Trilling},
BOOKTITLE = {FM99: The World Congress in Formal Methods},
EDITOR = {Jeannette Wing and Jim Woodcock},
PAGES = {1859--1860},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1708 and 1709},
MONTH = sep,
YEAR = 1999,
ADDRESS = {Toulouse, France},
NOTE = {Pages 1--938 are in the first volume, 939--1872 in the
second.}
}
@inproceedings{Verhoeven&Backhouse:FM99,
TITLE = {Interfacing Program Construction and Verification},
AUTHOR = {Richard Verhoeven and Roland Backhouse},
BOOKTITLE = {FM99: The World Congress in Formal Methods},
EDITOR = {Jeannette Wing and Jim Woodcock},
PAGES = {1128--1146},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1708 and 1709},
MONTH = sep,
YEAR = 1999,
ADDRESS = {Toulouse, France},
NOTE = {Pages 1--938 are in the first volume, 939--1872 in the
second.}
}
@inproceedings{Behnke98:TOOLS96,
TITLE = {Supporting Algebraic Program Derivation by {PVS}},
AUTHOR = {Ralf Behnke and Rudolf Berghammer and S\"{o}nke Magnussen},
BOOKTITLE = {Tools for System Development and Verification},
EDITOR = {Bettina Buth and Rudolf Berghammer and Jan Peleska},
PAGES = {22--40},
PUBLISHER = {Shaker Verlag},
SERIES = {BISS Monographs},
YEAR = 1998,
ADDRESS = {Aachen, Germany},
NOTE = {Proceedings of a workshop held at Bremen in 1996}
}
@inproceedings{Dold95,
TITLE = {Representing, Verifying and Applying Software Development
Steps using the {PVS} system},
AUTHOR = {Axel Dold},
BOOKTITLE = {Algebraic Methodology and Software Technology, AMAST'95},
EDITOR = {V. S. Alagar and Maurice Nivat},
PAGES = {431--445},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 936,
MONTH = jul,
YEAR = 1995,
ADDRESS = {Montreal, Canada}
}
@phdthesis{Dold:PhD,
TITLE = {Formal Software Development using Generic Development
Steps},
AUTHOR = {Axel Dold},
YEAR = 2000,
SCHOOL = {Universit{\"a}t Ulm, Germany}
}
@inproceedings{Shankar:MPC95,
TITLE = {Computer-Aided Computing},
AUTHOR = {N. Shankar},
BOOKTITLE = {Mathematics of Program Construction '95},
EDITOR = {Bernhard M\"oller},
PAGES = {50--66},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 947,
YEAR = 1995
}
@article{Shankar:SCP96,
TITLE = {Steps Towards Mechanizing Program Transformations Using
{PVS}},
AUTHOR = {N. Shankar},
JOURNAL = {Science of Computer Programming},
PAGES = {33--57},
VOLUME = 26,
NUMBER = {1--3},
YEAR = 1996
}
@inproceedings{Jacobs97,
TITLE = {Behaviour-Refinement of Coalgebraic Specifications with
Coinductive Correctness Proofs},
AUTHOR = {Bart Jacobs},
BOOKTITLE = {{TAPSOFT} '97: Theory and Practice of Software Development},
EDITOR = {Michel Bidoit and Max Dauchet},
PAGES = {787--802},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1214,
MONTH = apr,
YEAR = 1997,
ADDRESS = {Lille, France}
}
@inproceedings{Jacobs97:AMAST,
TITLE = {Invariants, Bisimulations and the Correctness of Coalgebraic
Refinements},
AUTHOR = {Bart Jacobs},
BOOKTITLE = {Algebraic Methodology and Software Technology, {AMAST}'97},
EDITOR = {Michael Johnson},
PAGES = {276--291},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1349,
MONTH = dec,
YEAR = 1997,
ADDRESS = {Sydney, Australia}
}
@inproceedings{Jackson00:TPHOLS,
TITLE = {Total-Correctness Refinement for Sequential Reactive
Systems},
AUTHOR = {Paul Jackson},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 13th International
Conference, {TPHOLs 2000}},
EDITOR = {Mark Aargaard and John Harrison},
PAGES = {320--337},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1869,
MONTH = aug,
YEAR = 2000,
ADDRESS = {Portland, OR}
}
@mastersthesis{Knappmann96,
TITLE = {A {PVS} Based Tool for Developing Programs in the {Refinement
Calculus}},
AUTHOR = {Jens Knappmann},
MONTH = oct,
YEAR = 1996,
SCHOOL = {Institut f\"{u}r Informatik und Praktische Mathematik
der Christian-Albrechts-Universit\"{a}t zu Kiel},
ADDRESS = {Kiel, Germany}
}
@techreport{K-HButh95,
TITLE = {Automated Code Generator Verification Based on Algebraic
Laws},
AUTHOR = {Karl-Heinz Buth},
TYPE = {Procos II Report},
NUMBER = {Kiel KHB 5/1},
MONTH = sep,
YEAR = 1995,
INSTITUTION = {Christian-Albrechts Universit{\"a}t zu Kiel},
ADDRESS = {Kiel, Germany},
NOTE = {Available at \url{ftp://ftp.informatik.uni-kiel.de/pub/kiel/procos/kiel-khb-5-1.ps.Z}}
}
@inproceedings{Dold-etal97,
TITLE = {Formal Verification of Transformations for Peephole
Optimiztion},
AUTHOR = {A. Dold and F. W. von Henke and H. Pfeifer and H. Rue{\ss}},
BOOKTITLE = {Formal Methods Europe {FME '97}},
PAGES = {459--472},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1313,
MONTH = sep,
YEAR = 1997,
ADDRESS = {Graz, Austria}
}
@inproceedings{DGVZ98,
TITLE = {{{ASM}-Based Mechanized Verification of Compiler Backends}},
AUTHOR = {A. Dold and T. Gaul and V. Vialard and W. Zimmermann},
BOOKTITLE = {Proceedings of the 5th International Workshop on
Abstract State Machines},
EDITOR = {Uwe Gl{\"a}sser and Peter H. Schmitt},
PAGES = {50-67},
MONTH = sep,
YEAR = 1998,
ADDRESS = {Magdeburg, Germany},
NOTE = {Available at \url{http://i44www.info.uni-karlsruhe.de/~verifix/pres/paper/ASM-WS98-DGVZ.p%
s.gz}}
}
@inproceedings{Dold-etal98:STTT,
TITLE = {Mechanized Verification of Compiler Backends},
AUTHOR = {Axel Dold and Thilo Gaul and Wolf Zimmermann},
BOOKTITLE = {Proceedings of the International Workshop on Software
Tools for Technology Transfer {STTT'98}},
EDITOR = {Tiziana Margaria and Bernhard Steffen},
PAGES = {13--22},
MONTH = jun,
YEAR = 1998,
ORGANIZATION = {BRICS NS-98-4},
ADDRESS = {Aalborg, Denmark},
NOTE = {Proceedings available at \url{http://www.brics.dk/NS/98/4/}}
}
@inproceedings{Dold&Vialard99,
TITLE = {Formal Verification of a Compiler Back-End Generic Checker
Program},
AUTHOR = {Axel Dold and Vincent Vialard},
BOOKTITLE = {Third International {Andrei Ershov} Memorial Conference:
Perspectives of System Informatics, {PSI'99}},
EDITOR = {D. Bj{\o}rner and M. Broy and A.V. Zamulin},
PAGES = {470--480},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1755,
MONTH = jul,
YEAR = 1999,
ADDRESS = {Novosibirsk, Russia}
}
@inproceedings{Stringer-Calvert97,
TITLE = {Using {PVS} to Prove a {Z} refinement: A Case Study},
AUTHOR = {David W. J. Stringer-Calvert and Susan Stepney and
Ian Wand},
BOOKTITLE = {Formal Methods Europe {FME '97}},
PAGES = {573--588},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1313,
MONTH = sep,
YEAR = 1997,
ADDRESS = {Graz, Austria}
}
@phdthesis{Stringer-Calvert98:thesis,
TITLE = {Mechanical Verification of Compiler Correctness},
AUTHOR = {David W. J. Stringer-Calvert},
MONTH = mar,
YEAR = 1998,
SCHOOL = {University of York, Department of Computer Science},
ADDRESS = {York, England},
NOTE = {Available at \url{http://www.csl.sri.com/~dave_sc/papers/thesis.html}}
}
@techreport{Wahab:UWARWICK:CS-RR-354,
TITLE = {Verification and Abstraction of Flow-Graph Programs
with Pointers and Computed Jumps},
AUTHOR = {M. Wahab},
TYPE = {Research Report},
NUMBER = {CS-RR-354},
MONTH = nov,
YEAR = 1998,
INSTITUTION = {Department of Computer Science, University of
Warwick},
ADDRESS = {Coventry, UK},
NOTE = {Available at \url{http://www.dcs.warwick.ac.uk/pub/reports/rr/354.html}}
}
@phdthesis{Wahab98,
TITLE = {Object Code Verification},
AUTHOR = {Matthew Wahab},
MONTH = dec,
YEAR = 1998,
SCHOOL = {Department of Computer Science, University of Warwick},
ADDRESS = {Coventry, UK},
NOTE = {Available at \url{http://www.dcs.warwick.ac.uk/pub/reports/theses/wahab98.html}}
}
@inproceedings{Arons99:VLSI,
TITLE = {Verifying {Tomasulo'}s Algorithm by Refinement},
AUTHOR = {Tamara Arons and Amir Pnueli},
BOOKTITLE = {The Twelfth International Conference on {VLSI} Design},
PAGES = {306--309},
MONTH = jan,
YEAR = 1999,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Goa, India}
}
@inproceedings{Arons&Pnueli00:TACAS,
TITLE = {A Comparison of two Verification Methods for Speculative
Instruction Execution},
AUTHOR = {Tamarah Arons and Amir Pnueli},
BOOKTITLE = {Tools and Algorithms for the Construction and Analysis
of Systems {(TACAS 2000)}},
EDITOR = {Susanne Graf and Michael Schwartzbach},
PAGES = {487--502},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
NUMBER = 1785,
MONTH = mar,
YEAR = 2000,
ADDRESS = {Berlin, Germany}
}
@inproceedings{Cyrluk96:FMCAD,
TITLE = {Inverting the Abstraction Mapping: A Methodology for
Hardware Verification},
AUTHOR = {David Cyrluk},
BOOKTITLE = {Formal Methods in Computer-Aided Design (FMCAD '96)},
EDITOR = {Mandayam Srivas and Albert Camilleri},
PAGES = {172--186},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1166,
MONTH = nov,
YEAR = 1996,
ADDRESS = {Palo Alto, CA}
}
@inproceedings{Cyrluk97:ICFEM,
TITLE = {Systematic Formal Verification of Interpreters},
AUTHOR = {David Cyrluk and John Rushby and Mandayam Srivas},
BOOKTITLE = {First International Conference on Formal Engineering
Methods (ICFEM '97)},
EDITOR = {Michael G. Hinchey and Shaoying Liu},
PAGES = {140--149},
MONTH = nov,
YEAR = 1997,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Hiroshima, Japan}
}
@inproceedings{Damm&Pnueli97,
TITLE = {Verifying Out-of-Order Executions},
AUTHOR = {Werner Damm and Amir Pnueli},
BOOKTITLE = {Advances in Hardware Design and Verification: {IFIP
WG10.5} International Conference on Correct Hardware
Design and Verification Methods (CHARME)},
EDITOR = {Hon F. li and David K. Probst},
PAGES = {23--47},
PUBLISHER = {Chapman \& Hall},
MONTH = oct,
YEAR = 1997,
ADDRESS = {Montreal, Canada}
}
@inproceedings{Fisler94:TPCD,
TITLE = {Extending Formal Reasoning with Support for Hardware
Diagrams},
AUTHOR = {Kathi Fisler},
BOOKTITLE = {Theorem Provers in Circuit Design ({TPCD} '94)},
EDITOR = {Ramayya Kumar and Thomas Kropf},
PAGES = {298--303},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 910,
MONTH = sep,
YEAR = 1994,
ADDRESS = {Bad Herrenalb, Germany}
}
@inproceedings{Gopalakrishnan-etal97,
TITLE = {Formal Modeling and Validation Applied to a Commercial
Coherent Bus: A Case Study},
AUTHOR = {Ganesh Gopalakrishnan and Rajnish Ghughal and Ravi
Hosabettu and Abdelillah Mokkedem and Ratan Nalumasu},
BOOKTITLE = {Advances in Hardware Design and Verification: {IFIP
WG10.5} International Conference on Correct Hardware
Design and Verification Methods (CHARME)},
EDITOR = {Hon F. li and David K. Probst},
PAGES = {48--62},
PUBLISHER = {Chapman \& Hall},
MONTH = oct,
YEAR = 1997,
ADDRESS = {Montreal, Canada}
}
@inproceedings{Greve98:FMCAD,
TITLE = {Symbolic Simulation of the {JEM1} Microprocessor},
AUTHOR = {David Greve},
BOOKTITLE = {Formal Methods in Computer-Aided Design (FMCAD '98)},
EDITOR = {Ganesh Gopalakrishnan and Phillip Windley},
PAGES = {321--333},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1522,
MONTH = nov,
YEAR = 1998,
ADDRESS = {Palo Alto, CA}
}
@inproceedings{Hardin98:CAV,
TITLE = {Transforming the Theorem Prover into a Digital Design
Tool: From Concept Car to Off-Road Vehicle},
AUTHOR = {David Hardin and Matthew Wilding and David Greve},
BOOKTITLE = {Computer-Aided Verification, CAV '98},
EDITOR = {Alan J. Hu and Moshe Y. Vardi},
PAGES = {39--44},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1427,
MONTH = jun,
YEAR = 1998,
ADDRESS = {Vancouver, Canada}
}
@inproceedings{Hosabettu98:CAV,
TITLE = {Decomposing the Proof of Correctness of Pipelined Microprocessors},
AUTHOR = {Ravi Hosabettu and Mandayam Srivas and Ganesh Gopalakrishnan},
BOOKTITLE = {Computer-Aided Verification, CAV '98},
EDITOR = {Alan J. Hu and Moshe Y. Vardi},
PAGES = {122--134},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1427,
MONTH = jun,
YEAR = 1998,
ADDRESS = {Vancouver, Canada}
}
@inproceedings{Hosabettu:CAV99,
TITLE = {Proof of Correctness of a Processor with Reorder Buffer
using the Completion Functions Approach},
AUTHOR = {Ravi Hosabettu and Mandayam Srivas and Ganesh Gopalakrishnan},
BOOKTITLE = {Computer-Aided Verification, CAV '99},
EDITOR = {Nicolas Halbwachs and Doron Peled},
PAGES = {47--59},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1633,
MONTH = jul,
YEAR = 1999,
ADDRESS = {Trento, Italy}
}
@inproceedings{Hosabettu:CHARME99,
TITLE = {Proof of Correctness of a Processor Implementing {Tomasulo's}
Algorithm without a Reorder Buffer},
AUTHOR = {Ravi Hosabettu and Ganesh Gopalakrishnan and Mandayam
Srivas},
BOOKTITLE = {Advances in Hardware Design and Verification: {IFIP
WG10.5} International Conference on Correct Hardware
Design and Verification Methods (CHARME '99)},
PAGES = {8--22},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1703,
MONTH = sep,
YEAR = 1999,
ADDRESS = {Bad Herrenalb, Germany}
}
@inproceedings{Hosabettu-etal00:CAV,
TITLE = {Verifying Microarchitectures that Support Speculation
and Exceptions},
AUTHOR = {Ravi Hosabettu and Ganesh Gopalakrishnan and Mandayam
Srivas},
BOOKTITLE = {Computer-Aided Verification, CAV '2000},
EDITOR = {E. A. Emerson and A. P. Sistla},
PAGES = {521--537},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1855,
MONTH = jul,
YEAR = 2000,
ADDRESS = {Chicago, IL}
}
@inproceedings{Johnson94:TPCD,
TITLE = {Studies of the Single-Pulser in Various Reasoning Systems},
AUTHOR = {Steven D. Johnson and Paul S. Miner and Albert Camlleri},
BOOKTITLE = {Theorem Provers in Circuit Design ({TPCD} '94)},
EDITOR = {Ramayya Kumar and Thomas Kropf},
PAGES = {126--145},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 910,
MONTH = sep,
YEAR = 1994,
ADDRESS = {Bad Herrenalb, Germany}
}
@inproceedings{Johnson&Miner97,
TITLE = {Integrated Reasoning Support in System Design: Design
Derivation and Theorem Proving},
AUTHOR = {Steven D. Johnson and Paul S. Miner},
BOOKTITLE = {Advances in Hardware Design and Verification: {IFIP
WG10.5} International Conference on Correct Hardware
Design and Verification Methods (CHARME)},
EDITOR = {Hon F. li and David K. Probst},
PAGES = {255--272},
PUBLISHER = {Chapman \& Hall},
MONTH = oct,
YEAR = 1997,
ADDRESS = {Montreal, Canada}
}
@inproceedings{Leathrum97:LFM,
TITLE = {Fundamental Hardware Design in {PVS}},
AUTHOR = {James {Leathrum, Jr.}},
BOOKTITLE = {LFM' 97: Fourth NASA Langley Formal Methods Workshop},
EDITOR = {C. Michael Holloway and Kelly J. Hayhurst},
PAGES = {193--204},
SERIES = {NASA Conference Publication 3356},
MONTH = sep,
YEAR = 1997,
ORGANIZATION = {NASA Langley Research Center},
ADDRESS = {Hampton, VA},
NOTE = {Available at \url{http://atb-www.larc.nasa.gov/Lfm97/proceedings/}}
}
@inproceedings{Li-etal97,
TITLE = {Proving the Correctness of the Interlock Mechanism in
Processor Design},
AUTHOR = {Xiaoshan Li and Antonio Cau and Ben Moszkowski and
Nick Coleman and Hussein Zedan},
BOOKTITLE = {Advances in Hardware Design and Verification: {IFIP
WG10.5} International Conference on Correct Hardware
Design and Verification Methods (CHARME)},
EDITOR = {Hon F. li and David K. Probst},
PAGES = {5--22},
PUBLISHER = {Chapman \& Hall},
MONTH = oct,
YEAR = 1997,
ADDRESS = {Montreal, Canada}
}
@inproceedings{Miner&Johnson96,
TITLE = {Verification of an Optimized Fault-Tolerant Clock Synchronization
Circuit: A case study exploring the boundary between
formal reasoning systems},
AUTHOR = {Paul S. Miner and Steven D. Johnson},
BOOKTITLE = {Designing Correct Circuits},
EDITOR = {Mary Sheeran and Satnam Singh},
PUBLISHER = {Electronic Workshops in Computing (\url{http://ewic.org.uk/ewic/})},
MONTH = sep,
YEAR = 1996,
ADDRESS = {Bastad, Sweden}
}
@inproceedings{Miner94:circuit,
TITLE = {Interaction of Formal Design Systems in the Development
of a Fault-Tolerant Clock Synchronization Circuit},
AUTHOR = {Paul S. Miner and Shyamsundar Pullela and Steven D.
Johnson},
BOOKTITLE = {13th Symposium on Reliable Distributed Systems},
PAGES = {128--137},
MONTH = oct,
YEAR = 1994,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Dana Point, CA}
}
@inproceedings{Miner96:FMCAD,
TITLE = {Verification of {IEEE} Compliant Subtractive Division
Algorithms},
AUTHOR = {Paul S. Miner and James F. {Leathrum, Jr.}},
BOOKTITLE = {Formal Methods in Computer-Aided Design (FMCAD '96)},
EDITOR = {Mandayam Srivas and Albert Camilleri},
PAGES = {64--78},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1166,
MONTH = nov,
YEAR = 1996,
ADDRESS = {Palo Alto, CA}
}
@inproceedings{Miller&Srivas95,
TITLE = {Formal Verification of the {AAMP5} Microprocessor: A
Case Study in the Industrial Use of Formal Methods},
AUTHOR = {Steven P. Miller and Mandayam Srivas},
BOOKTITLE = {WIFT '95: Workshop on Industrial-Strength Formal
Specification Techniques},
PAGES = {2--16},
YEAR = 1995,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Boca Raton, FL}
}
@inproceedings{Pnueli98:FMCAD,
TITLE = {Verification of Data-Insensitive Circuits: An In-Order-Retirement
Case Study},
AUTHOR = {Amir Pnueli and Tamara Arons},
BOOKTITLE = {Formal Methods in Computer-Aided Design (FMCAD '98)},
EDITOR = {Ganesh Gopalakrishnan and Phillip Windley},
PAGES = {351--368},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1522,
MONTH = nov,
YEAR = 1998,
ADDRESS = {Palo Alto, CA}
}
@inproceedings{Ruess96:CAV,
TITLE = {Modular Verification of {SRT} Division},
AUTHOR = {H. Rue{\ss} and N. Shankar and M. K. Srivas},
BOOKTITLE = {Computer-Aided Verification, CAV '96},
EDITOR = {Rajeev Alur and Thomas A. Henzinger},
PAGES = {123--134},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1102,
MONTH = {July/August},
YEAR = 1996,
ADDRESS = {New Brunswick, NJ}
}
@article{Ruess99:FMSD,
TITLE = {Modular Verification of {SRT} Division},
AUTHOR = {H. Rue{\ss} and N. Shankar and M. K. Srivas},
JOURNAL = {Formal Methods in Systems Design},
PAGES = {45--73},
VOLUME = 14,
NUMBER = 1,
MONTH = jan,
YEAR = 1999
}
@inproceedings{Sree97:AMAST,
TITLE = {{ATM} Switch Design: Parametric High-Level Modeling
and Formal Verification},
AUTHOR = {Sreeranga P. Rajan and Masahiro Fujita},
BOOKTITLE = {Algebraic Methodology and Software Technology, {AMAST}'97},
EDITOR = {Michael Johnson},
PAGES = {437--450},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1349,
MONTH = dec,
YEAR = 1997,
ADDRESS = {Sydney, Australia}
}
@article{Sree98:todaes,
TITLE = {{ATM} Switch Design by High Level Modeling, Formal Verification,
and High Level Synthesis},
AUTHOR = {S. P. Rajan and M. Fujita and K. Yuan and M. T-C. Lee},
JOURNAL = {ACM Transactions on Design Automation of Electronic
Systems (TODAES)},
PAGES = {554--562},
VOLUME = 3,
NUMBER = 4,
MONTH = oct,
YEAR = 1998
}
@inproceedings{Srivas&Miller95:chdl,
TITLE = {Applying Formal Verification to a Commercial Microprocessor},
AUTHOR = {Mandayam K. Srivas and Steven P. Miller},
BOOKTITLE = {{CHDL '95}: 12th Conference on Computer Hardware
Description Languages and their Applications},
EDITOR = {Steven D. Johnson},
PAGES = {493--502},
MONTH = aug,
YEAR = 1995,
ORGANIZATION = {Proceedings published in a single volume jointly
with ASP-DAC '95, CHDL '95, and VLSI '95, IEEE Catalog
no.\ 95TH8102},
ADDRESS = {Chiba, Japan}
}
@incollection{Srivas&Miller95:inbook,
TITLE = {Formal Verification of the {AAMP5} Microprocessor},
AUTHOR = {Mandayam K. Srivas and Steven P. Miller},
BOOKTITLE = {Applications of Formal Methods},
CHAPTER = 7,
EDITOR = {Michael G. Hinchey and Jonathan P. Bowen},
PAGES = {125--180},
PUBLISHER = {Prentice Hall},
SERIES = {Prentice Hall International Series in Computer Science},
YEAR = 1995,
ADDRESS = {Hemel Hempstead, UK}
}
@article{Srivas&Miller96:FMSD,
TITLE = {Applying Formal Verification to the {AAMP5} Microprocessor:
A Case Study in the Industrial Use of Formal Methods},
AUTHOR = {Mandayam K. Srivas and Steven P. Miller},
JOURNAL = {Formal Methods in Systems Design},
PAGES = {153--188},
VOLUME = 8,
NUMBER = 2,
MONTH = mar,
YEAR = 1996
}
@article{Mansouri00:FMSD,
TITLE = {Automated Correctness Condition Generation for Formal
Verification of Synthesized {RTL} Designs},
AUTHOR = {Nazanin Mansouri and Ranga Vemuri},
JOURNAL = {Formal Methods in Systems Design},
PAGES = {59--91},
VOLUME = 16,
NUMBER = 1,
MONTH = jan,
YEAR = 2000
}
@inproceedings{Naren98:ICCD,
TITLE = {Theorem Proving Guided Development of Formal Assertions
in a Resource-Constrained Scheduler for High-Level Synthesis},
AUTHOR = {Naren Narasimhan and Elena Teica and Rajesh Radhakrishnan
and Sriram Govindarajan and Ranga Vemuri},
BOOKTITLE = {International Conference on Computer Design ({ICCD}'98)},
EDITOR = {Andreas Kuehlmann},
MONTH = oct,
YEAR = 1998,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Austin, TX}
}
@inproceedings{Naren98:tphols,
TITLE = {On the Effectiveness of Theorem Proving Guided Discovery
of Formal Assertions for a Register Allocator in a High-Level
Synthesis System},
AUTHOR = {Naren Narasimhan and Ranga Vemuri},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 11th International
Conference, {TPHOLs '98}},
EDITOR = {Jim Grundy and Malcolm Newey},
PAGES = {367--386},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1479,
MONTH = sep,
YEAR = 1998,
ADDRESS = {Canberra, Australia}
}
@techreport{Sree94:Philips,
TITLE = {Transformations in High Level Synthesis: Specification
and Verification},
AUTHOR = {P. Sreeranga Rajan},
NUMBER = {NL-TN 118/94},
MONTH = apr,
YEAR = 1994,
INSTITUTION = {Philips Research Laboratories},
ADDRESS = {Eindhoven, The Netherlands},
NOTE = {Revised version available as SRI Technical Report SRI-CSL-94-10,
October 1994}
}
@inproceedings{Sree95:chdl,
TITLE = {Correctness of Transformations in High Level Synthesis},
AUTHOR = {Sreeranga P. Rajan},
BOOKTITLE = {{CHDL '95}: 12th Conference on Computer Hardware
Description Languages and their Applications},
EDITOR = {Steven D. Johnson},
PAGES = {597--603},
MONTH = aug,
YEAR = 1995,
ORGANIZATION = {Proceedings published in a single volume jointly
with ASP-DAC '95, CHDL '95, and VLSI '95, IEEE Catalog
no.\ 95TH8102},
ADDRESS = {Chiba, Japan}
}
@phdthesis{Sree:thesis,
TITLE = {Transformations on Dependency Graphs: Formal Specification
and Efficient Mechanical Verification},
AUTHOR = {Sreeranga P. Rajan},
MONTH = oct,
YEAR = 1995,
SCHOOL = {Department of Computer Science, University of British
Columbia},
ADDRESS = {Vancouver, Canada}
}
@inproceedings{Nalumasu&Ganesh98,
TITLE = {Deriving Efficient Cache Coherence Protocols Through
Refinement},
AUTHOR = {Ratan Nalumasu and Ganesh Gopalakrishnan},
BOOKTITLE = {Formal Methods for Parallel Programming: Theory
and Applications {(FMPPTA)}},
MONTH = mar,
YEAR = 98,
ADDRESS = {Orlando, FL},
NOTE = {Available at \url{http://www.loria.fr/~mery/lncs_fmppta98/paper7.ps}}
}
@phdthesis{Park:thesis,
TITLE = {Computer Assisted Analysis of Multiprocessor Memory
Systems},
AUTHOR = {Seungjoon Park},
MONTH = jun,
YEAR = 1996,
SCHOOL = {Department of Electrical Engineering, Stanford University}
}
@unpublished{Park&Dill96:PDS,
TITLE = {An Executable Specification, Analyzer and Verifier for
Relaxed Memory Order: With Formal Proofs},
AUTHOR = {Seungjoon Park and David L. Dill},
YEAR = 1996,
NOTE = {Submitted for publication; an earlier version (without
proofs) is available~\cite{Park&Dill95:spaa}}
}
@article{Park&Dill98:TCS,
TITLE = {Verification of Cache Coherence Protocols by Aggregation
of Distributed Transactions},
AUTHOR = {Seungjoon Park and David L. Dill},
JOURNAL = {Theory of Computing Systems},
PAGES = {355--376},
VOLUME = 31,
NUMBER = 4,
YEAR = 1998
}
@inproceedings{Rajan95:multimedia,
TITLE = {A Formal Basis for Structured Multimedia Collaborations},
AUTHOR = {Sreeranga Rajan and P. Venkat Rangan and Harrick M.
Vin},
BOOKTITLE = {Proceedings of the 2nd IEEE International Conference
on Multimedia Computing and Systems},
PAGES = {194--201},
MONTH = may,
YEAR = 1995,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Washington, DC}
}
@inproceedings{rbj00,
TITLE = {An Approach to Symbolic Test Generation},
AUTHOR = {V. Rusu and L. du Bousquet and T. J\'{e}ron},
BOOKTITLE = {2nd International Workshop on Integrated Formal
Method (IFM'00)},
PAGES = {338-357},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
NUMBER = 1945,
MONTH = nov,
YEAR = 2000,
ADDRESS = {Dagstuhl, Germany}
}
@inproceedings{Graham96,
TITLE = {A Method for the Formal Testing of Program Visualization
Tools},
AUTHOR = {T. C. Nicholas Graham},
BOOKTITLE = {Proceedings of the Fourth Workshop on Program Comprehension},
PAGES = {45--54},
PUBLISHER = {IEEE Computer Society},
MONTH = mar,
YEAR = 1996,
ADDRESS = {Berlin, Germany}
}
@inproceedings{Suri&Sinha98,
TITLE = {On the Use of Formal Methods for Validation},
AUTHOR = {Neeraj Suri and Purnendu Sinha},
BOOKTITLE = {Fault Tolerant Computing Symposium 28},
PAGES = {390--399},
MONTH = jun,
YEAR = 1998,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Munich, Germany}
}
@inproceedings{Sinha&Suri99:FTCS,
TITLE = {Identification of Test Cases Using a Formal Fault Injection
Approach},
AUTHOR = {Purnendu Sinha and Neeraj Suri},
BOOKTITLE = {Fault Tolerant Computing Symposium 29},
PAGES = {314--321},
MONTH = jun,
YEAR = 1999,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Madison, WI}
}
@inproceedings{Sinha&Suri99:RTSS,
TITLE = {Formal Techniques for Dependable Real Time Protocols},
AUTHOR = {Purnendu Sinha and Neeraj Suri},
BOOKTITLE = {Real Time Systems Symposium},
MONTH = dec,
YEAR = 1999,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Phoenix, AZ}
}
@inproceedings{Qadeer&Shankar98,
TITLE = {Verifying a Self-Stabilizing Mutual Exclusion Algorithm},
AUTHOR = {Shaz Qadeer and Natarajan Shankar},
BOOKTITLE = {IFIP International Conference on Programming Concepts
and Methods (PROCOMET '98)},
EDITOR = {David Gries and Willem-Paul de Roever},
PAGES = {424--443},
PUBLISHER = {Chapman \& Hall},
MONTH = jun,
YEAR = 1998,
ADDRESS = {Shelter Island, NY}
}
@inproceedings{Kulkarni99:SSS,
TITLE = {A Case Study in Component-based Mechanical Verification
of Fault-Tolerant Programs},
AUTHOR = {Sandeep Kulkarni and John Rushby and N. Shankar},
BOOKTITLE = {{ICDCS} Workshop on Self-Stabilizing Systems},
PAGES = {33--40},
MONTH = jun,
YEAR = 1999,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Austin, TX}
}
@inproceedings{Gargantini&Riccobene00:ASM,
TITLE = {Encoding {Abstract State Machines} in {PVS}},
AUTHOR = {Angelo Gargantini and Elvinia Riccobene},
BOOKTITLE = {Abstract State Machines: Theory and Applications
({ASM} 2000)},
EDITOR = {Yuri Gurevich and Phillip W. Kutter and Martin Odersky
and Lothar Thiele},
PAGES = {303--322},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
NUMBER = 1912,
MONTH = mar,
YEAR = 2000,
ADDRESS = {Monte Verit\`{a}, Switzerland}
}
@inproceedings{Bodeveix-etal99,
TITLE = {A Formalization of the {B-Method} in {Coq} and {PVS}},
AUTHOR = {Jean Paul Bodeveix and Mamoun Filali and C\'{e}sar
A. Mu{\~{n}}oz},
BOOKTITLE = {FM99: The World Congress in Formal Methods, User
Group Meeting 2. The B-Method: Applying B in an Industrial
Context: Tools, Lessons and Techniques},
MONTH = sep,
YEAR = 1999,
NOTE = {Available on the CD-ROM for \cite{FM99}}
}
@inproceedings{Munoz&Rushby:FM99,
TITLE = {Structural Embeddings: Mechanization with Method},
AUTHOR = {C\'{e}sar Mu{\~{n}}oz and John Rushby},
BOOKTITLE = {FM99: The World Congress in Formal Methods},
EDITOR = {Jeannette Wing and Jim Woodcock},
PAGES = {452--471},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1708 and 1709},
MONTH = sep,
YEAR = 1999,
ADDRESS = {Toulouse, France},
NOTE = {Pages 1--938 are in the first volume, 939--1872 in the
second.}
}
@inproceedings{Paige&Ostroff:FM99,
TITLE = {Developing {BON} as an Industrial-Strength Formal Method},
AUTHOR = {Richard F. Paige and Jonathan S. Ostroff},
BOOKTITLE = {FM99: The World Congress in Formal Methods},
EDITOR = {Jeannette Wing and Jim Woodcock},
PAGES = {834--853},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1708 and 1709},
MONTH = sep,
YEAR = 1999,
ADDRESS = {Toulouse, France},
NOTE = {Pages 1--938 are in the first volume, 939--1872 in the
second.}
}
@inproceedings{Bensalem99:DCCA,
TITLE = {A Methodology for Proving Control Systems with {Lustre}
and {PVS}},
AUTHOR = {S. Bensalem and P. Caspi and C. Parent-Vigouroux and
C. Dumas},
BOOKTITLE = {Dependable Computing for Critical Applications---7},
EDITOR = {Charles B. Weinstock and John Rushby},
PAGES = {89--107},
PUBLISHER = {IEEE Computer Society},
SERIES = {Dependable Computing and Fault Tolerant Systems},
VOLUME = 12,
MONTH = jan,
YEAR = 1999,
ADDRESS = {San Jose, CA}
}
@inproceedings{Rushby&Srivas:HOL93,
TITLE = {Using {PVS} to Prove Some Theorems of {David Parnas}},
AUTHOR = {John Rushby and Mandayam Srivas},
BOOKTITLE = {Higher Order Logic Theorem Proving and its Applications
(6th International Workshop, HUG '93)},
EDITOR = {Jeffrey J. Joyce and Carl-Johan H. Seger},
PAGES = {163--173},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 780,
MONTH = aug,
YEAR = 1993,
ADDRESS = {Vancouver, Canada}
}
@inproceedings{Heimdahl&Czerny96,
TITLE = {Using {PVS} to Analyze Hierarchical State-Based Requirements
for Completeness and Consistency},
AUTHOR = {Mats P. E. Heimdahl and Barbara J. Czerny},
BOOKTITLE = {IEEE High-Assurance Systems Engineering Workshop
(HASE '96)},
PAGES = {252--262},
MONTH = oct,
YEAR = 1996,
ADDRESS = {Niagara on the Lake, Canada}
}
@inproceedings{Heimdahl97:LFM,
TITLE = {Verifying Communication Related Safety Constraints in
{RSML} Specifications},
AUTHOR = {Mats P.E. Heimdahl},
BOOKTITLE = {LFM' 97: Fourth NASA Langley Formal Methods Workshop},
EDITOR = {C. Michael Holloway and Kelly J. Hayhurst},
PAGES = {115--128},
SERIES = {NASA Conference Publication 3356},
MONTH = sep,
YEAR = 1997,
ORGANIZATION = {NASA Langley Research Center},
ADDRESS = {Hampton, VA},
NOTE = {Available at \url{http://atb-www.larc.nasa.gov/Lfm97/proceedings/}}
}
@inproceedings{Heimdahl97:ICFEM,
TITLE = {Specification and Analysis of System Level Inter-Component
Communication},
AUTHOR = {Mats P. E. Heimdahl and Jeffrey M. Thompson},
BOOKTITLE = {First International Conference on Formal Engineering
Methods (ICFEM '97)},
EDITOR = {Michael G. Hinchey and Shaoying Liu},
PAGES = {192--201},
MONTH = nov,
YEAR = 1997,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Hiroshima, Japan}
}
@inproceedings{Czerny&Heimdahl:ASE98,
TITLE = {Automated Integrative Analysis of State-based Requirements},
AUTHOR = {Barbara J. Czerny and Mats P. E. Heimdahl},
BOOKTITLE = {Thirteenth IEEE Conference on Automated Software
Engineering ({ASE '98})},
EDITOR = {D. Redmiles and B. Nuseibeh},
MONTH = oct,
YEAR = 1998,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Nonolulu, Hawaii}
}
@article{Heimdahl98:computer,
TITLE = {Specification and Analysis of Intercomponent Communication},
AUTHOR = {Mats P. E. Heimdahl and Jeffrey M. Thompson and Barbara
J. Czerny},
JOURNAL = {IEEE Computer},
PAGES = {47--54},
VOLUME = 31,
NUMBER = 4,
MONTH = apr,
YEAR = 1998
}
@inproceedings{Agerholm96,
TITLE = {Translating Specifications in {VDM-SL} to {PVS}},
AUTHOR = {Sten Agerholm},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 9th International
Conference, {TPHOLs '96}},
EDITOR = {Joakim von Wright and Jim Grundy and John Harrison},
PAGES = {1--16},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1125,
MONTH = aug,
YEAR = 1996,
ADDRESS = {Turku, Finland}
}
@incollection{Agerholm97:VDMbook,
TITLE = {On the Verification of {VDM} Specification and Refinement
with {PVS}},
AUTHOR = {Sten Agerholm and Juan Bicarregui and Savi Maharaj},
BOOKTITLE = {Proof in {VDM}: Case Studies},
CHAPTER = 6,
EDITOR = {Juan Bicarregui},
PAGES = {157--190},
PUBLISHER = {Springer-Verlag},
SERIES = {FACIT (Formal Approaches to Computing and Information
Technology)},
YEAR = 1997,
ADDRESS = {London, UK}
}
@inproceedings{Maharaj97:ASE,
TITLE = {On the Verification of {VDM} Specification and Refinement
with {PVS}},
AUTHOR = {Savi Maharaj and Juan Bicarregui},
BOOKTITLE = {12th IEEE International Conference on Automated
Software Engineering ({ASE '97})},
EDITOR = {M. Lowry and Y. Ledru},
PAGES = {280--289},
MONTH = nov,
YEAR = 1997,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Incline Village, NV}
}
@inproceedings{Alexander-etal:FM99,
TITLE = {A Brief Summary of {VSPEC}},
AUTHOR = {Perry Alexander and Murali Rangarajan and Phillip Baraona},
BOOKTITLE = {FM99: The World Congress in Formal Methods},
EDITOR = {Jeannette Wing and Jim Woodcock},
PAGES = {1068--1086},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1708 and 1709},
MONTH = sep,
YEAR = 1999,
ADDRESS = {Toulouse, France},
NOTE = {Pages 1--938 are in the first volume, 939--1872 in the
second.}
}
@inproceedings{Adams-etal:CADE99,
TITLE = {{VSDITLU}: A Verifiable Symbolic Definite Integral Table
Look-Up},
AUTHOR = {A. A. Adams and H. Gottliebsen and S. A. Linton and
U. Martin},
BOOKTITLE = {Automated Deduction---{CADE-16}},
PAGES = {112--126},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = 1632,
MONTH = jul,
YEAR = 1999,
ADDRESS = {Trento, Italy}
}
@inproceedings{Adams-etal:ISSAC99,
TITLE = {Automated Theorem Proving in Support of Computer Algebra:
Symbolic Definite Integration as a Case Study},
AUTHOR = {A. A. Adams and H. Gottliebsen and S. A. Linton and
U. Martin},
BOOKTITLE = {Proceedings of the 1999 International Symposium
on Symbolic and Algebraic Computation, ({ISSAC '99})},
PAGES = {253--260},
MONTH = jul,
YEAR = 1999,
ORGANIZATION = {Association for Computing Machinery},
ADDRESS = {Vancouver, B.C., Canada}
}
@inproceedings{Buth98:TOOLS96,
TITLE = {Combining Tools for the Verification of Fault-Tolerant
Systems},
AUTHOR = {Bettina Buth and Rachel Cardell-Oliver and Jan Peleska},
BOOKTITLE = {Tools for System Development and Verification},
EDITOR = {Bettina Buth and Rudolf Berghammer and Jan Peleska},
PAGES = {41--69},
PUBLISHER = {Shaker Verlag},
SERIES = {BISS Monographs},
YEAR = 1998,
ADDRESS = {Aachen, Germany},
NOTE = {Proceedings of a workshop held at Bremen in 1996}
}
@inproceedings{Buth98:tools,
TITLE = {{PAMELA} + {PVS}},
AUTHOR = {Bettina Buth},
BOOKTITLE = {Tool Support for System Specification, Development,
and Verification},
EDITOR = {Rudolph Berghammer and Yassine Lakhnech},
PAGES = {62--76},
PUBLISHER = {Springer-Verlag},
SERIES = {Advances in Computing Science},
MONTH = jun,
YEAR = 1998,
ADDRESS = {Malente, Germany},
NOTE = {Proceedings published in May 1999}
}
@inproceedings{Buth97:AMAST,
TITLE = {{PAMELA $+$ PVS}},
AUTHOR = {Bettina Buth},
BOOKTITLE = {Algebraic Methodology and Software Technology, {AMAST}'97},
EDITOR = {Michael Johnson},
PAGES = {560--562},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1349,
MONTH = dec,
YEAR = 1997,
ADDRESS = {Sydney, Australia}
}
@inproceedings{Corbett-etal00:ICSE,
TITLE = {Bandera: Extracting Finite-state Models from {Java}
Source Code},
AUTHOR = {James Corbett and Matthew Dwyer and John Hatcliff and
Corina Pasareanu and Robby and Shawn Laubach and Hongjun
Zheng},
BOOKTITLE = {22nd International Conference on Software Engineering},
PAGES = {439--448},
MONTH = jun,
YEAR = 2000,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Limerick, Ireland}
}
@proceedings{Compass89,
TITLE = {COMPASS '89 (Proceedings of the Fourth Annual Conference
on Computer Assurance)},
BOOKTITLE = {COMPASS '89 (Proceedings of the Fourth Annual Conference
on Computer Assurance)},
MONTH = jun,
YEAR = 1989,
ORGANIZATION = {IEEE Washington Section},
ADDRESS = {Gaithersburg, MD}
}
@proceedings{FTCS-highlights,
TITLE = {Fault Tolerant Computing Symposium 25: Highlights from
25 Years},
BOOKTITLE = {Fault Tolerant Computing Symposium 25: Highlights
from 25 Years},
PUBLISHER = {IEEE Computer Society},
MONTH = jun,
YEAR = 1995,
ORGANIZATION = {IEEE Computer Society},
ADDRESS = {Pasadena, CA}
}
@article{Saiedian96,
TITLE = {An Invitation to Formal Methods},
AUTHOR = {Hossein {Saiedian (Ed.)}},
JOURNAL = {IEEE Computer},
PAGES = {16--30},
VOLUME = 29,
NUMBER = 4,
MONTH = apr,
YEAR = 1996,
NOTE = {A ``roundtable'' of short articles by several authors.}
}
@proceedings{Encress95,
TITLE = {Safety and Reliability of Software Based Systems (Twelfth
Annual {CSR} Workshop)},
BOOKTITLE = {Safety and Reliability of Software Based Systems
(Twelfth Annual {CSR} Workshop)},
EDITOR = {Roger Shaw},
PUBLISHER = {Springer},
MONTH = sep,
YEAR = 1995,
ADDRESS = {Bruges, Belgium}
}
@inproceedings{Park&Dill95:spaa,
TITLE = {An Executable Specification, Analyzer and Verifier for
{RMO (Relaxed Memory Order)}},
AUTHOR = {Seungjoon Park and David L. Dill},
BOOKTITLE = {7th ACM Symposium on Parallel Algorithms and Architectures},
PAGES = {34--51},
MONTH = jul,
YEAR = 1995
}
@proceedings{FM99,
TITLE = {FM99: The World Congress in Formal Methods},
BOOKTITLE = {FM99: The World Congress in Formal Methods},
EDITOR = {Jeannette Wing and Jim Woodcock},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1708 and 1709},
MONTH = sep,
YEAR = 1999,
ADDRESS = {Toulouse, France},
NOTE = {Pages 1--938 are in the first volume, 939--1872 in the
second.}
}