List of Technical Reports [In Reverse Chronological Order] TR# Date Author Title 60 Aug 87 Kaufmann A User's Manual for an Interactive Enhancement to the Boyer-Moore Theorem Prover. 59 May 87 Kaufmann/Young Comparing Gypsy and the Boyer-Moore Logic for Specifying Secure Systems 58 Apr 87 Shankar Proof-Checking Metamathematics 57 Apr 87 Kim On Automatically Generating and Using Examples in a Computational Logic System 56 Apr 87 Kim Measure Guessing: On Experiment with Hypothesis Generation from Examples 55 Feb 87 Boyer/Moore User's Manual 54 Feb 87 Bevier, Hunt, Toward Verified Execution and Young Environments 53 Dec 86 Chou Methods and Examples in Mechanical Geometry Theorem Proving 52 Nov 86 Boyer/Moore The Addition of Bound Quantifiers and Partial Functions to the Boyer-Moore Logic and Theorem Prover 51 May 86 Cohen Proving Gypsy Programs 50 Jul 86 Chou Proving Geometry Theorems Using Wu's Method 49 Dec 85 Chou Proving and Discovering Geometry Theorems Using Wu's Method 48 Feb 86 Good/Akers Smith Report on Gypsy 2.05 47 Dec 85 Hunt FM8501: A Verified Microprocessor 46 Jan 85 Kim EGS: A Transformational Approach to Automatic Example Generation 45 Jan 85 Shankar A Mechanical Proof of the Church-Rosser Theorem 44 Jan 85 Boyer&Moore Integrating Decision Procedures Into Heuristic Theorem Provers 43 Dec 84 Shankar Towards Mechanical Metamathematics 42 Mar 84 Siebert General Message Flow Modulator 41 Mar 84 Good Mechanical Proofs about Computer Programs 40 Mar 84 McHugh Toward the Generation of Efficient Code from Verified Programs 39 Dec 83 Akers A Gypsy-to-Ada Program Compiler 38 Jul 83 Russinoff An Experiment with the Boyer-Moore Program Verification System: A Proof of Wilson's Theorem 37 May 83 Boyer&Moore A Mechanical Proof of the Turing Completeness of Pure Lisp 36 May 83 Boyer&Moore A Fully Automatic Proof of the Correctness of an Ordered Tree Insertion Function 35 Jan 83 Boyer&Moore Proof-Checking, Theorem Proving, and Program Verification 34 Dec 82 Good,Siebert.. Message Flow Modulator - Final Report 33 Sep 82 Boyer&Moore Proof Checking the RSA Public Key Encryption Algorithm 32 Feb 81 Boyer&Moore MJRTY - A Fast Majority Vote Algorithm 31 Sep 82 Good Reusable Problem Domain Theories 30 Sep 82 Good The Proof of a Distributed System in Gypsy 29 Jul 82 Boyer, Moore.. The Use of a Formal Simulator to Verify a Simple Real Time Control Program 28 Jul 82 Boyer&Moore A Mechanical Proof of the Unsolvability of the Halting Problem 27 Aug 82 DiVito Verification of TCP-Like Data Transport Functions 26 Aug 82 DiVito Verification of the Stenning Protocol 25 Aug 82 DiVito Verification of Communications Protocols and Abstract Process Models 24 Mar 82 DiVito Integrated Methods for Protocol Specification and Verification 23 Jun 81 Hunter The First Generation Gypsy Compiler 22 Jun 81 DiVito Transcripts for the Proof of the Alternating Bit Protocol 21 Jun 81 DiVito A Mechanical Verification of the Alternating Bit Protocol 20 Aug 80 LSmith Compiling from the Gypsy Verification Environment 19 Dec 80 Young&Good Generics and Verification in Ada 18 Nov 80 Tripathi.. A Preliminary Evaluation of Verifiability in Ada 17 Dec 79 Young.. Evaluation of Verifiability in HAL/S 16 Jul 79 Hare A Structure Editor for the Gypsy Verification Environment 15 Jan 79 Good.. Principles of Proving Concurrent Programs in Gypsy 14 Oct 78 Cohen Formal Specifications for Real-time Systems 13 Oct 78 Good.. A Report on the Development of Gypsy 12 Aug 78 Hoch Hardware Support for Modern Software Concepts 11 Jun 78 Good&Cohen Verifiable Communications Processing in Gypsy 10 Sep 78 Good,Cohen.. Report on the Language Gypsy:Version 2.0 9 Dec 77 Moriconi A System of Incrementally Designing & Verifying Programs 8 Oct 77 Horn Specifications for a Secure Computer Communications Network 7 May 77 Good Constructing Verified and Reliable Communications Processing Systems 6 Jan 77 Good Constructing Verifiable Reliable and Secure Communications Processing Systems 5 Aug 76 Szygenda.. A Methodology for Fail-Secure Minicomputers 4 Dec 76 Wells The Specification and Implementation of a Verifiable Communications System 3 Dec 76 Ambler.. A Study of Protection in Programming Languages 2 Jul 76 Ambler.. Gypsy: A Language for Specification & Implementation of Verifiable Programs 1 Aug 76 Ambler.. Report on the Language Gypsy: Version 1.0