PVS Bibliography
John Rushby
Computer Science Laboratory
SRI International
Menlo Park CA 94025 USA
Email: pvs-request@csl.sri.com
WWW: http://www.csl.sri.com/pvs.html
November 29, 2000
This bibliography lists most of the publications that I am aware of
concerning the development and application of the PVS verification system
and its predecessors. The files used to create this report, including the
BibTEX bibliography, are available at
http://www.csl.sri.com/pvs-bib.html. PVS users are encouraged to
use the BibTEX entries from these files, which are as accurate, complete,
and up to date as I can make them.
I have limited this list to publications that should be available in a
university or research library. For this reason, I have omitted citations to
conference proceedings that were not issued by a technical society or
commercial publisher, unless they are on the Web; similarly, technical
reports are cited only when they are widely distributed (e.g., NASA), or
where there is no other source and they are are on the Web (or otherwise
freely available, if they predate the Web). Many of the journal and
conference papers listed are supported by technical reports that provide
much more detail; I am willing to add these if there is demand. Because
papers are often available on the web in advance of the journal or
proceedings in which they will appear, I now include such papers and mark
them "to appear."
Most of the publications later than about 1990, and some earlier ones, are
available on the Web from http://www.csl.sri.com/fm-papers.html
(for SRI papers) or http://www.csl.sri.com/pvs-users.html (for
others); hard copies of all these papers are available at SRI. Many papers
are archived at the NECI Scientific Literature Digital Library
http://citeseer.nj.nec.com/cs and at The Hypatia Digital Library at
1
http://hypatia.dcs.qmw.ac.uk/ or can be found on the authors' home
pages, which can usually be tracked down using a search engine such as
www.google.com.
Please keep me informed of new papers (or forgotten historical ones) that
should be added to this collection, and of any inaccuracies.
History
PVS is the most recent in a line of specification languages, theorem
provers, and verification systems developed at SRI that goes back over 20
years. Early systems included the Jovial Verification System [1] (Jovial was
a language based on Algol 58, a precursor to the more famous Algol 60,
that was used by the US Air Force), and the Hierarchical Development
Methodology (HDM) [2-4]. HDM had a "security analyzer" [5] based on
information flow [6] that was used in the verification of the Honeywell
SCOMP [7, 8] (the first computer to gain the NSA's A1 [9] rating) and
several other secure systems [10, 11].
The HDM security flow analyzer used the Boyer-Moore theorem prover,
much of whose early development was performed at SRI [12]. A parallel
development was Shostak's Theorem Prover STP [13], which was based on
his decision procedures [14-18] and used in the analysis of some aspects of
the SIFT flight control computer [19, 20] (note 1) and early experiments in
hardware verification [23].
HDM and STP were the main design influences on "Enhanced HDM"
(Ehdm), whose development began in 1983. Ehdm introduced the
higher-order specification language with theory-level (they are called
"modules" in Ehdm) parameterization that provides much of the
foundation for the PVS language. Ehdm was operational by 1985 [24-26]
and was further developed through the following decade [27, 28] (note 2).
Verification of fault-tolerant algorithms and architectures provided the
biggest applications of Ehdm [29-35], and some small experiments in
hardware verification [36, 37] were also performed.
____________________________________
1. Although the SIFT verification was a significant accomplishment at
the time, the paper describing it [21] leaves the impression that the
full operating system was verified, as opposed to some properties of
its design. This led to severe criticism by a NASA peer review [22].
2. Ehdm has some capabilities currently lacking in PVS: for example,
hierarchical development based on theory interpretations, imperative
program verification using a small subset of a Pascal-like language, a
superior prover interface (to an interactive prover derived from
that of PVS) and more capable (though slower) arithmetic decision
procedures. However, it lacks some of the linguistic capabilities of
PVS: for example, dependent typing, abstract data types, inductive
relations, and several type constructors. Ehdm continues to be
available, but its distribution is controlled by the US Government.
2
PVS was started in late 1990 as an SRI-funded research program to
prototype ideas for an interactive prover for Ehdm and the design of a
"next generation" verification system (hence its original name: "Prototype
Verification System"). SRI made the first version of PVS freely available in
1993 [38] and it proved so popular that we have continued to develop it
ever since (first with SRI IR&D funds, and later with additional support
from NASA, NRL, AFOSR, ARPA, and NSF).
Documentation and Availability
PVS is freely available under license from SRI. Information, examples,
papers, documentation, and the system itself are available from the PVS
home page at http://www.csl.sri.com/pvs.html and the CSL ftp server
at ftp://ftp.csl.sri.com/pub/pvs, and from mirror sites in England,
France, Germany, and Japan (note 3).
The PVS system is described briefly in three system descriptions [39-41]
and an experience report [42] and fully documented in separate manuals
for the language [43], prover [44], system [45], and semantics [46]. Some of
the motivation and design decisions for PVS are described in [47], and the
utility of its type system is argued in [48, 49]. Tutorials provide general
introductions to PVS [50-52], plus more specialized treatments for
hardware [53], abstract data types [54], tabular and requirements
specifications [55], and distributed systems [56, 57]. General introductions
to formal methods, with PVS examples, are provided by the NASA
Guidebook series [58, 59].
Methodology and Technology
Some of the philosophical and methodological ideas behind PVS and its
applications are described in [60-71], while issues in the application of
formal methods to safety-critical systems are described in [58, 72-74] and
hardware verification is discussed in [75].
The theorem-proving techniques employed in PVS are described
in [76-81], and their integration with model checking and with tabular
specifications are described in [82] and [83], respectively. Use of a decision
procedure for WS1S within PVS is described in [84] Experimental support
for efficient evaluation and its use to support reflection in PVS are
described in [85, 86], while the very efficient evaluator built-in to PVS 2.3 is
____________________________________
3. These sites are ftp://ftp.cs.york.ac.uk/pub/pvs at the University
of York, England; ftp://ftp.ibp.fr/pub/pvs at the University of
Paris VI, France; ftp://ftp. informatik.uni-ulm.de/pub/KI/pvs at the
University of Ulm, Germany; and ftp:
//nicosia.is.s.u-tokyo.ac.jp/pub/misc/pvs at Tokyo University, Japan.
3
described in [87]. Techniques and tools to support automated generation of
abstractions and invariants in PVS are described in [88-100] and the
integration of these capabilities in extensions to PVS such as SAL and
InVeST are described in [101-106].
Comparisons between PVS and ACL2 treatments of an interactive
consistency algorithm [107], and between PVS and HOL specifications of
the IEEE 854 floating-point standard [108] are available, while Mike
Gordon provides a discussion of PVS from a HOL perspective [109] and
David Griffioen and Marieke Huisman compare PVS and
Isabelle/HOL [110]. Jan Friso Groote, Fran cois Monin and Jaco van de
Pol provide a tutorial on protocol and distributed systems verification that
considers Isabelle, Coq, and PVS, and makes some comparison between the
systems [111], while Kern and Greenstreet survey several methods for
hardware verification, including PVS [112]. Heinrich Rust presents a PVS
treatment for an "invoicing" example used in the comparison of many
systems [113]. Matt Wilding describes an approach, derived from those
used with Nqthm and ACL2, for developing robust proofs of machine code
programs [114]. Georg Droschl compares some aspects of PVS and VDM
on an industrially-motivated example [115, 116]. Merriam and Harrison
provide an examination of interface issues, and compare PVS with two
other systems [117], while Archer and Heitmeyer describe using PVS to
produce "human-style" proofs [118, 119]. Issues in introducing formal
methods, including PVS, to students and engineers are discussed by Knight
et al [120].
Applications
PVS has been applied to classical topics in mathematical analysis (with
applicaiton to computer algebra systems) [121, 122], to the modeling of
process calculi [123, 124] and transition systems [125, 126], to the
specification of abstract datatypes [127-129], classes in object-oriented
languages [130-133], and Java programs [134-136], to critical algorithms
for fault tolerance in automobile and aircraft control systems [137-145], to
partitioning in these systems [146-148] to software requirements and
software design for aircraft [149-151] and for manned [152-159] and
interplanetary [160-162] spacecraft, to aircraft trajectories [163, 164] to
protection systems for nuclear power plants [165, 166], to command and
control [167], to issues in computer security [168-170], active
networks [171], and cryptographic protocols [172-175], to operating
systems [176], distributed algorithms [177-189], real-time and
scheduling [190-212], reactive [213], and hybrid systems [214-216], to
embedded systems [217-219], distributed systems [220-228] and
protocols [229-233], to software architecture [234], program
4
development [235-237], software development steps [238-242] and
refinement [243-246], to compilers [247-255], to hardware design [256-284]
and synthesis [285-290], to memory models and cache coherence
protocols [291-294], to multimedia collaborations [295], to test
generation [296] and to testing program visualization tools [297], to
validating fault-tolerant real-time systems [298-300], and to
self-stabilization [301, 302]. PVS has also been used to support other
specification notations including Abstract State Machines (ASMs) [303],
the B Method [304, 305], BON [306], Lustre [307], Tabular
methods [308-313], VDM [314-316], and VSPEC [317], and in conjunction
with computer algebra systems [318, 319], and in combination with other
tools [320-323].
References
[1] B. Elspas, M. Green, M. Moriconi, and R. Shostak. A JOVIAL
verifier. Technical report, Computer Science Laboratory, SRI
International, January 1979.
[2] Lawrence Robinson and Karl N. Levitt. Proof techniques for
hierarchically structured programs. Communications of the ACM,
20(4):271-283, April 1976.
[3] L. Robinson, K. N. Levitt, and B. A. Silverberg. The HDM
Handbook. Computer Science Laboratory, SRI International, Menlo
Park, CA, June 1979. Three Volumes.
[4] Jay M. Spitzen, Karl N. Levitt, and Lawrence Robinson. An example
of hierarchical design and proof. Communications of the ACM,
21(12):1064-1075, December 1978.
[5] R. J. Feiertag. A technique for proving specifications are multilevel
secure. Technical Report CSL-109, Computer Science Laboratory,
SRI International, Menlo Park, CA, January 1980.
[6] R. J. Feiertag, K. N. Levitt, and L. Robinson. Proving multilevel
security of a system design. In Sixth ACM Symposium on Operating
System Principles, pages 57-65, November 1977.
[7] Terry Vickers Benzel. Analysis of a kernel verification. In Proceedings
of the Symposium on Security and Privacy, pages 125-131, Oakland,
CA, April 1984. IEEE Computer Society.
[8] J. M. Silverman. Reflections on the verification of the security of an
operating system kernel. In Ninth ACM Symposium on Operating
5
System Principles, pages 143-154, Bretton Woods, NH, October
1983. (ACM Operating Systems Review, Vol. 17, No. 5).
[9] Department of Defense. Department of Defense Trusted Computer
System Evaluation Criteria, December 1985. DOD 5200.28-STD
(supersedes CSC-STD-001-83).
[10] Kenneth S. Lindsay. A taxonomy of the causes of proof failures in
applications using the HDM methodology. In Fourth Aerospace
Computer Security Applications Conference, pages 419-423, Orlando,
FL, December 1988. IEEE Computer Society. Reprinted
in [324, pp. 79-83].
[11] Bill Smith, Cynthia Reese, Kenneth S. Lindsay, and Brian Crane. A
description of a formal verification and validation (FVV) process. In
Fourth Aerospace Computer Security Applications Conference, pages
401-408, Orlando, FL, December 1988. IEEE Computer Society.
Reprinted in [324, pp. 71-78].
[12] R. S. Boyer and J S. Moore. A Computational Logic. Academic
Press, New York, NY, 1979.
[13] R. E. Shostak, R. Schwartz, and P. M. Melliar-Smith. STP: A
mechanized logic for specification and verification. In D. Loveland,
editor, 6th International Conference on Automated Deduction
(CADE), volume 138 of Lecture Notes in Computer Science, New
York, NY, 1982. Springer-Verlag.
[14] Robert E. Shostak. On the SUP-INF method for proving Presburger
formulas. Journal of the ACM, 24(4):529-543, October 1977.
[15] Robert E. Shostak. An algorithm for reasoning about equality.
Communications of the ACM, 21(7):583-585, July 1978.
[16] Robert E. Shostak. A practical decision procedure for arithmetic with
function symbols. Journal of the ACM, 26(2):351-360, April 1979.
[17] Robert E. Shostak. Deciding linear inequalities by computing loop
residues. Journal of the ACM, 28(4):769-779, October 1981.
[18] Robert E. Shostak. Deciding combinations of theories. Journal of the
ACM, 31(1):1-12, January 1984.
[19] Charles B. Weinstock. SIFT: System design and implementation. In
Fault Tolerant Computing Symposium 10, pages 75-77, Kyoto, Japan,
October 1980. IEEE Computer Society. Reprinted in [325, pp. 29-30].
6
[20] John H. Wensley, Leslie Lamport, Jack Goldberg, Milton W. Green,
Karl N. Levitt, P. M. Melliar-Smith, Robert E. Shostak, and
Charles B. Weinstock. SIFT: Design and analysis of a fault-tolerant
computer for aircraft control. Proceedings of the IEEE,
66(10):1240-1255, October 1978.
[21] P. M. Melliar-Smith and R. L. Schwartz. Formal specification and
verification of SIFT: A fault-tolerant flight control system. IEEE
Transactions on Computers, C-31(7):616-630, July 1982.
[22] NASA Conference Publication 2377. Peer Review of a Formal
Verification/Design Proof Methodology, July 1983.
[23] Robert E. Shostak. Formal verification of circuit designs. In
T. Uehara and M. Barbacci, editors, Computer Hardware Description
Languages, pages 13-29. North-Holland, 1983.
[24] Richard A. Kemmerer. Verification assessment study final report.
Technical Report C3-CR01-86, National Computer Security Center,
Ft. Meade, MD, 1986. 5 Volumes (Overview, Gypsy, Affirm, FDM,
and Ehdm). US distribution only.
[25] P. Michael Melliar-Smith and John Rushby. The Enhanced HDM
system for specification and verification. In Proc. VerkShop III, pages
41-43, Watsonville, CA, February 1985. Published as ACM Software
Engineering Notes, Vol. 10, No. 4, Aug. 85.
[26] John Rushby. The security model of Enhanced HDM. In Proceedings
7th DoD/NBS Computer Security Initiative Conference, pages
120-136, Gaithersburg, MD, September 1984.
[27] F. W. von Henke, J. S. Crow, R. Lee, J. M. Rushby, and R. A.
Whitehurst. The Ehdm verification environment: An overview. In
Proceedings 11th National Computer Security Conference, pages
147-155, Baltimore, MD, October 1988. NBS/NCSC.
[28] John Rushby, Friedrich von Henke, and Sam Owre. An introduction
to formal specification and verification using Ehdm. Technical
Report SRI-CSL-91-2, Computer Science Laboratory, SRI
International, Menlo Park, CA, February 1991.
[29] Ben L. Di Vito and Ricky W. Butler. Formal techniques for
synchronized fault-tolerant systems. In C. E. Landwehr, B. Randell,
and L. Simoncini, editors, Dependable Computing for Critical
Applications_3, volume 8 of Dependable Computing and
Fault-Tolerant Systems, pages 163-188. Springer-Verlag, Vienna,
Austria, September 1992.
7
[30] Paul S. Miner. Verification of fault-tolerant clock synchronization
systems. NASA Technical Paper 3349, NASA Langley Research
Center, Hampton, VA, November 1993.
[31] John Rushby. Formal verification of an Oral Messages algorithm for
interactive consistency. Technical Report SRI-CSL-92-1, Computer
Science Laboratory, SRI International, Menlo Park, CA, July 1992.
Also available as NASA Contractor Report 189704, October 1992.
[32] John Rushby. A fault-masking and transient-recovery model for
digital flight-control systems. In Jan Vytopil, editor, Formal
Techniques in Real-Time and Fault-Tolerant Systems, Kluwer
International Series in Engineering and Computer Science, chapter 5,
pages 109-136. Kluwer, Boston, Dordecht, London, 1993.
[33] John Rushby. A formally verified algorithm for clock synchronization
under a hybrid fault model. In Thirteenth ACM Symposium on
Principles of Distributed Computing, pages 304-313, Los Angeles,
CA, August 1994. Association for Computing Machinery. Also
available as NASA Contractor Report 198289.
[34] John Rushby and Friedrich von Henke. Formal verification of
algorithms for critical systems. IEEE Transactions on Software
Engineering, 19(1):13-23, January 1993.
[35] Natarajan Shankar. Mechanical verification of a generalized protocol
for Byzantine fault-tolerant clock synchronization. In J. Vytopil,
editor, Formal Techniques in Real-Time and Fault-Tolerant Systems,
volume 571 of Lecture Notes in Computer Science, pages 217-236,
Nijmegen, The Netherlands, January 1992. Springer-Verlag.
[36] Ricky W. Butler and Jon A. Sjogren. Formal design verification of
digital circuitry. Reliability Engineering and System Safety, 32:67-93,
1991.
[37] J. Joyce, E. Liu, J. Rushby, N. Shankar, R. Suaya, and F. von Henke.
From formal verification to silicon compilation. In IEEE Compcon,
pages 450-455, San Francisco, CA, February 1991.
[38] N. Shankar, S. Owre, and J. M. Rushby. PVS Tutorial. Computer
Science Laboratory, SRI International, Menlo Park, CA, February
1993. Also appears in Tutorial Notes, Formal Methods Europe '93:
Industrial-Strength Formal Methods, pages 357-406, Odense,
Denmark, April 1993.
[39] S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M.K. Srivas. PVS:
Combining specification, proof checking, and model checking. In
8
Rajeev Alur and Thomas A. Henzinger, editors, Computer-Aided
Verification, CAV '96, volume 1102 of Lecture Notes in Computer
Science, pages 411-414, New Brunswick, NJ, July/August 1996.
Springer-Verlag.
[40] S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype
verification system. In Deepak Kapur, editor, 11th International
Conference on Automated Deduction (CADE), volume 607 of Lecture
Notes in Artificial Intelligence, pages 748-752, Saratoga, NY, June
1992. Springer-Verlag.
[41] N. Shankar. PVS: Combining specification, proof checking, and
model checking. In Mandayam Srivas and Albert Camilleri, editors,
Formal Methods in Computer-Aided Design (FMCAD '96), volume
1166 of Lecture Notes in Computer Science, pages 257-264, Palo
Alto, CA, November 1996. Springer-Verlag.
[42] Sam Owre, John Rushby, N. Shankar, and David Stringer-Calvert.
PVS: an experience report. In Dieter Hutter, Werner Stephan, Paolo
Traverso, and Markus Ullman, editors, Applied Formal
Methods_FM-Trends 98, volume 1641 of Lecture Notes in Computer
Science, pages 338-345, Boppard, Germany, October 1998.
Springer-Verlag.
[43] S. Owre, N. Shankar, J. M. Rushby, and D. W. J. Stringer-Calvert.
PVS Language Reference. Computer Science Laboratory, SRI
International, Menlo Park, CA, September 1999.
[44] N. Shankar, S. Owre, J. M. Rushby, and D. W. J. Stringer-Calvert.
PVS Prover Guide. Computer Science Laboratory, SRI International,
Menlo Park, CA, September 1999.
[45] S. Owre, N. Shankar, J. M. Rushby, and D. W. J. Stringer-Calvert.
PVS System Guide. Computer Science Laboratory, SRI
International, Menlo Park, CA, September 1999.
[46] Sam Owre and Natarajan Shankar. The formal semantics of PVS.
Technical Report SRI-CSL-97-2, Computer Science Laboratory, SRI
International, Menlo Park, CA, August 1997.
[47] Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von
Henke. Formal verification for fault-tolerant architectures:
Prolegomena to the design of PVS. IEEE Transactions on Software
Engineering, 21(2):107-125, February 1995.
[48] John Rushby, Sam Owre, and N. Shankar. Subtypes for
specifications: Predicate subtyping in PVS. IEEE Transactions on
Software Engineering, 24(9):709-720, September 1998.
9
[49] Natarajan Shankar and Sam Owre. Principles and pragmatics of
subtyping in PVS. In Didier Bert, Christine Choppy, and Peter
Mosses, editors, Recent Trends in Algebraic Development Techniques,
WADT '99, volume 1827 of Lecture Notes in Computer Science,
pages 37-52, Toulouse, France, September 1999. Springer-Verlag.
[50] Ricky W. Butler. An elementary tutorial on formal specification and
verification using PVS 2. NASA Technical Memorandum 108991,
NASA Langley Research Center, Hampton, VA, June 1993. Revised
June 1995. Available, with PVS specification files, at
http://atb-www.larc.nasa.gov/ftp/larc/PVS-tutorial; use only
files marked "revised.".
[51] Judy Crow, Sam Owre, John Rushby, Natarajan Shankar, and
Mandayam Srivas. A tutorial introduction to PVS. Presented at
WIFT '95: Workshop on Industrial-Strength Formal Specification
Techniques, Boca Raton, Florida, April 1995. Available, with
specification files, at
http://www.csl.sri.com/wift-tutorial.html.
[52] John Rushby and David W. J. Stringer-Calvert. A less elementary
tutorial for the PVS specification and verification system. Technical
Report SRI-CSL-95-10, Computer Science Laboratory, SRI
International, Menlo Park, CA, June 1995. Revised, July 1996.
Available, with specification files, at
http://www.csl.sri.com/csl-95-10.html.
[53] S. Owre, J. M. Rushby, N. Shankar, and M. K. Srivas. A tutorial on
using PVS for hardware verification. In Ramayya Kumar and
Thomas Kropf, editors, Theorem Provers in Circuit Design (TPCD
'94), volume 910 of Lecture Notes in Computer Science, pages
258-279, Bad Herrenalb, Germany, September 1994. Springer-Verlag.
[54] Sam Owre and Natarajan Shankar. Abstract datatypes in PVS.
Technical Report SRI-CSL-93-9R, Computer Science Laboratory, SRI
International, Menlo Park, CA, December 1993. Extensively revised
June 1997; Also available as NASA Contractor Report CR-97-206264.
[55] Sam Owre, John Rushby, and Natarajan Shankar. Analyzing tabular
and state-transition specifications in PVS. Technical Report
SRI-CSL-95-12, Computer Science Laboratory, SRI International,
Menlo Park, CA, July 1995. Available, with specification files, at
http://www.csl.sri.com/csl-95-12.html. Also published as
NASA Contractor Report 201729.
[56] John Rushby. Specification, proof checking, and model checking for
protocols and distributed systems with PVS. Tutorial presented at
10
FORTE X/PSTV XVII '97: Formal Description Techniques and
Protocol Specification, Testing and Verification, November 1997.
Available, with specification files, at
http://www.csl.sri.com/forte97.html.
[57] John Rushby. Theorem proving for verification. In Franck Cassez,
editor, Modelling and Verification of Parallel Processes: MoVEP 2k,
Nantes, France, June 2000. Tutorial presented at MoVEP: revised
version to be published by Springer LNCS.
[58] Judith Crow et al. NASA Formal Methods Specification and
Verification Guidebook for Software and Computer Systems, Volume
I: Planning and Technology Insertion. NASA Office of Safety and
Mission Assurance, Washington, DC, 1995. Available at
http://eis.jpl.nasa.gov/quality/Formal`Methods/.
[59] Judith Crow et al. NASA Formal Methods Specification and
Verification Guidebook for Software and Computer Systems, Volume
II: A Practitioner's Companion. NASA Office of Safety and Mission
Assurance, Washington, DC, 1997. Available at
http://eis.jpl.nasa.gov/quality/Formal`Methods/.
[60] David A. Cyrluk and Mandayam K. Srivas. Theorem proving: Not
an esoteric diversion, but the unifying framework for industrial
verification. In International Conference on Computer Design: VLSI
in Computers and Processors (ICCD '95), pages 538-544, Austin,
TX, October 1995. IEEE Computer Society.
[61] David L. Dill and John Rushby. Acceptance of formal methods:
Lessons from hardware design. IEEE Computer, 29(4):23-24, April
1996. Part of [326].
[62] John Rushby. Formal methods for dependable real-time systems. In
International Symposium on Real-Time Embedded Processing for
Space Applications, pages 355-366, Les Saintes-Maries-de-la-Mer,
France, November 1992. CNES, the French Space Agency. Published
by C'epadu`es-'Editions, Toulouse, France.
[63] John Rushby. Mechanizing formal methods: Opportunities and
challenges. In Jonathan P. Bowen and Michael G. Hinchey, editors,
ZUM '95: The Z Formal Specification Notation; 9th International
Conference of Z Users, volume 967 of Lecture Notes in Computer
Science, pages 105-113, Limerick, Ireland, September 1995.
Springer-Verlag.
[64] John Rushby. Automated deduction and formal methods. In Rajeev
Alur and Thomas A. Henzinger, editors, Computer-Aided
11
Verification, CAV '96, volume 1102 of Lecture Notes in Computer
Science, pages 169-183, New Brunswick, NJ, July/August 1996.
Springer-Verlag.
[65] John Rushby. Mechanized formal methods: Progress and prospects.
In V. Chandru and V. Vinay, editors, 16th Conference on the
Foundations of Software Technology and Theoretical Computer
Science, volume 1180 of Lecture Notes in Computer Science, pages
43-51, Hyderabad, India, December 1996. Springer-Verlag.
[66] John Rushby. Calculating with requirements. In 3rd IEEE
International Symposium on Requirements Engineering, pages
144-146, Annapolis, MD, January 1997. IEEE Computer Society.
[67] John Rushby. Mechanized formal methods: Where next? In
Jeannette Wing and Jim Woodcock, editors, FM99: The World
Congress in Formal Methods, volume 1708 and 1709 of Lecture Notes
in Computer Science, pages 48-51, Toulouse, France, September
1999. Springer-Verlag. Pages 1-938 are in the first volume, 939-1872
in the second.
[68] N. Shankar. Towards mechanical metamathematics. Journal of
Automated Reasoning, 1(4):407-434, 1985.
[69] N. Shankar. Observations on the use of computers in proof checking.
Notices of the American Mathematical Society, 35(6):804-805,
July/August 1988.
[70] N. Shankar. Metamathematics, Machines, and G"odel's Proof.
Cambridge Tracts in Theoretical Computer Science. Cambridge
University Press, Cambridge, UK, 1994.
[71] Natarajan Shankar. Unifying verification paradigms. In Bengt
Jonsson and Joachim Parrow, editors, Formal Techniques in
Real-Time and Fault-Tolerant Systems, volume 1135 of Lecture Notes
in Computer Science, pages 22-39, Uppsala, Sweden, September
1996. Springer-Verlag.
[72] John Rushby. Formal methods and the certification of critical
systems. Technical Report SRI-CSL-93-7, Computer Science
Laboratory, SRI International, Menlo Park, CA, December 1993.
Also issued under the title 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.
[73] John Rushby. Critical system properties: Survey and taxonomy.
Reliability Engineering and System Safety, 43(2):189-219, 1994.
12
[74] John Rushby. Formal methods and their role in the certification of
critical systems. Technical Report SRI-CSL-95-1, Computer Science
Laboratory, SRI International, Menlo Park, CA, March 1995. Also
available as NASA Contractor Report 4673, August 1995, and issued
as part of the FAA Digital Systems Validation Handbook (the guide
for aircraft certification). Reprinted in [327, pp. 1-42].
[75] Mandayam Srivas, Harald Ruess, and David Cyrluk. Hardware
verification using PVS. In Thomas Kropf, editor, Formal Hardware
Verification: Methods and Systems in Comparison, volume 1287 of
Lecture Notes in Computer Science, pages 156-205. Springer-Verlag,
1997.
[76] David Cyrluk, Patrick Lincoln, and N. Shankar. On Shostak's
decision procedure for combinations of theories. In M. A. McRobbie
and J. K. Slaney, editors, Automated Deduction_CADE-13, volume
1104 of Lecture Notes in Artificial Intelligence, pages 463-477, New
Brunswick, NJ, July/August 1996. Springer-Verlag.
[77] David Cyrluk, Harald Ruess, and Oliver M"oller. An efficient decision
procedure for the theory of fixed-sized bit-vectors. In Orna
Grumberg, editor, Computer-Aided Verification, CAV '97, volume
1254 of Lecture Notes in Computer Science, pages 60-71, Haifa,
Israel, June 1997. Springer-Verlag.
[78] D. Cyrluk and P. Narendran. Ground temporal logic_a logic for
hardware verification. In David Dill, editor, Computer-Aided
Verification, CAV '94, volume 818 of Lecture Notes in Computer
Science, pages 247-259, Stanford, CA, June 1994. Springer-Verlag.
[79] D. Cyrluk, S. Rajan, N. Shankar, and M. K. Srivas. Effective
theorem proving for hardware verification. In Ramayya Kumar and
Thomas Kropf, editors, Theorem Provers in Circuit Design (TPCD
'94), volume 910 of Lecture Notes in Computer Science, pages
203-222, Bad Herrenalb, Germany, September 1994. Springer-Verlag.
[80] Oliver M"oller and Harald Ruess. Solving bit-vector equations. In
Ganesh Gopalakrishnan and Phillip Windley, editors, Formal
Methods in Computer-Aided Design (FMCAD '98), volume 1522 of
Lecture Notes in Computer Science, pages 36-48, Palo Alto, CA,
November 1998. Springer-Verlag.
[81] Ashish Tiwari, Leo Bachmair, and Harald Ruess. Rigid e-unification
revisited. In David McAllester, editor, Automated
Deduction_CADE-17, volume 1831 of Lecture Notes in Artificial
Intelligence, pages 220-234, Pittsburgh, PA, June 2000.
Springer-Verlag.
13
[82] S. Rajan, N. Shankar, and M.K. Srivas. An integration of
model-checking with automated proof checking. In Pierre Wolper,
editor, Computer-Aided Verification, CAV '95, volume 939 of Lecture
Notes in Computer Science, pages 84-97, Liege, Belgium, June 1995.
Springer-Verlag.
[83] Sam Owre, John Rushby, and N. Shankar. Integration in PVS:
Tables, types, and model checking. In Ed Brinksma, editor, Tools and
Algorithms for the Construction and Analysis of Systems (TACAS
'97), volume 1217 of Lecture Notes in Computer Science, pages
366-383, Enschede, The Netherlands, April 1997. Springer-Verlag.
[84] Sam Owre and Harald Ruess. Integrating WS1S with PVS. In E. A.
Emerson and A. P. Sistla, editors, Computer-Aided Verification, CAV
'2000, volume 1855 of Lecture Notes in Computer Science, pages
548-551, Chicago, IL, July 2000. Springer-Verlag.
[85] Friedrich von Henke, Stephan Pfab, Harald Ruess, and Sam Owre.
Towards light-weight verification and heavy-weight testing. In
Rudolph Berghammer and Yassine Lakhnech, editors, Tool Support
for System Specification, Development, and Verification, Advances in
Computing Science, pages 189-200, Malente, Germany, June 1998.
Springer-Verlag. Proceedings published in May 1999.
[86] Friedrich von Henke, Stephan Pfab, Holger Pfeifer, and Harald Ruess.
Case studies in meta-level theorem proving. In Jim Grundy and
Malcolm Newey, editors, Theorem Proving in Higher Order Logics:
11th International Conference, TPHOLs '98, volume 1479 of Lecture
Notes in Computer Science, pages 461-478, Canberra, Australia,
September 1998. Springer-Verlag.
[87] N. Shankar. Efficiently executing PVS. Project report, Computer
Science Laboratory, SRI International, Menlo Park, CA, November
1999. Available at
http://www.csl.sri.com/shankar/PVSeval.ps.gz.
[88] Saddek Bensalem, Yassine Lakhnech, and Hassen Sa"idi. Powerful
techniques for the automatic generation of invariants. In Rajeev Alur
and Thomas A. Henzinger, editors, Computer-Aided Verification,
CAV '96, volume 1102 of Lecture Notes in Computer Science, pages
323-335, New Brunswick, NJ, July/August 1996. Springer-Verlag.
[89] Saddek Bensalem, Yassine Lakhnech, and Sam Owre. Computing
abstractions of infinite state systems compositionally and
automatically. In Alan J. Hu and Moshe Y. Vardi, editors,
Computer-Aided Verification, CAV '98, volume 1427 of Lecture Notes
14
in Computer Science, pages 319-331, Vancouver, Canada, June 1998.
Springer-Verlag.
[90] Parosh Aziz Abdulla, Aurore Annichini, Saddek Bensalem, Ahmed
Bouajjani, Peter Habermehl, and Yassine Lakhnech. Verification of
infinite-state systems by combining abstraction and reachability
analysis. In Nicolas Halbwachs and Doron Peled, editors,
Computer-Aided Verification, CAV '99, volume 1633 of Lecture Notes
in Computer Science, pages 146-159, Trento, Italy, July 1999.
Springer-Verlag.
[91] Vlad Rusu and Eli Singerman. On proving safety properties by
integrating static analysis, theorem proving and abstraction. In
W. Rance Cleaveland, editor, Tools and Algorithms for the
Construction and Analysis of Systems (TACAS '99), volume 1579 of
Lecture Notes in Computer Science, pages 178-192, Amsterdam, The
Netherlands, March 1999. Springer-Verlag.
[92] Susanne Graf and Hassen Sa"idi. Verifying invariants using theorem
proving. In Rajeev Alur and Thomas A. Henzinger, editors,
Computer-Aided Verification, CAV '96, volume 1102 of Lecture Notes
in Computer Science, pages 196-207, New Brunswick, NJ,
July/August 1996. Springer-Verlag.
[93] Hassen Sa"idi. A tool for proving invariance properties of concurrent
systems automatically. In Tools and Algorithms for the Construction
and Analysis of Systems TACAS '96, volume 1055 of Lecture Notes
in Computer Science, pages 412-416, Passau, Germany, March 1996.
Springer-Verlag.
[94] Hassen Sa"idi. The Invariant Checker: Automated deductive
verification of reactive systems. In Orna Grumberg, editor,
Computer-Aided Verification, CAV '97, volume 1254 of Lecture Notes
in Computer Science, pages 436-439, Haifa, Israel, June 1997.
Springer-Verlag.
[95] Hassen Sa"idi and Susanne Graf. Construction of abstract state
graphs with PVS. In Orna Grumberg, editor, Computer-Aided
Verification, CAV '97, volume 1254 of Lecture Notes in Computer
Science, pages 72-83, Haifa, Israel, June 1997. Springer-Verlag.
[96] Hassen Sa"idi. Automated deductive verification of parallel systems.
In C. Michael Holloway and Kelly J. Hayhurst, editors, LFM' 97:
Fourth NASA Langley Formal Methods Workshop, NASA Conference
Publication 3356, pages 163-176, Hampton, VA, September 1997.
NASA Langley Research Center. Available at
http://atb-www.larc.nasa.gov/Lfm97/proceedings/.
15
[97] Hassen Sa"idi and N. Shankar. Abstract and model check while you
prove. In Nicolas Halbwachs and Doron Peled, editors,
Computer-Aided Verification, CAV '99, volume 1633 of Lecture Notes
in Computer Science, pages 443-454, Trento, Italy, July 1999.
Springer-Verlag.
[98] Hassen Sa"idi. Model checking guided abstraction and analysis. In
Jens Palsberg, editor, Seventh International Static Analysis
Symposium (SAS'00), volume 1824 of Lecture Notes in Computer
Science, pages 377-396, Santa Barbara CA, June 2000.
Springer-Verlag.
[99] Natarajan Shankar. Symbolic analysis of transition systems. In Yuri
Gurevich, Phillip W. Kutter, Martin Odersky, and Lothar Thiele,
editors, Abstract State Machines: Theory and Applications (ASM
2000), number 1912 in Lecture Notes in Computer Science, pages
287-302, Monte Verit`a, Switzerland, March 2000. Springer-Verlag.
[100] Natarajan Shankar. Combining theorem proving and model checking
through symbolic analysis. In CONCUR 2000: Concurrency Theory,
number 1877 in Lecture Notes in Computer Science, pages 1-16,
State College, PA, August 2000. Springer-Verlag.
[101] Saddek Bensalem, Yassine Lakhnech, and Sam Owre. InVeSt: A tool
for the verification of invariants. In Alan J. Hu and Moshe Y. Vardi,
editors, Computer-Aided Verification, CAV '98, volume 1427 of
Lecture Notes in Computer Science, pages 505-510, Vancouver,
Canada, June 1998. Springer-Verlag.
[102] Saddek Bensalem, Vijay Ganesh, Yassine Lakhnech, C'esar Mu"noz,
Sam Owre, Harald Ruess, John Rushby, Vlad Rusu, Hassen Sa"idi,
N. Shankar, Eli Singerman, and Ashish Tiwari. An overview of SAL.
In C. Michael Holloway, editor, LFM 2000: Fifth NASA Langley
Formal Methods Workshop, pages 187-196, Hampton, VA, June 2000.
NASA Langley Research Center. Proceedings available at
http://shemesh.larc.nasa.gov/fm/Lfm2000/Proc/.
[103] John Rushby. Ubiquitous abstraction: A new approach for
mechanized formal verification (extended abstract). In John Staples,
Michael G. Hinchey, and Shaoying Liu, editors, Second International
Conference on Formal Engineering Methods (ICFEM '98), pages
176-178, Brisbane, Australia, December 1998. IEEE Computer
Society.
[104] John Rushby. Integrated formal verification: Using model checking
with automated abstraction, invariant generation, and theorem
16
proving. In D. Dams, R. Gerth, S. Leue, and M. Massink, editors,
Theoretical and Practical Aspects of SPIN Model Checking: 5th and
6th International SPIN Workshops, volume 1680 of Lecture Notes in
Computer Science, pages 1-11, Trento, Italy, and Toulouse, France,
July and September 1999. Springer-Verlag.
[105] John Rushby. From refutation to verification. In Tommaso Bolognesi
and Diego Latella, editors, Formal Description Techniques and
Protocol Specification, Testing and Verification FORTE XIII/PSTV
XX 2000, pages 369-374, Pisa, Italy, October 2000. Kluwer Academic
Publishers.
[106] John Rushby. Disappearing formal methods. In High-Assurance
Systems Engineering Symposium, pages 95-96, Albuquerque, NM,
November 2000. Association for Computing Machinery.
[107] William D. Young. Comparing verification systems: Interactive
Consistency in ACL2. IEEE Transactions on Software Engineering,
23(4):214-223, April 1997.
[108] Victor A. Carre"no and Paul S. Miner. Specification of the IEEE-854
floating-point standard in HOL and PVS. In HOL95: Eighth
International Workshop on Higher-Order Logic Theorem Proving and
Its Applications, Aspen Grove, UT, September 1995. Category B
proceedings, available at
http://lal.cs.byu.edu/lal/hol95/Bprocs/indexB.html.
[109] Mike Gordon. Notes on PVS from a HOL perspective. Available at
http://www.cl.cam.ac.uk/users/mjcg/PVS.html, August 1995.
[110] David Griffioen and Marieke Huisman. A comparison of PVS and
Isabelle/HOL. In Jim Grundy and Malcolm Newey, editors, Theorem
Proving in Higher Order Logics: 11th International Conference,
TPHOLs '98, volume 1479 of Lecture Notes in Computer Science,
pages 123-142, Canberra, Australia, September 1998.
Springer-Verlag.
[111] Jan Friso Groote, cois Monin Fran and Jaco van de Pol. Checking
verifications of protocols and distributed systems by computer. In
Davide Sangiorgi and Robert de Simone, editors, CONCUR'98:
Concurrency Theory, volume 1466 of Lecture Notes in Computer
Science, pages 629-655, Nice, France, September 1998.
Springer-Verlag.
[112] Christoph Kern and Mark R. Greenstreet. Formal verification in
hardware design: A survey. ACM Transactions on Design
17
Automation of Electronic Systems (TODAES), 4(2):123-193, April
1999.
[113] Heinrich Rust. A PVS specification of an invoicing system. In
M. Allemand, C. Attiogb'e, and H. Habrias, editors, Proceedings of an
International Workshop on Specification Techniques and Formal
Methods, pages 51-65. University of Nantes, France, March 1998.
Available at
http://www.informatik.tu-cottbus.de/"rust/publications/a`
pvs`specificat%ion`of`an`invoicing`system.ps.gz.
[114] Matthew Wilding. Robust computer system proofs in PVS. In
C. Michael Holloway and Kelly J. Hayhurst, editors, LFM' 97:
Fourth NASA Langley Formal Methods Workshop, NASA Conference
Publication 3356, pages 177-184, Hampton, VA, September 1997.
NASA Langley Research Center. Available at
http://atb-www.larc.nasa.gov/Lfm97/proceedings/.
[115] Georg Droschl. On the integration of formal methods: Events and
scenarios in PVS and VDM. In Proceedings, 3rd. Irish Workshop in
Formal Methods, Galway, Ireland, July 1999. Electronic Workshops
in Computing (http://ewic.org.uk/ewic/).
[116] Georg Droschl. Analyzing the requirements of an access control using
VDMTools and PVS. In Jeannette Wing and Jim Woodcock, editors,
FM99: The World Congress in Formal Methods, volume 1708 and
1709 of Lecture Notes in Computer Science, page 1807, Toulouse,
France, September 1999. Springer-Verlag. Pages 1-938 are in the first
volume, 939-1872 in the second.
[117] Nicholas A. Merriam and Michael D. Harrison. Evaluating the
interfaces of three theorem proving assistants. In F. Bodart and
J. Vanderdonckt, editors, Proceedings of the 3rd International
Eurographics Workshop on Design, Specification, and Verification of
Interactive Systems, 1996.
[118] Myla Archer and Constance Heitmeyer. Human-style theorem
proving using PVS. In Elsa Gunter and Amy Felty, editors, Theorem
Proving in Higher Order Logics: 10th International Conference,
TPHOLs '97, volume 1275 of Lecture Notes in Computer Science,
pages 33-48, Murray Hill, NJ, August 1997. Springer-Verlag.
[119] Myla Archer, Constance Heitmeyer, and Steve Sims. TAME: A PVS
interface to simplify proofs for automata models. In User Interfaces
for Theorem Provers, Eindhoven, The Netherlands, July 1998.
Informal proceedings available at
http://www.win.tue.nl/cs/ipa/uitp/proceedings.html.
18
[120] John Knight, Colleen DeJong, Matthew Gibble, and Lu'is Nakano.
Why are formal methods not used more widely? In C. Michael
Holloway and Kelly J. Hayhurst, editors, LFM' 97: Fourth NASA
Langley Formal Methods Workshop, NASA Conference Publication
3356, pages 1-12, Hampton, VA, September 1997. NASA Langley
Research Center. Available at
http://atb-www.larc.nasa.gov/Lfm97/proceedings/.
[121] Bruno Dutertre. Elements of mathematical analysis in PVS. In
Joakim von Wright, Jim Grundy, and John Harrison, editors,
Theorem Proving in Higher Order Logics: 9th International
Conference, TPHOLs '96, volume 1125 of Lecture Notes in Computer
Science, pages 141-156, Turku, Finland, August 1996.
Springer-Verlag.
[122] Hanne Gottliebsen. Transcendental functions and continuity checking
in PVS. In Mark Aargaard and John Harrison, editors, Theorem
Proving in Higher Order Logics: 13th International Conference,
TPHOLs 2000, volume 1869 of Lecture Notes in Computer Science,
pages 197-214, Portland, OR, August 2000. Springer-Verlag.
[123] Twan Basten and Jozef Hooman. Process algebra in PVS. In
W. Rance Cleaveland, editor, Tools and Algorithms for the
Construction and Analysis of Systems (TACAS '99), volume 1579 of
Lecture Notes in Computer Science, pages 270-284, Amsterdam, The
Netherlands, March 1999. Springer-Verlag.
[124] Dmitri Schamschurko. Modeling process calculi with PVS. In
B. Jacobs, L. Moss, H. Reichel, and J. Rutten, editors, First
Workshop on Coalgebraic Methods in Computer Science (CMCS'98),
volume 11 of Electronic Notes in Theoretical Computer Science,
pages 197-214, Lisbon, Portugal, March 1998. Elsevier. Available at
http://www.elsevier.nl/cas/tree/store/tcs/free/entcs/
store/tcs11/tcs110%11.ps.
[125] David Griffioen and Frits Vaandrager. Normed simulations. In
Alan J. Hu and Moshe Y. Vardi, editors, Computer-Aided
Verification, CAV '98, volume 1427 of Lecture Notes in Computer
Science, pages 332-344, Vancouver, Canada, June 1998.
Springer-Verlag.
[126] Amir Pnueli, N. Shankar, and Eli Singerman. Fair synchronous
transition systems and their liveness proofs. In Formal Techniques in
Real-Time and Fault-Tolerant Systems, volume 1486 of Lecture Notes
in Computer Science, pages 198-209, Lyngby, Denmark, September
1998. Springer-Verlag.
19
[127] M. Devillers, D. Griffioen, and O. Mueller. Possibly infinite sequences
in theorem provers: A comparative study. In Elsa Gunter and Amy
Felty, editors, Theorem Proving in Higher Order Logics: 10th
International Conference, TPHOLs '97, volume 1275 of Lecture
Notes in Computer Science, pages 89-104, Murray Hill, NJ, August
1997. Springer-Verlag.
[128] Ulrich Hensel and Bart Jacobs. Proof principles for datatypes with
iterated recursion. In Eugenio Moggi and Giuseppe Rosolini, editors,
Category Theory and Computer Science, volume 1290 of Lecture
Notes in Computer Science, pages 220-241, Santa Margherita Ligure,
Italy, September 1997. Springer-Verlag.
[129] Ulrich Hensel and Bart Jacobs. Coalgebraic theories of sequences in
PVS. Journal of Logic and Computation, 9(4):463-500, 1999.
[130] Ulrich Hensel, Marieke Huisman, Bart Jacobs, and Hendrik Tews.
Reasoning about classes in object-oriented languages: Logical models
and tools. In Chris Hankin, editor, Programming Languages and
Systems: 7th European Symposium On Programming (ESOP),
volume 1381 of Lecture Notes in Computer Science, pages 105-121,
Lisbon, Portugal, March 1998. Springer-Verlag.
[131] Marieke Huisman, Bart Jacobs, and Joachim van den Berg. A case
study in class library verification: Java's vector class. In A. Moreira
and D. Demeyer, editors, Object-Oriented Technology: ECOOP'99
Workshop Reader, volume 1743 of Lecture Notes in Computer
Science, pages 109_110, Lisbon, Portugal, June 1999.
Springer-Verlag.
[132] Bart Jacobs, Joachim van den Berg, Marieke Huisman, Martijn van
Berkum, Ulrich Hensel, and Hendrick Tews. Reasoning about Java
classes. In Proceedings, Object-Oriented Programming Systems,
Languages and Applications (OOPSLA'98), pages 329-340,
Vancouver, Canada, October 1998. Association for Computing
Machinery. Proceedings issued as ACM SIGPLAN Notices Vol. 33,
No. 10, October 1998.
[133] Marieke Huisman and Bart Jacobs. Inheritance in higher order logic:
Modeling and reasoning. In Mark Aargaard and John Harrison,
editors, Theorem Proving in Higher Order Logics: 13th International
Conference, TPHOLs 2000, volume 1869 of Lecture Notes in
Computer Science, pages 301-319, Portland, OR, August 2000.
Springer-Verlag.
20
[134] Marieke Huisman. Java Program Verification in Higher-Order Logic
with PVS and Isabelle. PhD thesis, University of Nijmegen, The
Netherlands, 2001.
[135] Marieke Huisman and Bart Jacobs. Java program verfication via a
hoare logic with abrupt termination. In Tom Maibaum, editor,
Fundamental Approaches to Software Engineering, FASE 2000,
number 1783 in Lecture Notes in Computer Science, pages 284-303,
Berlin, Germany, March/April 2000. Springer-Verlag.
[136] Joachim van den Berg, Marieke Huisman, Bart Jacobs, and Erik Poll.
A type-theoretic memory model for verification of sequential Java
programs. In Didier Bert, Christine Choppy, and Peter Mosses,
editors, Recent Trends in Algebraic Development Techniques, WADT
'99, number 1827 in Lecture Notes in Computer Science, pages 1-21,
Toulouse, France, September 1999. Springer-Verlag.
[137] Patrick Lincoln and John Rushby. Formal verification of an
algorithm for interactive consistency under a hybrid fault model. In
Costas Courcoubetis, editor, Computer-Aided Verification, CAV '93,
volume 697 of Lecture Notes in Computer Science, pages 292-304,
Elounda, Greece, June/July 1993. Springer-Verlag.
[138] Patrick Lincoln and John Rushby. A formally verified algorithm for
interactive consistency under a hybrid fault model. In Fault Tolerant
Computing Symposium 23, pages 402-411, Toulouse, France, June
1993. IEEE Computer Society. Reprinted in [325, pp. 438-447].
[139] Patrick Lincoln and John Rushby. Formal verification of an
interactive consistency algorithm for the Draper FTP architecture
under a hybrid fault model. In COMPASS '94 (Proceedings of the
Ninth Annual Conference on Computer Assurance), pages 107-120,
Gaithersburg, MD, June 1994. IEEE Washington Section.
[140] Holger Pfeifer, Detlef Schwier, and Friedrich W. von Henke. Formal
verification for time-triggered clock synchronization. In Charles B.
Weinstock and John Rushby, editors, Dependable Computing for
Critical Applications_7, volume 12 of Dependable Computing and
Fault Tolerant Systems, pages 207-226, San Jose, CA, January 1999.
IEEE Computer Society.
[141] Holger Pfeifer. Formal verification of the TTA group membership
algorithm. In Tommaso Bolognesi and Diego Latella, editors, Formal
Description Techniques and Protocol Specification, Testing and
Verification FORTE XIII/PSTV XX 2000, pages 3-18, Pisa, Italy,
October 2000. Kluwer Academic Publishers.
21
[142] John Rushby. Systematic formal verification for fault-tolerant
time-triggered algorithms. IEEE Transactions on Software
Engineering, 25(5):651-660, September/October 1999.
[143] John Rushby. Verification diagrams revisited: Disjunctive invariants
for easy verification. In E. A. Emerson and A. P. Sistla, editors,
Computer-Aided Verification, CAV '2000, volume 1855 of Lecture
Notes in Computer Science, pages 508-520, Chicago, IL, July 2000.
Springer-Verlag.
[144] D. Schwier and F. von Henke. Mechanical verification of clock
synchronization algorithms. In Formal Techniques in Real-Time and
Fault-Tolerant Systems, volume 1486 of Lecture Notes in Computer
Science, pages 262-271, Lyngby, Denmark, September 1998.
Springer-Verlag.
[145] Chris J. Walter, Patrick Lincoln, and Neeraj Suri. Formally verified
on-line diagnosis. IEEE Transactions on Software Engineering,
23(11):684-721, November 1997.
[146] Ben L. Di Vito. A formal model of partitioning for integrated
modular avionics. NASA Contractor Report CR-1998-208703, NASA
Langley Research Center, August 1998.
[147] Ben L. Di Vito. A model of cooperative noninterference for
integrated modular avionics. In Charles B. Weinstock and John
Rushby, editors, Dependable Computing for Critical Applications_7,
volume 12 of Dependable Computing and Fault Tolerant Systems,
pages 269-286, San Jose, CA, January 1999. IEEE Computer Society.
[148] Matthew M. Wilding, David S. Hardin, and David A. Greve.
Invariant performance: A statement of task isolation useful for
embedded application integration. In Charles B. Weinstock and John
Rushby, editors, Dependable Computing for Critical Applications_7,
volume 12 of Dependable Computing and Fault Tolerant Systems,
pages 287-300, San Jose, CA, January 1999. IEEE Computer Society.
[149] Ricky W. Butler. An introduction to requirements capture using
PVS: Specification of a simple autopilot. NASA Technical
Memorandum 110255, NASA Langley Research Center, Hampton,
VA, May 1996.
[150] Bruno Dutertre and Victoria Stavridou. Formal requirements
analysis of an avionics control system. IEEE Transactions on
Software Engineering, 23(5):267-278, May 1997.
22
[151] Bruno Dutertre and Victoria Stavridou. Requirements analysis of
real-time control systems using PVS. In C. Michael Holloway and
Kelly J. Hayhurst, editors, LFM' 97: Fourth NASA Langley Formal
Methods Workshop, NASA Conference Publication 3356, pages
65-74, Hampton, VA, September 1997. NASA Langley Research
Center. Available at
http://atb-www.larc.nasa.gov/Lfm97/proceedings/.
[152] Judith Crow and Ben L. Di Vito. Formalizing Space Shuttle software
requirements: Four case studies. ACM Transactions on Software
Engineering and Methodology, 7(3):296-332, July 1998.
[153] Steve Easterbrook, Robyn Lutz, Richard Covington, John Kelly,
Yoko Ampo, and David Hamilton. Experiences using lightweight
formal methods for requirements modeling. IEEE Transactions on
Software Engineering, 24(1):4-14, January 1998.
[154] Larry W. Roberts and Mike Beims. Using formal methods to assist
in the requirements analysis of the Space Shuttle HAC Change
Request (CR 90960E). Technical Report JSC-27599, NASA Johnson
Space Center, Houston, TX, September 1996.
[155] Ben L. Di Vito. Formalizing new navigation requirements for
NASA's Space Shuttle. In Formal Methods Europe FME '96, volume
1051 of Lecture Notes in Computer Science, pages 160-178, Oxford,
UK, March 1996. Springer-Verlag.
[156] Ben L. Di Vito. High-automation proofs for properties of
requirements models. Software Tools for Technology Transfer, 3(1),
2000. To appear; available at
http://shemesh.larc.nasa.gov/people/bld/ftp/sttt-bld.ps.
[157] Ben L. Di Vito and Larry W. Roberts. Using formal methods to
assist in the requirements analysis of the Space Shuttle GPS Change
Request. NASA Contractor Report 4752, NASA Langley Research
Center, August 1996.
[158] David Hamilton, Rick Covington, and John Kelly. Experiences in
applying formal methods to the analysis of software and system
requirements. In WIFT '95: Workshop on Industrial-Strength Formal
Specification Techniques, pages 30-43, Boca Raton, FL, 1995. IEEE
Computer Society.
[159] David Hamilton, Rick Covington, and Alice Lee. An experience
report on requirements reliability engineering using formal methods.
In Sixth International Conference on Software Reliability
23
Engineering, ISSRE '95, pages 52-57, Toulouse, France, 1995. IEEE
Computer Society.
[160] Yoko Ampo and Robyn Lutz. Evaluation of software safety analysis
using formal methods. In Workshop for Foundation of Software
Engineering (FOSE), Hamana-Ko, Japan, December 1995. In
Japanese.
[161] Robyn Lutz and Yoko Ampo. Experience report: Using formal
methods for requirements analysis of critical spacecraft software. In
Proceedings of the 19th Annual Software Engineering Workshop,
pages 231-248, Greenbelt, MD, December 1994. NASA Goddard
Space Flight Center.
[162] Robyn Lutz. Reuse of a formal model for requirements validation. In
C. Michael Holloway and Kelly J. Hayhurst, editors, LFM' 97:
Fourth NASA Langley Formal Methods Workshop, NASA Conference
Publication 3356, pages 75-86, Hampton, VA, September 1997.
NASA Langley Research Center. Available at
http://atb-www.larc.nasa.gov/Lfm97/proceedings/.
[163] Victor Carre"no and C'esar Mu"noz. Aircraft trajectory modeling and
alerting algorithm verification. In Mark Aargaard and John Harrison,
editors, Theorem Proving in Higher Order Logics: 13th International
Conference, TPHOLs 2000, volume 1869 of Lecture Notes in
Computer Science, pages 90-105, Portland, OR, August 2000.
Springer-Verlag.
[164] Victor Carre"no and C'esar Mu"noz. Formal analysis of parallel landing
scenarios. In 19th AIAA/IEEE Digital Avionics Systems Conference,
Philadelphia, PA, October 2000.
[165] Mark Lawford, Jeff McDougall, Peter Froebel, and Greg Moum.
Practical application of functional and relational methods for the
specification and verification of safety critical software. In Teodor
Rus, editor, Algebraic Methodology and Software Technology,
AMAST 2000, volume 1816 of Lecture Notes in Computer Science,
pages 73-88, Iowa City, IA, May 2000. Springer-Verlag.
[166] S. Koo, H. Son, and P. Seong. Mathematical verification of a nuclear
power plant protection system function with combined CPN and
PVS. Journal of the Korean Nuclear Society, 31:157-171, April 1999.
[167] Jaco van de Pol, Jozef Hooman, and Edwin de Jong. Formal
requirements specification for command and control systems. In
Engineering of Computer Based Systems (ECBS), pages 37-44,
24
Jerusalem, Israel, March-April 1998. IEEE Computer Society.
Available at http://www.win.tue.nl/cs/tt/hooman/ECBS98.html.
[168] Drew Dean. Static typing with dynamic linking. In Fourth ACM
Conference on Computer and Communications Security, pages 18-27,
Zurich, Switzerland, April 1997. Association for Computing
Machinery.
[169] John Hoffman and Charlie Payne. A formal experience at Secure
Computing Corporation. In Alan J. Hu and Moshe Y. Vardi, editors,
Computer-Aided Verification, CAV '98, volume 1427 of Lecture Notes
in Computer Science, pages 49-56, Vancouver, Canada, June 1998.
Springer-Verlag.
[170] Ramesh V. Peri, William A. Wulf, and Darrell M. Kienzle. A logic of
composition for information flow predicates. In 9th Computer
Security Foundations Workshop, pages 82-94, Kenmare, Ireland,
June 1996. IEEE Computer Society.
[171] Darryl Dieckman, Perry Alexander, and Philip A. Wilsey.
ActiveSPEC: A framework for the specification and verification of
active network services and security policies. In Nevin Heintze and
Jeannette Wing, editors, Workshop on Formal Methods and Security
Protocols, Indianapolis, IN, June 1998. Informal proceedings available
at http://www.cs.bell-labs.com/who/nch/fmsp/program.html.
[172] Bruno Dutertre and Steve Schneider. Embedding CSP in PVS. an
application to authentication protocols. In Elsa Gunter and Amy
Felty, editors, Theorem Proving in Higher Order Logics: 10th
International Conference, TPHOLs '97, volume 1275 of Lecture
Notes in Computer Science, pages 121-136, Murray Hill, NJ, August
1997. Springer-Verlag.
[173] Jonathan K. Millen. A necessarily parallel attack. In Nevin Heintze
and Edmund Clarke, editors, Workshop on Formal Methods and
Security Protocols, Part of the Federated Logic Conference, Trento,
Italy, July 1999.
[174] David Monniaux. Decision procedures for the analysis of
cryptographic protocols by logics of belief. In 12th Computer
Security Foundations Workshop, pages 44-54, Mordano, Italy, June
1999. IEEE Computer Society.
[175] Harald Ruess and Jonathan Millen. Local secrecy for state-based
models. In Formal Methods and Computer Security (FMCS),
Chicago, IL, July 2000.
25
[176] N.S. Pendharkar and K. Gopinath. Formal verification of an O.S.
submodule. In V. Arvind and R. Ramanujin, editors, 18th Conference
on the Foundations of Software Technology and Theoretical Computer
Science, volume 1530 of Lecture Notes in Computer Science, pages
197-208, Madras, India, December 1998. Springer-Verlag.
[177] Rapha"el Couturier and Dominique M'ery. An experiment in
parallelizing an application using formal methods. In Alan J. Hu and
Moshe Y. Vardi, editors, Computer-Aided Verification, CAV '98,
volume 1427 of Lecture Notes in Computer Science, pages 345-356,
Vancouver, Canada, June 1998. Springer-Verlag.
[178] Dmitri Chkliaev, Jozef Hooman, and Peter van der Stok. Mechanical
verification of a non-blocking atomic commitment protocol. In
International Workshop on Distributed System Validation and
Verification (DSVV'2000), pages E96-E103, Taipei, Taiwan, April
2000.
[179] Dmitri Chkliaev, Jozef Hooman, and Peter van der Stok.
Serializability preserving extensions of concurrency control protocols.
In D. Bjorner, M. Broy, and A.V. Zamulin, editors, Third
International Andrei Ershov Memorial Conference: Perspectives of
System Informatics, PSI'99, volume 1755 of Lecture Notes in
Computer Science, pages 180-193, Novosibirsk, Russia, July 1999.
Springer-Verlag.
[180] Dmitri Chkliaev, Jozef Hooman, and Peter van der Stok. Mechanical
verification of transaction processing systems. In Third International
Conference on Formal Engineering Methods (ICFEM 2000), pages
89-97, York, England, November 200. IEEE Computer Society.
[181] Rapha"el Couturier. Formal engineering of the bitonic sort using PVS.
In Proceedings, 2nd. Irish Workshop in Formal Methods, Cork,
Ireland, July 1998. Electronic Workshops in Computing
(http://ewic.org.uk/ewic/).
[182] Marco Devillers, David Griffioen, Judi Romijn, and Frits Vaandrager.
Verification of a leader election protocol: Formal methods applied to
IEEE 1394. Formal Methods in Systems Design, 16(3):307-320, June
2000.
[183] Marcelo Glusman and Shmuel Katz. Mechanizing proofs of
computation equivalence. In Nicolas Halbwachs and Doron Peled,
editors, Computer-Aided Verification, CAV '99, volume 1633 of
Lecture Notes in Computer Science, pages 354-367, Trento, Italy,
July 1999. Springer-Verlag.
26
[184] Klaus Havelund. Mechanical verification of a garbage collector. In
Jos'e Rolim et al., editors, Parallel and Distributed Processing
(Combined Proceedings of 11 Workshops), volume 1586 of Lecture
Notes in Computer Science, pages 1258-1283, San Juan, Puerto Rico,
April 1999. Springer-Verlag. Presented at the Workshop on Formal
Methods for Parallel Programming: Theory and Applications
(FMPPTA).
[185] Jozef Hooman. Formal verification of the binary exponential backoff
protocol. Proceedings of the Estonian Academy of Sciences (Special
issue on the 9th Nordic Workshop on Programming Theory),
4(2):89-105, 1998. Also available at
http://www.win.tue.nl/cs/tt/hooman/BEB.html.
[186] Paul Jackson. Verifying a garbage collection algorithm. In Jim
Grundy and Malcolm Newey, editors, Theorem Proving in Higher
Order Logics: 11th International Conference, TPHOLs '98, volume
1479 of Lecture Notes in Computer Science, pages 225-244,
Canberra, Australia, September 1998. Springer-Verlag.
[187] Abdel Mokkedem, Ravi M. Hosabettu, Michael D. Jones, and
Ganesh C. Gopalakrishnan. Formalization and analysis of a solution
to the PCI 2.1 bus transaction ordering problem. Formal Methods in
Systems Design, 16(1):93-119, January 2000.
[188] John Penix, Dale Martin, Peter Frey, Radharamanan Radhakrishnan,
Perry Alexander, and Phillip A. Wilsey. Experiences in verifying
parallel simulation algorithms. In Mark Ardis, editor, Second
Workshop on Formal Methods in Software Practice (FMSP '98),
pages 16-23, Clearwater Beach, FL, March 1998. Association for
Computing Machinery.
[189] Kothanda Umamageswaran, Krishnan Subramani, Philip A. Wilsey,
and Perry Alexander. Formal verification and empirical analysis of
rollback relaxation. Journal of Systems Architecture (formerly
published as Microprocessing and Microprogramming: the Euromicro
Journal), 44(6-7):473-495, March 1998.
[190] V. S. Alagar, D. Muthiayen, and F. Pompeo. From behavioral
specification to axiomatic description of real-time reactive systems.
In Fifth IEEE Real-Time Technology and Applications Symposium,
Work-In-Progress Session, Vancouver, British Columbia, Canada,
June 1999. IEEE Computer Society. Available at
http://www.cs.concordia.ca/"faculty/manas/rtas99wip/.
[191] Andren Alborghetti, Angelo Gargantini, and Angelo Morzenti.
Providing automated support to deductive analysis of time critical
27
systems. In Mehdi Jazayeri and Helmut Schauer, editors, Software
Engineering_ESEC/FSE '97: Sixth European Software Engineering
Conference and Fifth ACM SIGSOFT Symposium on the
Foundations of Software Engineering, volume 1301 of Lecture Notes
in Computer Science, pages 211-226, Zurich, Switzerland, September
1997. Springer-Verlag.
[192] Myla Archer and Constance Heitmeyer. Mechanical verification of
timed automata: A case study. In IEEE Real-Time Technology and
Applications Symposium (RTAS'96), pages 192-203, Brookline, MA,
June 1996. IEEE Computer Society.
[193] M. Archer and C. Heitmeyer. TAME: A specialized specification and
verification system for timed automata. In Azer Bestavros, editor,
Work In Progress (WIP) Proceedings of the 17th IEEE Real-Time
Systems Symposium (RTSS'96), pages 3-6, Washington, DC,
December 1996. The WIP Proceedings is available at
http://www.cs.bu.edu/pub/ieee-rts/rtss96/wip/proceedings.
[194] Leon Bun. Checking properties of ASTRAL specifications with PVS.
In Proceedings of 2nd Annual Conference of the Advanced School for
Computing and Imaging (ASCI'96), pages 102-107, Lommel,
Belgium, June 1996. Available at
http://sepc.twi.tudelft.nl/"leonbun/papers/asci96.ps.
[195] Leon Bun. Embedding Astral in PVS. In Proceedings of 3rd Annual
Conference of the Advanced School for Computing and Imaging
(ASCI'97), pages 130-136, Lommel, Belgium, June 1997. Available
at http://sepc.twi.tudelft.nl/"leonbun/papers/asci97.ps.
[196] F. S. de Boer, H. Tej, W.-P. de Roever, and M. van Hulst.
Compositionality in real-time shared variable concurrency. In Bengt
Jonsson and Joachim Parrow, editors, Formal Techniques in
Real-Time and Fault-Tolerant Systems, volume 1135 of Lecture Notes
in Computer Science, pages 420-439, Uppsala, Sweden, September
1996. Springer-Verlag.
[197] Philippe Du Bois, Eric Dubois, and Jean-Marc Zeippen. On the use
of a formal RE language: The generalized railroad crossing problem.
In 3rd IEEE International Symposium on Requirements Engineering,
pages 128-137, Annapolis, MD, January 1997. IEEE Computer
Society.
[198] Bruno Dutertre. The Priority Ceiling Protocol: Formalization and
analysis using PVS. Technical report, System Design Laboratory,
SRI International, Menlo Park, CA, October 1999. Available at
http://www.sdl.sri.com/dsa/publis/prio-ceiling.html.
28
[199] Bruno Dutertre and Victoria Stavridou. Formal analysis for realtime
scheduling. In 19th AIAA/IEEE Digital Avionics Systems
Conference, Philadelphia, PA, October 2000.
[200] Bruno Dutertre. Formal analysis of the priority ceiling protocol. In
Real Time Systems Symposium, Orlando, FL, December 2000. IEEE
Computer Society. To appear.
[201] Simon Fowler and Andy Wellings. Formal analysis of a real-time
kernel specification. In Bengt Jonsson and Joachim Parrow, editors,
Formal Techniques in Real-Time and Fault-Tolerant Systems, volume
1135 of Lecture Notes in Computer Science, pages 440-458, Uppsala,
Sweden, September 1996. Springer-Verlag.
[202] Simon Fowler and Andy Wellings. Formal development of a real-time
kernel. In Real Time Systems Symposium, pages 220-229, San
Francisco, CA, December 1997. IEEE Computer Society.
[203] Jozef Hooman. Correctness of real time systems by construction. In
H. Langmaack, W.-P. de Roever, and J. Vytopil, editors, Formal
Techniques in Real-Time and Fault-Tolerant Systems, volume 863 of
Lecture Notes in Computer Science, pages 19-40, L"ubeck, Germany,
September 1994. Springer-Verlag.
[204] Jozef Hooman. Using PVS for an assertional verification of the
RPC-Memory specification problem. In Manfred Broy, Stephan
Merz, and Katharina Spies, editors, Formal Systems Specification:
The RPC-Memory Specification Case Study, volume 1169 of Lecture
Notes in Computer Science, pages 275-304. Springer-Verlag, 1996.
[205] Jozef Hooman. Verification of distributed real-time and fault-tolerant
protocols. In Michael Johnson, editor, Algebraic Methodology and
Software Technology, AMAST'97, volume 1349 of Lecture Notes in
Computer Science, pages 261-275, Sydney, Australia, December
1997. Springer-Verlag.
[206] Jozef Hooman. Compositional verification of real-time applications.
In Willem-Paul de Roever, Hans Langmaack, and Amir Pnueli,
editors, Compositionality: The Significant Difference (Revised
lectures from International Symposium COMPOS'97), volume 1536
of Lecture Notes in Computer Science, pages 276-300, Bad Malente,
Germany, September 1997. Springer-Verlag.
[207] Paul Z. Kolano. Proof assistance for real-time systems using an
interactive theorem prover. In J.-P. Katoen, editor, Formal Methods
for Real-Time and Probabilistic Systems (Proceedings 5th
International AMAST Workshop, ARTS'99), volume 1601 of Lecture
29
Notes in Computer Science, pages 315-333, Bamberg, Germany, May
1999. Springer-Verlag.
[208] Paul Kolano, Richard Kemmerer, and Dino Mandrioli. Parallel
refinement mechanisms for real-time systems. In Tom Maibaum,
editor, Fundamental Approaches to Software Engineering, FASE
2000, number 1783 in Lecture Notes in Computer Science, pages
35-50, Berlin, Germany, March/April 2000. Springer-Verlag.
[209] Darmalingum Muthiayen. Real-Time Reactive System
Development_A Formal Approach Based on UML and PVS. PhD
thesis, Department of Computer Science at Concordia University,
Montreal, Canada, January 2000.
[210] Natarajan Shankar. Verification of real-time systems using PVS. In
Costas Courcoubetis, editor, Computer-Aided Verification, CAV '93,
volume 697 of Lecture Notes in Computer Science, pages 280-291,
Elounda, Greece, June/July 1993. Springer-Verlag.
[211] Jens Ulrik Skakkebaek. A Verification Assistant for a Real-Time
Logic. PhD thesis, Department of Computer Science, Technical
University of Denmark, Lyngby, Denmark, November 1994.
[212] Jens U. Skakkebaek and N. Shankar. Towards a Duration Calculus
proof assistant in PVS. In H. Langmaack, W.-P. de Roever, and
J. Vytopil, editors, Formal Techniques in Real-Time and
Fault-Tolerant Systems, volume 863 of Lecture Notes in Computer
Science, pages 660-679, L"ubeck, Germany, September 1994.
Springer-Verlag.
[213] Pertti Kellom"aki. Verification of reactive systems using DisCo and
PVS. In Formal Methods Europe FME '97, volume 1313 of Lecture
Notes in Computer Science, pages 589-604, Graz, Austria,
September 1997. Springer-Verlag.
[214] M. Archer and C. Heitmeyer. Verifying hybrid systems modeled as
timed automata: A case study. In Oded Maler, editor, Proceedings of
the International Workshop on Hybrid and Real-Time Systems
(HART'97), volume 1201 of Lecture Notes in Computer Science,
pages 171-185, Grenoble, France, March 1997. Springer-Verlag.
[215] Thomas A. Henzinger and Vlad Rusu. Reachability verification for
hybrid automata. In Thomas A. Henzinger and Shankar Sastry,
editors, Hybrid Systems: Computation and Control (First
International Workshop, HSCC'98), volume 1386 of Lecture Notes in
Computer Science, pages 190-204, Berkeley, CA, April 1998.
Springer-Verlag.
30
[216] Jan Vitt and Jozef Hooman. Assertional specification and verification
using PVS of the steam boiler control system. In Jean-Raymond
Abrial, Egon Boerger, and Hans Langmaack, editors, Formal
Methods for Industrial Applications: Specifying and Programming the
Steam Boiler Control, volume 1165 of Lecture Notes in Computer
Science, pages 453-472. Springer-Verlag, 1996.
[217] Roel Bloo, Jozef Hooman, and Edwin de Jong. Semantical aspects of
an architecture for distributed embedded systems. In Proceedings of
the 2000 ACM Symposium on Applied Computing (SAC 2000),
volume 1, pages 149-155, Como, Italy, March 2000. Association for
Computing Machinery.
[218] Edwin de Jong, Jaco van de Pol, and Jozef Hooman. Refinement in
requirements specification and analysis: A case study. In 7th IEEE
International Conference and Workshop on the Engineering of
Computer Based Systems (ECBS), pages 290-298, Edinburgh,
Scotland, April 2000. IEEE Computer Society.
[219] Jaco van de Pol, Jozef Hooman, and Edwin de Jong. Modular formal
specification of data and behaviour. In K. Araki, A. Galloway, and
K. Taguchi, editors, Proceedings 1st Conference on Integrated Formal
Methods (IFM'99), pages 109-128, York, UK, June 1999. Springer.
[220] Frank S. de Boer and Marten van Hulst. Local nondeterminism in
asynchronously communicating processes. In Formal Methods Europe
FME '96, volume 1051 of Lecture Notes in Computer Science, pages
367-384, Oxford, UK, March 1996. Springer-Verlag.
[221] Victoria Chernyakhovsky, Peter Frey, Radharamanan Radhakrihnan,
Philip A. Wilsey, Perry Alexander, and Harold W. Carter. A formal
framework for specifying and verifying time warp optimizations. In
Jos'e Rolim et al., editors, Parallel and Distributed Processing
(Combined Proceedings of 11 Workshops), volume 1586 of Lecture
Notes in Computer Science, pages 1228-1242, San Juan, Puerto Rico,
April 1999. Springer-Verlag. Presented at the Workshop on Formal
Methods for Parallel Programming: Theory and Applications
(FMPPTA).
[222] Peter Frey, Radharamanan Radhakrishnan, Philip A. Wilsey, Perry
Alexander, and Harold W. Carter. An extensible formal framework
for the specification and verification of an optimistic simulation
protocol. In Proceedings of the 32nd Annual Hawaii International
Conference on System Sciences. IEEE Computer Society, January
1999. Available at http://computer.org/conferen/proceed/
hicss/0001/00013/00013049abs.htm.
31
[223] Jozef Hooman. Developing proof rules for distributed real-time
systems with PVS. In Bettina Buth, Rudolf Berghammer, and Jan
Peleska, editors, Tools for System Development and Verification,
BISS Monographs, pages 120-139, Aachen, Germany, 1998. Shaker
Verlag. Proceedings of a workshop held at Bremen in 1996.
[224] Pertti Kellom"aki. Mechanizing invariant proofs of joint action
systems. In Fourth Symposium on Programming Languages and
Software Tools, pages 141-152, Visegrad, Hungary, June 1995.
Available at http:
//www.cs.tut.fi/"pk/papers/visegrad-95/visegrad.ps.gz.
[225] Pertti Kellom"aki. Using auxiliary knowledge in automating invariant
proofs. In International Conference on Theorem Proving in Higher
Order Logics, pages 57-68, Turku, Finland, August 1996.
Supplementary proceedings, available at
http://www.tucs.abo.fi/publications/general/G1.html.
[226] David Lesens and Hassen Sa"idi. Automatic verification of
parameterized networks of processes by abstraction. In Faron Moller,
editor, 2nd International Workshop on Verification of Infinite State
Systems: Infinity '97, volume 9 of Electronic Notes in Theoretical
Computer Science, Bologna, Italy, July 1997. Elsevier. Available at
http://www.elsevier.nl/cas/tree/store/tcs/free/entcs/
store/tcs9/tcs9009%.ps.
[227] N. Shankar. A lazy approach to compositional verification. Technical
Report SRI-CSL-93-8, Computer Science Laboratory, SRI
International, Menlo Park, CA, December 1993.
[228] Marten van Hulst. Compositional Verification of Parallel Programs
using Epistemic Logic and Abstract Assertional Languages. PhD
thesis, Faculteit Wiskunde en Informatica, Universiteit Utrecht, The
Netherlands, June 1995.
[229] Jozef Hooman. Verifying part of the ACCESS.bus protocol using
PVS. In P. S. Thiagarajan, editor, 15th Conference on the
Foundations of Software Technology and Theoretical Computer
Science, volume 1026 of Lecture Notes in Computer Science, pages
96-110, Bangalore, India, December 1995. Springer-Verlag.
[230] Klaus Havelund and N. Shankar. Experiments in theorem proving
and model checking for protocol verification. In Formal Methods
Europe FME '96, volume 1051 of Lecture Notes in Computer Science,
pages 662-681, Oxford, UK, March 1996. Springer-Verlag.
32
[231] Lars Kh"une, Jozef Hooman, and Willem-Paul de Roever. Towards
mechanical verification of parts of the IEEE P1394 serial bus. In 2nd
International Workshop on Applied Formal Methods in System
Design, Zagreb, Croatia, June 1997. Available at
http://www.win.tue.nl/cs/tt/hooman/P1394.html.
[232] Abdel Mokkedem and Tim Leonard. Formal verification of the Alpha
21364 network protocol. In Mark Aargaard and John Harrison,
editors, Theorem Proving in Higher Order Logics: 13th International
Conference, TPHOLs 2000, volume 1869 of Lecture Notes in
Computer Science, pages 443-461, Portland, OR, August 2000.
Springer-Verlag.
[233] Micha"el Rusinowitch, Sorin Stratulat, and Francis Klay. Mechanical
verification of a generic incremental ABR conformance algorithm. In
E. A. Emerson and A. P. Sistla, editors, Computer-Aided
Verification, CAV '2000, volume 1855 of Lecture Notes in Computer
Science, pages 344-357, Chicago, IL, July 2000. Springer-Verlag.
[234] John Herbert, Bruno Dutertre, Robert Riemenschneider, and
Victoria Stavridou. A formalization of software architecture. In
Jeannette Wing and Jim Woodcock, editors, FM99: The World
Congress in Formal Methods, volume 1708 and 1709 of Lecture Notes
in Computer Science, pages 116-133, Toulouse, France, September
1999. Springer-Verlag. Pages 1-938 are in the first volume, 939-1872
in the second.
[235] Jozef Hooman. Program design in PVS. In K.Berghammer,
J.Peleska, and B. Buth, editors, Workshop on Tool Support for
System Development and Verification, Bremen, Germany, 1997.
Available at http://www.win.tue.nl/cs/tt/hooman/PDPVS.html.
[236] Michel L'evy and Laurent Trilling. A PVS-based approach for
teaching constructing correct iterations. In Jeannette Wing and Jim
Woodcock, editors, FM99: The World Congress in Formal Methods,
volume 1708 and 1709 of Lecture Notes in Computer Science, pages
1859-1860, Toulouse, France, September 1999. Springer-Verlag.
Pages 1-938 are in the first volume, 939-1872 in the second.
[237] Richard Verhoeven and Roland Backhouse. Interfacing program
construction and verification. In Jeannette Wing and Jim Woodcock,
editors, FM99: The World Congress in Formal Methods, volume 1708
and 1709 of Lecture Notes in Computer Science, pages 1128-1146,
Toulouse, France, September 1999. Springer-Verlag. Pages 1-938 are
in the first volume, 939-1872 in the second.
33
[238] Ralf Behnke, Rudolf Berghammer, and S"onke Magnussen.
Supporting algebraic program derivation by PVS. In Bettina Buth,
Rudolf Berghammer, and Jan Peleska, editors, Tools for System
Development and Verification, BISS Monographs, pages 22-40,
Aachen, Germany, 1998. Shaker Verlag. Proceedings of a workshop
held at Bremen in 1996.
[239] Axel Dold. Representing, verifying and applying software
development steps using the PVS system. In V. S. Alagar and
Maurice Nivat, editors, Algebraic Methodology and Software
Technology, AMAST'95, volume 936 of Lecture Notes in Computer
Science, pages 431-445, Montreal, Canada, July 1995.
Springer-Verlag.
[240] Axel Dold. Formal Software Development using Generic
Development Steps. PhD thesis, Universit"at Ulm, Germany, 2000.
[241] N. Shankar. Computer-aided computing. In Bernhard M"oller, editor,
Mathematics of Program Construction '95, volume 947 of Lecture
Notes in Computer Science, pages 50-66. Springer-Verlag, 1995.
[242] N. Shankar. Steps towards mechanizing program transformations
using PVS. Science of Computer Programming, 26(1-3):33-57, 1996.
[243] Bart Jacobs. Behaviour-refinement of coalgebraic specifications with
coinductive correctness proofs. In Michel Bidoit and Max Dauchet,
editors, TAPSOFT '97: Theory and Practice of Software
Development, volume 1214 of Lecture Notes in Computer Science,
pages 787-802, Lille, France, April 1997. Springer-Verlag.
[244] Bart Jacobs. Invariants, bisimulations and the correctness of
coalgebraic refinements. In Michael Johnson, editor, Algebraic
Methodology and Software Technology, AMAST'97, volume 1349 of
Lecture Notes in Computer Science, pages 276-291, Sydney,
Australia, December 1997. Springer-Verlag.
[245] Paul Jackson. Total-correctness refinement for sequential reactive
systems. In Mark Aargaard and John Harrison, editors, Theorem
Proving in Higher Order Logics: 13th International Conference,
TPHOLs 2000, volume 1869 of Lecture Notes in Computer Science,
pages 320-337, Portland, OR, August 2000. Springer-Verlag.
[246] Jens Knappmann. A PVS based tool for developing programs in the
Refinement Calculus. Master's thesis, Institut f"ur Informatik und
Praktische Mathematik der Christian-Albrechts-Universit"at zu Kiel,
Kiel, Germany, October 1996.
34
[247] Karl-Heinz Buth. Automated code generator verification based on
algebraic laws. Procos II Report Kiel KHB 5/1, Christian-Albrechts
Universit"at zu Kiel, Kiel, Germany, September 1995. Available at
ftp://ftp.informatik.uni-kiel.de/pub/kiel/procos/
kiel-khb-5-1.ps.Z.
[248] A. Dold, F. W. von Henke, H. Pfeifer, and H. Ruess. Formal
verification of transformations for peephole optimiztion. In Formal
Methods Europe FME '97, volume 1313 of Lecture Notes in Computer
Science, pages 459-472, Graz, Austria, September 1997.
Springer-Verlag.
[249] A. Dold, T. Gaul, V. Vialard, and W. Zimmermann. ASM-Based
Mechanized Verification of Compiler Backends. In Uwe Gl"asser and
Peter H. Schmitt, editors, Proceedings of the 5th International
Workshop on Abstract State Machines, pages 50-67, Magdeburg,
Germany, September 1998. Available at http://i44www.info.
uni-karlsruhe.de/"verifix/pres/paper/ASM-WS98-DGVZ.p%s.gz.
[250] Axel Dold, Thilo Gaul, and Wolf Zimmermann. Mechanized
verification of compiler backends. In Tiziana Margaria and Bernhard
Steffen, editors, Proceedings of the International Workshop on
Software Tools for Technology Transfer STTT'98, pages 13-22,
Aalborg, Denmark, June 1998. BRICS NS-98-4. Proceedings
available at http://www.brics.dk/NS/98/4/.
[251] Axel Dold and Vincent Vialard. Formal verification of a compiler
back-end generic checker program. In D. Bjorner, M. Broy, and A.V.
Zamulin, editors, Third International Andrei Ershov Memorial
Conference: Perspectives of System Informatics, PSI'99, volume 1755
of Lecture Notes in Computer Science, pages 470-480, Novosibirsk,
Russia, July 1999. Springer-Verlag.
[252] David W. J. Stringer-Calvert, Susan Stepney, and Ian Wand. Using
PVS to prove a Z refinement: A case study. In Formal Methods
Europe FME '97, volume 1313 of Lecture Notes in Computer Science,
pages 573-588, Graz, Austria, September 1997. Springer-Verlag.
[253] David W. J. Stringer-Calvert. Mechanical Verification of Compiler
Correctness. PhD thesis, University of York, Department of
Computer Science, York, England, March 1998. Available at
http://www.csl.sri.com/"dave`sc/papers/thesis.html.
[254] M. Wahab. Verification and abstraction of flow-graph programs with
pointers and computed jumps. Research Report CS-RR-354,
Department of Computer Science, University of Warwick, Coventry,
35
UK, November 1998. Available at
http://www.dcs.warwick.ac.uk/pub/reports/rr/354.html.
[255] Matthew Wahab. Object Code Verification. PhD thesis, Department
of Computer Science, University of Warwick, Coventry, UK,
December 1998. Available at http:
//www.dcs.warwick.ac.uk/pub/reports/theses/wahab98.html.
[256] Tamara Arons and Amir Pnueli. Verifying Tomasulo's algorithm by
refinement. In The Twelfth International Conference on VLSI
Design, pages 306-309, Goa, India, January 1999. IEEE Computer
Society.
[257] Tamarah Arons and Amir Pnueli. A comparison of two verification
methods for speculative instruction execution. In Susanne Graf and
Michael Schwartzbach, editors, Tools and Algorithms for the
Construction and Analysis of Systems (TACAS 2000), number 1785
in Lecture Notes in Computer Science, pages 487-502, Berlin,
Germany, March 2000. Springer-Verlag.
[258] David Cyrluk. Inverting the abstraction mapping: A methodology
for hardware verification. In Mandayam Srivas and Albert Camilleri,
editors, Formal Methods in Computer-Aided Design (FMCAD '96),
volume 1166 of Lecture Notes in Computer Science, pages 172-186,
Palo Alto, CA, November 1996. Springer-Verlag.
[259] David Cyrluk, John Rushby, and Mandayam Srivas. Systematic
formal verification of interpreters. In Michael G. Hinchey and
Shaoying Liu, editors, First International Conference on Formal
Engineering Methods (ICFEM '97), pages 140-149, Hiroshima,
Japan, November 1997. IEEE Computer Society.
[260] Werner Damm and Amir Pnueli. Verifying out-of-order executions.
In Hon F. li and David K. Probst, editors, Advances in Hardware
Design and Verification: IFIP WG10.5 International Conference on
Correct Hardware Design and Verification Methods (CHARME),
pages 23-47, Montreal, Canada, October 1997. Chapman & Hall.
[261] Kathi Fisler. Extending formal reasoning with support for hardware
diagrams. In Ramayya Kumar and Thomas Kropf, editors, Theorem
Provers in Circuit Design (TPCD '94), volume 910 of Lecture Notes
in Computer Science, pages 298-303, Bad Herrenalb, Germany,
September 1994. Springer-Verlag.
[262] Ganesh Gopalakrishnan, Rajnish Ghughal, Ravi Hosabettu,
Abdelillah Mokkedem, and Ratan Nalumasu. Formal modeling and
validation applied to a commercial coherent bus: A case study. In
36
Hon F. li and David K. Probst, editors, Advances in Hardware
Design and Verification: IFIP WG10.5 International Conference on
Correct Hardware Design and Verification Methods (CHARME),
pages 48-62, Montreal, Canada, October 1997. Chapman & Hall.
[263] David Greve. Symbolic simulation of the JEM1 microprocessor. In
Ganesh Gopalakrishnan and Phillip Windley, editors, Formal
Methods in Computer-Aided Design (FMCAD '98), volume 1522 of
Lecture Notes in Computer Science, pages 321-333, Palo Alto, CA,
November 1998. Springer-Verlag.
[264] David Hardin, Matthew Wilding, and David Greve. Transforming
the theorem prover into a digital design tool: From concept car to
off-road vehicle. In Alan J. Hu and Moshe Y. Vardi, editors,
Computer-Aided Verification, CAV '98, volume 1427 of Lecture Notes
in Computer Science, pages 39-44, Vancouver, Canada, June 1998.
Springer-Verlag.
[265] Ravi Hosabettu, Mandayam Srivas, and Ganesh Gopalakrishnan.
Decomposing the proof of correctness of pipelined microprocessors.
In Alan J. Hu and Moshe Y. Vardi, editors, Computer-Aided
Verification, CAV '98, volume 1427 of Lecture Notes in Computer
Science, pages 122-134, Vancouver, Canada, June 1998.
Springer-Verlag.
[266] Ravi Hosabettu, Mandayam Srivas, and Ganesh Gopalakrishnan.
Proof of correctness of a processor with reorder buffer using the
completion functions approach. In Nicolas Halbwachs and Doron
Peled, editors, Computer-Aided Verification, CAV '99, volume 1633
of Lecture Notes in Computer Science, pages 47-59, Trento, Italy,
July 1999. Springer-Verlag.
[267] Ravi Hosabettu, Ganesh Gopalakrishnan, and Mandayam Srivas.
Proof of correctness of a processor implementing Tomasulo's
algorithm without a reorder buffer. In Advances in Hardware Design
and Verification: IFIP WG10.5 International Conference on Correct
Hardware Design and Verification Methods (CHARME '99), volume
1703 of Lecture Notes in Computer Science, pages 8-22, Bad
Herrenalb, Germany, September 1999. Springer-Verlag.
[268] Ravi Hosabettu, Ganesh Gopalakrishnan, and Mandayam Srivas.
Verifying microarchitectures that support speculation and exceptions.
In E. A. Emerson and A. P. Sistla, editors, Computer-Aided
Verification, CAV '2000, volume 1855 of Lecture Notes in Computer
Science, pages 521-537, Chicago, IL, July 2000. Springer-Verlag.
37
[269] Steven D. Johnson, Paul S. Miner, and Albert Camlleri. Studies of
the single-pulser in various reasoning systems. In Ramayya Kumar
and Thomas Kropf, editors, Theorem Provers in Circuit Design
(TPCD '94), volume 910 of Lecture Notes in Computer Science,
pages 126-145, Bad Herrenalb, Germany, September 1994.
Springer-Verlag.
[270] Steven D. Johnson and Paul S. Miner. Integrated reasoning support
in system design: Design derivation and theorem proving. In Hon F.
li and David K. Probst, editors, Advances in Hardware Design and
Verification: IFIP WG10.5 International Conference on Correct
Hardware Design and Verification Methods (CHARME), pages
255-272, Montreal, Canada, October 1997. Chapman & Hall.
[271] James Leathrum, Jr. Fundamental hardware design in PVS. In
C. Michael Holloway and Kelly J. Hayhurst, editors, LFM' 97:
Fourth NASA Langley Formal Methods Workshop, NASA Conference
Publication 3356, pages 193-204, Hampton, VA, September 1997.
NASA Langley Research Center. Available at
http://atb-www.larc.nasa.gov/Lfm97/proceedings/.
[272] Xiaoshan Li, Antonio Cau, Ben Moszkowski, Nick Coleman, and
Hussein Zedan. Proving the correctness of the interlock mechanism
in processor design. In Hon F. li and David K. Probst, editors,
Advances in Hardware Design and Verification: IFIP WG10.5
International Conference on Correct Hardware Design and
Verification Methods (CHARME), pages 5-22, Montreal, Canada,
October 1997. Chapman & Hall.
[273] Paul S. Miner and Steven D. Johnson. Verification of an optimized
fault-tolerant clock synchronization circuit: A case study exploring
the boundary between formal reasoning systems. In Mary Sheeran
and Satnam Singh, editors, Designing Correct Circuits, Bastad,
Sweden, September 1996. Electronic Workshops in Computing
(http://ewic.org.uk/ewic/).
[274] Paul S. Miner, Shyamsundar Pullela, and Steven D. Johnson.
Interaction of formal design systems in the development of a
fault-tolerant clock synchronization circuit. In 13th Symposium on
Reliable Distributed Systems, pages 128-137, Dana Point, CA,
October 1994. IEEE Computer Society.
[275] Paul S. Miner and James F. Leathrum, Jr. Verification of IEEE
compliant subtractive division algorithms. In Mandayam Srivas and
Albert Camilleri, editors, Formal Methods in Computer-Aided Design
38
(FMCAD '96), volume 1166 of Lecture Notes in Computer Science,
pages 64-78, Palo Alto, CA, November 1996. Springer-Verlag.
[276] Steven P. Miller and Mandayam Srivas. Formal verification of the
AAMP5 microprocessor: A case study in the industrial use of formal
methods. In WIFT '95: Workshop on Industrial-Strength Formal
Specification Techniques, pages 2-16, Boca Raton, FL, 1995. IEEE
Computer Society.
[277] Amir Pnueli and Tamara Arons. Verification of data-insensitive
circuits: An in-order-retirement case study. In Ganesh
Gopalakrishnan and Phillip Windley, editors, Formal Methods in
Computer-Aided Design (FMCAD '98), volume 1522 of Lecture Notes
in Computer Science, pages 351-368, Palo Alto, CA, November 1998.
Springer-Verlag.
[278] H. Ruess, N. Shankar, and M. K. Srivas. Modular verification of SRT
division. In Rajeev Alur and Thomas A. Henzinger, editors,
Computer-Aided Verification, CAV '96, volume 1102 of Lecture Notes
in Computer Science, pages 123-134, New Brunswick, NJ,
July/August 1996. Springer-Verlag.
[279] H. Ruess, N. Shankar, and M. K. Srivas. Modular verification of SRT
division. Formal Methods in Systems Design, 14(1):45-73, January
1999.
[280] Sreeranga P. Rajan and Masahiro Fujita. ATM switch design:
Parametric high-level modeling and formal verification. In Michael
Johnson, editor, Algebraic Methodology and Software Technology,
AMAST'97, volume 1349 of Lecture Notes in Computer Science,
pages 437-450, Sydney, Australia, December 1997. Springer-Verlag.
[281] S. P. Rajan, M. Fujita, K. Yuan, and M. T-C. Lee. ATM switch
design by high level modeling, formal verification, and high level
synthesis. ACM Transactions on Design Automation of Electronic
Systems (TODAES), 3(4):554-562, October 1998.
[282] Mandayam K. Srivas and Steven P. Miller. Applying formal
verification to a commercial microprocessor. In Steven D. Johnson,
editor, CHDL '95: 12th Conference on Computer Hardware
Description Languages and their Applications, pages 493-502, Chiba,
Japan, August 1995. Proceedings published in a single volume jointly
with ASP-DAC '95, CHDL '95, and VLSI '95, IEEE Catalog no.
95TH8102.
[283] Mandayam K. Srivas and Steven P. Miller. Formal verification of the
AAMP5 microprocessor. In Michael G. Hinchey and Jonathan P.
39
Bowen, editors, Applications of Formal Methods, Prentice Hall
International Series in Computer Science, chapter 7, pages 125-180.
Prentice Hall, Hemel Hempstead, UK, 1995.
[284] Mandayam K. Srivas and Steven P. Miller. Applying formal
verification to the AAMP5 microprocessor: A case study in the
industrial use of formal methods. Formal Methods in Systems Design,
8(2):153-188, March 1996.
[285] Nazanin Mansouri and Ranga Vemuri. Automated correctness
condition generation for formal verification of synthesized RTL
designs. Formal Methods in Systems Design, 16(1):59-91, January
2000.
[286] Naren Narasimhan, Elena Teica, Rajesh Radhakrishnan, Sriram
Govindarajan, and Ranga Vemuri. Theorem proving guided
development of formal assertions in a resource-constrained scheduler
for high-level synthesis. In Andreas Kuehlmann, editor, International
Conference on Computer Design (ICCD'98), Austin, TX, October
1998. IEEE Computer Society.
[287] Naren Narasimhan and Ranga Vemuri. On the effectiveness of
theorem proving guided discovery of formal assertions for a register
allocator in a high-level synthesis system. In Jim Grundy and
Malcolm Newey, editors, Theorem Proving in Higher Order Logics:
11th International Conference, TPHOLs '98, volume 1479 of Lecture
Notes in Computer Science, pages 367-386, Canberra, Australia,
September 1998. Springer-Verlag.
[288] P. Sreeranga Rajan. Transformations in high level synthesis:
Specification and verification. Technical Report NL-TN 118/94,
Philips Research Laboratories, Eindhoven, The Netherlands, April
1994. Revised version available as SRI Technical Report
SRI-CSL-94-10, October 1994.
[289] Sreeranga P. Rajan. Correctness of transformations in high level
synthesis. In Steven D. Johnson, editor, CHDL '95: 12th Conference
on Computer Hardware Description Languages and their
Applications, pages 597-603, Chiba, Japan, August 1995.
Proceedings published in a single volume jointly with ASP-DAC '95,
CHDL '95, and VLSI '95, IEEE Catalog no. 95TH8102.
[290] Sreeranga P. Rajan. Transformations on Dependency Graphs:
Formal Specification and Efficient Mechanical Verification. PhD
thesis, Department of Computer Science, University of British
Columbia, Vancouver, Canada, October 1995.
40
[291] Ratan Nalumasu and Ganesh Gopalakrishnan. Deriving efficient
cache coherence protocols through refinement. In Formal Methods for
Parallel Programming: Theory and Applications (FMPPTA),
Orlando, FL, March 98. Available at
http://www.loria.fr/"mery/lncs`fmppta98/paper7.ps.
[292] Seungjoon Park. Computer Assisted Analysis of Multiprocessor
Memory Systems. PhD thesis, Department of Electrical Engineering,
Stanford University, June 1996.
[293] Seungjoon Park and David L. Dill. An executable specification,
analyzer and verifier for relaxed memory order: With formal proofs.
Submitted for publication; an earlier version (without proofs) is
available [328], 1996.
[294] Seungjoon Park and David L. Dill. Verification of cache coherence
protocols by aggregation of distributed transactions. Theory of
Computing Systems, 31(4):355-376, 1998.
[295] Sreeranga Rajan, P. Venkat Rangan, and Harrick M. Vin. A formal
basis for structured multimedia collaborations. In Proceedings of the
2nd IEEE International Conference on Multimedia Computing and
Systems, pages 194-201, Washington, DC, May 1995. IEEE
Computer Society.
[296] V. Rusu, L. du Bousquet, and T. J'eron. An approach to symbolic
test generation. In 2nd International Workshop on Integrated Formal
Method (IFM'00), number 1945 in Lecture Notes in Computer
Science, pages 338-357, Dagstuhl, Germany, November 2000.
Springer-Verlag.
[297] T. C. Nicholas Graham. A method for the formal testing of program
visualization tools. In Proceedings of the Fourth Workshop on
Program Comprehension, pages 45-54, Berlin, Germany, March 1996.
IEEE Computer Society.
[298] Neeraj Suri and Purnendu Sinha. On the use of formal methods for
validation. In Fault Tolerant Computing Symposium 28, pages
390-399, Munich, Germany, June 1998. IEEE Computer Society.
[299] Purnendu Sinha and Neeraj Suri. Identification of test cases using a
formal fault injection approach. In Fault Tolerant Computing
Symposium 29, pages 314-321, Madison, WI, June 1999. IEEE
Computer Society.
[300] Purnendu Sinha and Neeraj Suri. Formal techniques for dependable
real time protocols. In Real Time Systems Symposium, Phoenix, AZ,
December 1999. IEEE Computer Society.
41
[301] Shaz Qadeer and Natarajan Shankar. Verifying a self-stabilizing
mutual exclusion algorithm. In David Gries and Willem-Paul
de Roever, editors, IFIP International Conference on Programming
Concepts and Methods (PROCOMET '98), pages 424-443, Shelter
Island, NY, June 1998. Chapman & Hall.
[302] Sandeep Kulkarni, John Rushby, and N. Shankar. A case study in
component-based mechanical verification of fault-tolerant programs.
In ICDCS Workshop on Self-Stabilizing Systems, pages 33-40,
Austin, TX, June 1999. IEEE Computer Society.
[303] Angelo Gargantini and Elvinia Riccobene. Encoding Abstract State
Machines in PVS. In Yuri Gurevich, Phillip W. Kutter, Martin
Odersky, and Lothar Thiele, editors, Abstract State Machines:
Theory and Applications (ASM 2000), number 1912 in Lecture Notes
in Computer Science, pages 303-322, Monte Verit`a, Switzerland,
March 2000. Springer-Verlag.
[304] Jean Paul Bodeveix, Mamoun Filali, and C'esar A. Mu"noz. A
formalization of the B-Method in Coq and PVS. In FM99: The
World Congress in Formal Methods, User Group Meeting 2. The
B-Method: Applying B in an Industrial Context: Tools, Lessons and
Techniques, September 1999. Available on the CD-ROM for [329].
[305] C'esar Mu"noz and John Rushby. Structural embeddings:
Mechanization with method. In Jeannette Wing and Jim Woodcock,
editors, FM99: The World Congress in Formal Methods, volume 1708
and 1709 of Lecture Notes in Computer Science, pages 452-471,
Toulouse, France, September 1999. Springer-Verlag. Pages 1-938 are
in the first volume, 939-1872 in the second.
[306] Richard F. Paige and Jonathan S. Ostroff. Developing BON as an
industrial-strength formal method. In Jeannette Wing and Jim
Woodcock, editors, FM99: The World Congress in Formal Methods,
volume 1708 and 1709 of Lecture Notes in Computer Science, pages
834-853, Toulouse, France, September 1999. Springer-Verlag. Pages
1-938 are in the first volume, 939-1872 in the second.
[307] S. Bensalem, P. Caspi, C. Parent-Vigouroux, and C. Dumas. A
methodology for proving control systems with Lustre and PVS. In
Charles B. Weinstock and John Rushby, editors, Dependable
Computing for Critical Applications_7, volume 12 of Dependable
Computing and Fault Tolerant Systems, pages 89-107, San Jose, CA,
January 1999. IEEE Computer Society.
[308] John Rushby and Mandayam Srivas. Using PVS to prove some
theorems of David Parnas. In Jeffrey J. Joyce and Carl-Johan H.
42
Seger, editors, Higher Order Logic Theorem Proving and its
Applications (6th International Workshop, HUG '93), volume 780 of
Lecture Notes in Computer Science, pages 163-173, Vancouver,
Canada, August 1993. Springer-Verlag.
[309] Mats P. E. Heimdahl and Barbara J. Czerny. Using PVS to analyze
hierarchical state-based requirements for completeness and
consistency. In IEEE High-Assurance Systems Engineering Workshop
(HASE '96), pages 252-262, Niagara on the Lake, Canada, October
1996.
[310] Mats P.E. Heimdahl. Verifying communication related safety
constraints in RSML specifications. In C. Michael Holloway and
Kelly J. Hayhurst, editors, LFM' 97: Fourth NASA Langley Formal
Methods Workshop, NASA Conference Publication 3356, pages
115-128, Hampton, VA, September 1997. NASA Langley Research
Center. Available at
http://atb-www.larc.nasa.gov/Lfm97/proceedings/.
[311] Mats P. E. Heimdahl and Jeffrey M. Thompson. Specification and
analysis of system level inter-component communication. In
Michael G. Hinchey and Shaoying Liu, editors, First International
Conference on Formal Engineering Methods (ICFEM '97), pages
192-201, Hiroshima, Japan, November 1997. IEEE Computer Society.
[312] Barbara J. Czerny and Mats P. E. Heimdahl. Automated integrative
analysis of state-based requirements. In D. Redmiles and
B. Nuseibeh, editors, Thirteenth IEEE Conference on Automated
Software Engineering (ASE '98), Nonolulu, Hawaii, October 1998.
IEEE Computer Society.
[313] Mats P. E. Heimdahl, Jeffrey M. Thompson, and Barbara J. Czerny.
Specification and analysis of intercomponent communication. IEEE
Computer, 31(4):47-54, April 1998.
[314] Sten Agerholm. Translating specifications in VDM-SL to PVS. In
Joakim von Wright, Jim Grundy, and John Harrison, editors,
Theorem Proving in Higher Order Logics: 9th International
Conference, TPHOLs '96, volume 1125 of Lecture Notes in Computer
Science, pages 1-16, Turku, Finland, August 1996. Springer-Verlag.
[315] Sten Agerholm, Juan Bicarregui, and Savi Maharaj. On the
verification of VDM specification and refinement with PVS. In Juan
Bicarregui, editor, Proof in VDM: Case Studies, FACIT (Formal
Approaches to Computing and Information Technology), chapter 6,
pages 157-190. Springer-Verlag, London, UK, 1997.
43
[316] Savi Maharaj and Juan Bicarregui. On the verification of VDM
specification and refinement with PVS. In M. Lowry and Y. Ledru,
editors, 12th IEEE International Conference on Automated Software
Engineering (ASE '97), pages 280-289, Incline Village, NV,
November 1997. IEEE Computer Society.
[317] Perry Alexander, Murali Rangarajan, and Phillip Baraona. A brief
summary of VSPEC. In Jeannette Wing and Jim Woodcock, editors,
FM99: The World Congress in Formal Methods, volume 1708 and
1709 of Lecture Notes in Computer Science, pages 1068-1086,
Toulouse, France, September 1999. Springer-Verlag. Pages 1-938 are
in the first volume, 939-1872 in the second.
[318] A. A. Adams, H. Gottliebsen, S. A. Linton, and U. Martin.
VSDITLU: A verifiable symbolic definite integral table look-up. In
Automated Deduction_CADE-16, volume 1632 of Lecture Notes in
Artificial Intelligence, pages 112-126, Trento, Italy, July 1999.
Springer-Verlag.
[319] A. A. Adams, H. Gottliebsen, S. A. Linton, and U. Martin.
Automated theorem proving in support of computer algebra:
Symbolic definite integration as a case study. In Proceedings of the
1999 International Symposium on Symbolic and Algebraic
Computation, (ISSAC '99), pages 253-260, Vancouver, B.C.,
Canada, July 1999. Association for Computing Machinery.
[320] Bettina Buth, Rachel Cardell-Oliver, and Jan Peleska. Combining
tools for the verification of fault-tolerant systems. In Bettina Buth,
Rudolf Berghammer, and Jan Peleska, editors, Tools for System
Development and Verification, BISS Monographs, pages 41-69,
Aachen, Germany, 1998. Shaker Verlag. Proceedings of a workshop
held at Bremen in 1996.
[321] Bettina Buth. PAMELA + PVS. In Rudolph Berghammer and
Yassine Lakhnech, editors, Tool Support for System Specification,
Development, and Verification, Advances in Computing Science,
pages 62-76, Malente, Germany, June 1998. Springer-Verlag.
Proceedings published in May 1999.
[322] Bettina Buth. PAMELA + PVS. In Michael Johnson, editor,
Algebraic Methodology and Software Technology, AMAST'97, volume
1349 of Lecture Notes in Computer Science, pages 560-562, Sydney,
Australia, December 1997. Springer-Verlag.
[323] James Corbett, Matthew Dwyer, John Hatcliff, Corina Pasareanu,
Robby, Shawn Laubach, and Hongjun Zheng. Bandera: Extracting
44
finite-state models from Java source code. In 22nd International
Conference on Software Engineering, pages 439-448, Limerick,
Ireland, June 2000. IEEE Computer Society.
[324] IEEE Washington Section. COMPASS '89 (Proceedings of the Fourth
Annual Conference on Computer Assurance), Gaithersburg, MD,
June 1989.
[325] IEEE Computer Society. Fault Tolerant Computing Symposium 25:
Highlights from 25 Years, Pasadena, CA, June 1995. IEEE Computer
Society.
[326] Hossein Saiedian (Ed.). An invitation to formal methods. IEEE
Computer, 29(4):16-30, April 1996. A "roundtable" of short articles
by several authors.
[327] Roger Shaw, editor. Safety and Reliability of Software Based Systems
(Twelfth Annual CSR Workshop), Bruges, Belgium, September 1995.
Springer.
[328] Seungjoon Park and David L. Dill. An executable specification,
analyzer and verifier for RMO (Relaxed Memory Order). In 7th
ACM Symposium on Parallel Algorithms and Architectures, pages
34-51, July 1995.
[329] Jeannette Wing and Jim Woodcock, editors. FM99: The World
Congress in Formal Methods, volume 1708 and 1709 of Lecture Notes
in Computer Science, Toulouse, France, September 1999.
Springer-Verlag. Pages 1-938 are in the first volume, 939-1872 in the
second.
45