| [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 |