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