Mechanically Checked Proofs of Kernel Specifications, W. R. Bevier and J. F. Soegaard-Andersen, Proc. of the 3rd Workshop on Computer-Aided Verification, Aalborg, Denmark, July, 1991.
The Design and Proof of Correctness of a Fault-Tolerant Circuit, W. R. Bevier and W. D. Young, Proc. of the 2nd IFIP Working Conference on Dependable Computing for Critical Applications, February, 1991. Also appears as CLI Technical Report 57.
Operating System Correctness is a Mission Critical Requirement, W. R. Bevier, T. Taylor, Proc. 1989 Workshop on Operating Systems for Mission Critical Computing, September, 1989.
Primitive Recursive Program Transformation, R. S. Boyer, J S. Moore and R. E. Shostak. Proceedings of the Third Association for Computing Machinery Symposium on Principles of Programming Languages, Atlanta, 1976.
SELECT--A Formal System for Testing and Debugging Programs, R. S. Boyer, K. N. Levitt and B. Elspas. Proceedings of the International Conference on Reliable Software, IEEE Catalogue Number 75CHO940-7CSR, pp. 234-245, 1975.
R. S. Boyer, A Few Minor Remarks (on Metafunctions), Proceedings of the Workshop on Correctness and Metatheoretic Extensibility of Automated Reasoning Systems, INRIA Lorraine, Nancy, France, 1994, p. 22.
Metafunctions in Nqthm and Acl2, R. S. Boyer, Matt Kaufmann and J Moore, Proceedings of the Workshop on Correctness and Metatheoretic Extensibility of Automated Reasoning Systems, INRIA Lorraine, Nancy, France, 1994, pp. 16-18.
R. S. Boyer, A Mechanically Proof-Checked Encyclopedia of Mathematics: Should We Build One? Can We?, Proceedings of the 12th Annual Conference on Automated Deduction, Springer-Verlag Lecture Notes in Computer Science, Number 814, 1994, p. 237.
Principles of Proving Concurrent Programs in Gypsy, R. M. Cohen, D. I. Good and J. Keeton-Williams, in Proceedings of the Sixth ACM Symposium on Principles of Programming Languages, January, 1979.
A Report on the Development of Gypsy, R. M. Cohen, D. I. Good and L. W. Hunter, in Proceedings of the National ACM Conference 1978, December, 1978.
R. M. Cohen, Formal Specifications for Real-Time Systems, in Seventh Texas Conference on Computing Systems, October, 1978.
Verifiable Communications Processing in Gypsy, R. M. Cohen, D. I. Good, in Proceedings IEEE CompCon Fall'78, September, 1978.
Gypsy: A Language for Specification and Implementation of Verifiable Programs. R. M. Cohen, Allen Ambler, D. I. Good, James Browne, Wilhelm Burger, Charles Hoch, and Robert Wells, in Proceedings of an ACM Conference on Language Design for Reliable Software, March, 1977.
D. I. Good, W. D. Young, Program Verification and Embedded Aerospace Software, In Proceedings of the AIAA Computers in Aerospace Conference III, October, 1981.
D. I. Good, W. D. Young, Generics and Verification in Ada, In Proceedings of the ACM Symposium on the Ada Programming Language, November, 1980.
D. I. Good, A.R. Tripathi, W.D.Young, A Preliminary Evaluation of Verifiability in Ada, In Proceedings of the ACM Annual Conference, October, 1980.
D. I. Good, W. D. Young, A.R. Tripathi, James C. Browne, Evaluation of Verifiability of HAL/S, In Proceedings of AIAA Computers in Aerospace Conference II, October, 1979.
D. I. Good, R.M. Cohen, J. Keeton-Williams, Principles of Proving Concurrent Programs in Gypsy, SIGACT Conference, January, 1979.
D. I. Good, J.C. Browne, R.E. Wells, M.K. Smith, An Integrated Methodology or Formally Verified Communications Processing Systems, National Telecommunications Conference, December, 1978.
D. I. Good, R.M. Cohen, Verifiable Communications Processing in Gypsy, IEEE-Compcon '78 Seventeenth Computer Society Conference, Fall, 1978.
D. I. Good, R.M. Cohen, L.W. Hunter, A Report on the Development of Gypsy, 1978 National ACM Conference Proceedings (SIGPLAN)
D. I. Good, A.L. Ambler, J.C. Browne, W. Burger, R. Cohen, C. Hoch, R. Wells, Gypsy: A Language for Specification and Implementation of Verifiable Programs, In Proceedings of ACM Conference on Language Design for Reliable Software, March, 1977.
D. I. Good, Proving Programs, In Proceedings of 1976 ACM Conference, October, 1976.
D. I. Good, Provable Programming, In Proceedings of 1975 International Conference on Reliable Software, Los Angeles, April, 1975.
D. I. Good, R.L. London, W.W. Bledsoe, An Interactive Program Verification System, In Proceedings of 1975 International Conference on Reliable Software, Los Angeles, April, 1975
D. I. Good, Provable Programs and Processors, In Proceedings of 1974 National Computer Conference, AFIPS Press, 1974.
D. I. Good, E.M. Greenwalt, The MIX Computer as an Educational Tool, In Proceedings of the ACM National Conference, August, 1972.
Developing Correct Software, In Proceedings of First Texas Symposium on Computer Systems, June, 1972.
D. I. Good, Beyond Factorial, National Computer Conference panel discussion, September, 1978.
Maintaining Abstractions with Verification, W. H. Hunt, W. D. Young, COM\-PASS 1990 Proceedings, IEEE, 1990.
The Formalization of a Simple HDL, W. H. Hunt, Bishop C. Brock, Proceedings of the IFIP TC10/WG10.2/WG10.5 Workshop on Applied Formal Methods for Correct VLSI Design, Elsevier Science Publishers, 1989.
Toward Verified Execution Environments, W. H. Hunt, William R. Bevier and W. D. Young, Proceedings of the 1987 IEEE Symposium.
W. H. Hunt, The Mechanical Verification of a Microprocessor, in International Working Conference from H.D.L. Descriptions to Guaranteed Correct Circuit Designs, North Holland, September 1986.
Design Goals for ACL2 (M. Kaufmann, J Strother Moore), in Proceedings of Third International School and Symposium on Formal Techniques in Real Time and Fault Tolerant Systems, Kiel, Germany (1994), pp. 92-117. Published by Christian-Albrechts-Universitat.
The Role of Automated Reasoning in Integrated System Verification Environments (M. Kaufmann, Donald I. Good and J Moore), in: Proceedings of TTCP XTP-1 Workshop on Effective Use of Automated Reasoning Technology in System Development, Naval Research Laboratory, Washington DC, April 6-7, 1992.
Should We Begin a Standardization Process for Interface Logics? (M. Kaufmann, J Moore), Proceedings of TTCP XTP-1 Workshop on Effective Use of Automated Reasoning Technology in System Development, Naval Research Laboratory, Washington DC, April 6-7, 1992.
M. Kaufmann, An Informal Discussion of Issues in Mechanically-assisted Reasoning, in: Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications.
The Boyer-Moore Prover and Nuprl: An Experimental Comparison (M. Kaufmann, David Basin). In: Proceedings of the First Workshop on Logical Frameworks, Antibes, France, May 1990.
M. Kaufmann, Demo of the Boyer-Moore Theorem Prover and some of its extensions. In: Proceedings of the First Workshop on Logical Frameworks (informal proceedings for Esprit Basic Research Action workshop), Antibes, France, May 1990.
Comparing Specification Paradigms for Secure Systems: Gypsy and the Boyer-Moore Logic (M. Kaufmann, William Young), in: Proceedings of the 10th National Computer Security Conference (1987).
A Prototype Theorem-Prover for a Higher-Order Functional Language (M. Kaufmann, R. Boyer). In Proceedings of VERkshop III (Verification Workshop III), Watsonville, CA, February 1985.
Primitive Recursive Program Transformation, J S. Moore, R.S. Boyer and R.E. Shostak. Proceedings of the Third ACM Symposium on Principles of Programming Languages, Association for Computing Machinery, Atlanta, 1976.
J S. Moore, A Guided Tour Through a Working Theorem Prover. Proceedings of the Fourth Work shop on Artificial Intelligence, Institut fur Informatik, Universitat Bonn, pp. 89-97, 1979.
A Lemma Driven Automatic Theorem Prover for Recursive Function Theory, J S. Moore, R.S. Boyer. Proceedings of the 5th International Joint Conference on Artificial Intelligence, pp. 511-519, 1977.
Good, D., Browne, J. C., Wells, R. C., and Smith, M. K., An integrated methodology for formally verified communications processing systems, National Telecommunications Conference, December, 1978.
Smith, M.K., Procedural automata in the clown's world, Proceedings of the Fourth Texas Conference on Computing Systems, November 1975.
William R. Bevier and W. D. Young. A State-Based Approach to Noninterference, Proceedings of the Computer Security Foundations Workshop VII, IEEE Computer Society Press, pp. 11--21, June, 1994. Also to appear in Journal of Computer Security.
Miren Carranza and W. D. Young. Verifying a Fuzzy Controller, Proceedings of the Second International Workshop on Industrial Fuzzy Control and Intelligent Systems, Texas A&M University, December, 1992, pp. 194--203. Also appears as CLI technical report 82, September, 1992.
Bishop C. Brock, Warren A. Hunt, Jr., and W. D. Young. Introduction to a Formally Defined Hardware Description Language, in Proceedings of the International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, North-Holland: Amsterdam, 1992, pp. 3--36.
W. D. Young, Formal Methods versus Software Engineering: Is There a Conflict? Proceedings of the Fourth Testing, Analysis, and Verification Symposium, Victoria, British Columbia, October, 1991, pp. 188-189.
Maintaining Abstractions with Verification, W. D. Young, Warren A. Hunt, Jr., Proceedings of the Fifth Annual Conference on Computer Assurance, June 1990, pp. 117-125.
W. D. Young, Gypsy and the GVE, invited presentation at the International Workshop on Formal Methods in Software Development, Napa, California, May, 1990.
W. D. Young, Verified Program Support Environments, Proceedings of the International Workshop on Formal Methods in Software Development, Napa, California, May, 1990.
W. D. Young, Verified Compilation in Micro-Gypsy, Proceedings of the Software Testing, Analysis and Verification Symposium, Key West Florida, December, 1989, pp. 20-26.
Comparing Specification Paradigms: Gypsy and Z, Proceedings of the 12th National Computer Security Conference, Baltimore, MA, 1989, pp. 83-97.
W. D. Young, Toward Foundations of Security, presented at the Computer Security Foundations Workshop II, Franconia, N.H., June, 1989.
Comparing Specification Paradigms for Secure Systems: Gypsy and the Boyer-Moore Logic, W. D. Young, Matthew J. Kaufmann, Proceedings of the 10th National Computer Security Conference, 1987. Also available from Computational Logic as ICSCA technical report 59.
Coding for a Believable Specification to Implementation Mapping, W. D. Young, John McHugh, Proc. IEEE Symposium on Security and Privacy, April, 1987.
A Verified Labeler for the Secure Ada Target, W. D. Young, P.A. Telega, W.E. Boebert and R.Y. Kain, Proceedings of the 9th National Computer Security Conference, September, 1986.
Secure Ada Target: Issues, System Design, and Verification, W. D. Young, W.E. Boebert, R.Y. Kain and S.A. Hansohn, Proc. IEEE Symposium on Security and Privacy, March, 1985.
Program Verification and Embedded Aerospace Software, W. D. Young, D.I. Good, Proceedings of the AIAA Computers in Aerospace Conference III, October, 1981, pp. 246-250.
Generics and Verification in ADA, W. D. Young, D.I. Good, Proceedings of the ACM Symposium on the ADA Programming Language, November, 1980, pp. 123-127. Also available from Computational Logic as ICSCA technical report 19.
A Preliminary Evaluation of Verifiability in ADA, W. D. Young, A.R. Tripathi, D.I. Good, Proceedings of the ACM National Conference, October, 1980, pp. 218-224.
Evaluation of Verifiability in HAL/S, W. D. Young, A.R. Tripathi, D.I. Good, J.C. Browne, Proceedings of the AIAA Computers in Aerospace Conference II, October, 1979, pp. 359-366. Also available from Computational Logic as ICSCA technical report 18.
http://dirleton.csres.utexas.edu/staff/publications/conference.html