pvs-bib.html

[1] B. Elspas, M. Green, M. Moriconi, and R. Shostak. A JOVIAL verifier. Technical report, Computer Science Laboratory, SRI International, January 1979.
BibTeX entry
[2] Lawrence Robinson and Karl N. Levitt. Proof techniques for hierarchically structured programs. Communications of the ACM, 20(4):271-283, April 1976.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[8] J. M. Silverman. Reflections on the verification of the security of an operating system kernel. In Ninth ACM Symposium on Operating System Principles, pages 143-154, Bretton Woods, NH, October 1983. (ACM Operating Systems Review, Vol. 17, No. 5).
BibTeX entry
[9] Department of Defense. Department of Defense Trusted Computer System Evaluation Criteria, December 1985. DOD 5200.28-STD (supersedes CSC-STD-001-83).
BibTeX entry
[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].
BibTeX entry
[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].
BibTeX entry
[12] R. S. Boyer and J S. Moore. A Computational Logic. Academic Press, New York, NY, 1979.
BibTeX entry
[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.
BibTeX entry
[14] Robert E. Shostak. On the SUP-INF method for proving Presburger formulas. Journal of the ACM, 24(4):529-543, October 1977.
BibTeX entry
[15] Robert E. Shostak. An algorithm for reasoning about equality. Communications of the ACM, 21(7):583-585, July 1978.
BibTeX entry
[16] Robert E. Shostak. A practical decision procedure for arithmetic with function symbols. Journal of the ACM, 26(2):351-360, April 1979.
BibTeX entry
[17] Robert E. Shostak. Deciding linear inequalities by computing loop residues. Journal of the ACM, 28(4):769-779, October 1981.
BibTeX entry
[18] Robert E. Shostak. Deciding combinations of theories. Journal of the ACM, 31(1):1-12, January 1984.
BibTeX entry
[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].
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[22] NASA Conference Publication 2377. Peer Review of a Formal Verification/Design Proof Methodology, July 1983.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[30] Paul S. Miner. Verification of fault-tolerant clock synchronization systems. NASA Technical Paper 3349, NASA Langley Research Center, Hampton, VA, November 1993.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[36] Ricky W. Butler and Jon A. Sjogren. Formal design verification of digital circuitry. Reliability Engineering and System Safety, 32:67-93, 1991.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[39] S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M.K. Srivas. PVS: Combining specification, proof checking, and model checking. In 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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.''.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[56] John Rushby. Specification, proof checking, and model checking for protocols and distributed systems with PVS. Tutorial presented at 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.
BibTeX entry
[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.
BibTeX entry
[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/.
BibTeX entry
[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/.
BibTeX entry
[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.
BibTeX entry
[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].
BibTeX entry
[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ÚpaduŔs-╔ditions, Toulouse, France.
BibTeX entry
[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.
BibTeX entry
[64] John Rushby. Automated deduction and formal methods. In Rajeev Alur and Thomas A. Henzinger, editors, Computer-Aided Verification, CAV '96, volume 1102 of Lecture Notes in Computer Science, pages 169-183, New Brunswick, NJ, July/August 1996. Springer-Verlag.
BibTeX entry
[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.
BibTeX entry
[66] John Rushby. Calculating with requirements. In 3rd IEEE International Symposium on Requirements Engineering, pages 144-146, Annapolis, MD, January 1997. IEEE Computer Society.
BibTeX entry
[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.
BibTeX entry
[68] N. Shankar. Towards mechanical metamathematics. Journal of Automated Reasoning, 1(4):407-434, 1985.
BibTeX entry
[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.
BibTeX entry
[70] N. Shankar. Metamathematics, Machines, and G÷del's Proof. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, UK, 1994.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[73] John Rushby. Critical system properties: Survey and taxonomy. Reliability Engineering and System Safety, 43(2):189-219, 1994.
BibTeX entry
[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].
BibTeX entry
[75] Mandayam Srivas, Harald Rueß, 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.
BibTeX entry
[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.
BibTeX entry
[77] David Cyrluk, Harald Rueß, and Oliver M÷ller. 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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[80] Oliver M÷ller and Harald Rueß. 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.
BibTeX entry
[81] Ashish Tiwari, Leo Bachmair, and Harald Rueß. 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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[84] Sam Owre and Harald Rueß. 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.
BibTeX entry
[85] Friedrich von Henke, Stephan Pfab, Harald Rueß, 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.
BibTeX entry
[86] Friedrich von Henke, Stephan Pfab, Holger Pfeifer, and Harald Rueß. 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.
BibTeX entry
[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.
BibTeX entry
[88] Saddek Bensalem, Yassine Lakhnech, and Hassen Sa´di. 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.
BibTeX entry
[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 in Computer Science, pages 319-331, Vancouver, Canada, June 1998. Springer-Verlag.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[92] Susanne Graf and Hassen Sa´di. 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.
BibTeX entry
[93] Hassen Sa´di. 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.
BibTeX entry
[94] Hassen Sa´di. 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.
BibTeX entry
[95] Hassen Sa´di 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.
BibTeX entry
[96] Hassen Sa´di. 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/.
BibTeX entry
[97] Hassen Sa´di 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.
BibTeX entry
[98] Hassen Sa´di. 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.
BibTeX entry
[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Ó, Switzerland, March 2000. Springer-Verlag.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[102] Saddek Bensalem, Vijay Ganesh, Yassine Lakhnech, CÚsar Mu˝oz, Sam Owre, Harald Rueß, John Rushby, Vlad Rusu, Hassen Sa´di, 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/.
BibTeX entry
[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.
BibTeX entry
[104] John Rushby. Integrated formal verification: Using model checking with automated abstraction, invariant generation, and theorem 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.
BibTeX entry
[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.
BibTeX entry
[106] John Rushby. Disappearing formal methods. In High-Assurance Systems Engineering Symposium, pages 95-96, Albuquerque, NM, November 2000. Association for Computing Machinery.
BibTeX entry
[107] William D. Young. Comparing verification systems: Interactive Consistency in ACL2. IEEE Transactions on Software Engineering, 23(4):214-223, April 1997.
BibTeX entry
[108] Victor A. Carre˝o 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.
BibTeX entry
[109] Mike Gordon. Notes on PVS from a HOL perspective. Available at http://www.cl.cam.ac.uk/users/mjcg/PVS.html, August 1995.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[112] Christoph Kern and Mark R. Greenstreet. Formal verification in hardware design: A survey. ACM Transactions on Design Automation of Electronic Systems (TODAES), 4(2):123-193, April 1999.
BibTeX entry
[113] Heinrich Rust. A PVS specification of an invoicing system. In M. Allemand, C. AttiogbÚ, 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.
BibTeX entry
[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/.
BibTeX entry
[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/).
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[120] John Knight, Colleen DeJong, Matthew Gibble, and LuÝs 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/.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[129] Ulrich Hensel and Bart Jacobs. Coalgebraic theories of sequences in PVS. Journal of Logic and Computation, 9(4):463-500, 1999.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[134] Marieke Huisman. Java Program Verification in Higher-Order Logic with PVS and Isabelle. PhD thesis, University of Nijmegen, The Netherlands, 2001.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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].
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[142] John Rushby. Systematic formal verification for fault-tolerant time-triggered algorithms. IEEE Transactions on Software Engineering, 25(5):651-660, September/October 1999.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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/.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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 Engineering, ISSRE '95, pages 52-57, Toulouse, France, 1995. IEEE Computer Society.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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/.
BibTeX entry
[163] Victor Carre˝o and CÚsar Mu˝oz. 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.
BibTeX entry
[164] Victor Carre˝o and CÚsar Mu˝oz. Formal analysis of parallel landing scenarios. In 19th AIAA/IEEE Digital Avionics Systems Conference, Philadelphia, PA, October 2000.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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, Jerusalem, Israel, March-April 1998. IEEE Computer Society. Available at http://www.win.tue.nl/cs/tt/hooman/ECBS98.html.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[175] Harald Rueß and Jonathan Millen. Local secrecy for state-based models. In Formal Methods and Computer Security (FMCS), Chicago, IL, July 2000.
BibTeX entry
[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.
BibTeX entry
[177] RaphaŰl Couturier and Dominique MÚry. 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.
BibTeX entry
[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.
BibTeX entry
[179] Dmitri Chkliaev, Jozef Hooman, and Peter van der Stok. Serializability preserving extensions of concurrency control protocols. In D. Bjørner, 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.
BibTeX entry
[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.
BibTeX entry
[181] RaphaŰl 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/).
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[184] Klaus Havelund. Mechanical verification of a garbage collector. In JosÚ 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).
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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/.
BibTeX entry
[191] Andren Alborghetti, Angelo Gargantini, and Angelo Morzenti. Providing automated support to deductive analysis of time critical 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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[199] Bruno Dutertre and Victoria Stavridou. Formal analysis for realtime scheduling. In 19th AIAA/IEEE Digital Avionics Systems Conference, Philadelphia, PA, October 2000.
BibTeX entry
[200] Bruno Dutertre. Formal analysis of the priority ceiling protocol. In Real Time Systems Symposium, Orlando, FL, December 2000. IEEE Computer Society. To appear.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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Řbeck, Germany, September 1994. Springer-Verlag.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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 Notes in Computer Science, pages 315-333, Bamberg, Germany, May 1999. Springer-Verlag.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[211] Jens Ulrik Skakkebæk. A Verification Assistant for a Real-Time Logic. PhD thesis, Department of Computer Science, Technical University of Denmark, Lyngby, Denmark, November 1994.
BibTeX entry
[212] Jens U. Skakkebæk 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Řbeck, Germany, September 1994. Springer-Verlag.
BibTeX entry
[213] Pertti Kellomńki. 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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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Ú 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).
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[224] Pertti Kellomńki. 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.
BibTeX entry
[225] Pertti Kellomńki. 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.
BibTeX entry
[226] David Lesens and Hassen Sa´di. 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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[231] Lars KhŘne, 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.
BibTeX entry
[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.
BibTeX entry
[233] MichaŰl 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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[236] Michel LÚvy 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.
BibTeX entry
[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.
BibTeX entry
[238] Ralf Behnke, Rudolf Berghammer, and S÷nke 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.
BibTeX entry
[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.
BibTeX entry
[240] Axel Dold. Formal Software Development using Generic Development Steps. PhD thesis, Universitńt Ulm, Germany, 2000.
BibTeX entry
[241] N. Shankar. Computer-aided computing. In Bernhard M÷ller, editor, Mathematics of Program Construction '95, volume 947 of Lecture Notes in Computer Science, pages 50-66. Springer-Verlag, 1995.
BibTeX entry
[242] N. Shankar. Steps towards mechanizing program transformations using PVS. Science of Computer Programming, 26(1-3):33-57, 1996.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[246] Jens Knappmann. A PVS based tool for developing programs in the Refinement Calculus. Master's thesis, Institut fŘr Informatik und Praktische Mathematik der Christian-Albrechts-Universitńt zu Kiel, Kiel, Germany, October 1996.
BibTeX entry
[247] Karl-Heinz Buth. Automated code generator verification based on algebraic laws. Procos II Report Kiel KHB 5/1, Christian-Albrechts Universitńt zu Kiel, Kiel, Germany, September 1995. Available at ftp://ftp.informatik.uni-kiel.de/pub/kiel/procos/kiel-khb-5-1.ps.Z.
BibTeX entry
[248] A. Dold, F. W. von Henke, H. Pfeifer, and H. Rueß. 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.
BibTeX entry
[249] A. Dold, T. Gaul, V. Vialard, and W. Zimmermann. ASM-Based Mechanized Verification of Compiler Backends. In Uwe Glńsser 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.
BibTeX entry
[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/.
BibTeX entry
[251] Axel Dold and Vincent Vialard. Formal verification of a compiler back-end generic checker program. In D. Bjørner, 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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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, UK, November 1998. Available at http://www.dcs.warwick.ac.uk/pub/reports/rr/354.html.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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 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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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/.
BibTeX entry
[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.
BibTeX entry
[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/).
BibTeX entry
[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.
BibTeX entry
[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 (FMCAD '96), volume 1166 of Lecture Notes in Computer Science, pages 64-78, Palo Alto, CA, November 1996. Springer-Verlag.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[278] H. Rueß, 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.
BibTeX entry
[279] H. Rueß, N. Shankar, and M. K. Srivas. Modular verification of SRT division. Formal Methods in Systems Design, 14(1):45-73, January 1999.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[283] Mandayam K. Srivas and Steven P. Miller. Formal verification of the AAMP5 microprocessor. In Michael G. Hinchey and Jonathan P. Bowen, editors, Applications of Formal Methods, Prentice Hall International Series in Computer Science, chapter 7, pages 125-180. Prentice Hall, Hemel Hempstead, UK, 1995.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[292] Seungjoon Park. Computer Assisted Analysis of Multiprocessor Memory Systems. PhD thesis, Department of Electrical Engineering, Stanford University, June 1996.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[296] V. Rusu, L. du Bousquet, and T. JÚron. 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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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Ó, Switzerland, March 2000. Springer-Verlag.
BibTeX entry
[304] Jean Paul Bodeveix, Mamoun Filali, and CÚsar A. Mu˝oz. 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].
BibTeX entry
[305] CÚsar Mu˝oz 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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[308] John Rushby and Mandayam Srivas. Using PVS to prove some theorems of David Parnas. In Jeffrey J. Joyce and Carl-Johan H. 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.
BibTeX entry
[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.
BibTeX entry
[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/.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry
[323] James Corbett, Matthew Dwyer, John Hatcliff, Corina Pasareanu, Robby, Shawn Laubach, and Hongjun Zheng. Bandera: Extracting finite-state models from Java source code. In 22nd International Conference on Software Engineering, pages 439-448, Limerick, Ireland, June 2000. IEEE Computer Society.
BibTeX entry
[324] IEEE Washington Section. COMPASS '89 (Proceedings of the Fourth Annual Conference on Computer Assurance), Gaithersburg, MD, June 1989.
BibTeX entry
[325] IEEE Computer Society. Fault Tolerant Computing Symposium 25: Highlights from 25 Years, Pasadena, CA, June 1995. IEEE Computer Society.
BibTeX entry
[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.
BibTeX entry
[327] Roger Shaw, editor. Safety and Reliability of Software Based Systems (Twelfth Annual CSR Workshop), Bruges, Belgium, September 1995. Springer.
BibTeX entry
[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.
BibTeX entry
[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.
BibTeX entry

This file has been generated by bibtex2html 1.2