Note: .ps versions of the .pdf files linked to below are also available here.

Some Technical Reports of the Institute for Computing Science and Computer Applications, University of Texas at Austin, 1978-1987

We list below those ICS reports that are on-line here. The full list of reports is in the file full.text.

  • 60 Kaufmann. A User's Manual for an Interactive Enhancement to the Boyer-Moore Theorem Prover. Aug 87.

  • 59 Kaufmann, Young. Comparing Gypsy and the Boyer-Moore Logic for Specifying Secure Systems. May 87.

  • 57 Kim. On Automatically Generating and Using Examples in a Computational Logic System. Apr 87.

  • 54 Bevier, Hunt, and Young. Toward Verified Execution Environments. Feb 87.

  • 51 Cohen. Proving Gypsy Programs. May 86.

  • 48 Good, Akers, Smith. Report on Gypsy 2.05. Feb 86.

  • 46 Kim. EGS: A Transformational Approach to Automatic Example Generation. Jan 85.

  • 45 Shankar. A Mechanical Proof of the Church-Rosser Theorem. Jan 85.

  • 44 Boyer and Moore. Integrating Decision Procedures Into Heuristic Theorem Provers. Jan 85.

  • 43 Shankar. Towards Mechanical Metamathematics. Dec 84.

  • 42 Siebert and Good. General Message Flow Modulator. Mar 84.

  • 41 Good. Mechanical Proofs about Computer Programs. Mar 84.

  • 40 McHugh. Toward the Generation of Efficient Code from Verified Programs. Mar 84.

  • 39 Akers. A Gypsy-to-Ada Program Compiler. Dec 83.

  • 37 Boyer and Moore. A Mechanical Proof of the Turing Completeness of Pure Lisp. May 83.

  • 35 Boyer and Moore. Proof-Checking, Theorem Proving, and Program Verification. Jan 83.

  • 34 Good, Siebert, et al. Message Flow Modulator - Final Report. Dec 82.

  • 33 Boyer and Moore. Proof Checking the RSA Public Key Encryption Algorithm. Sep 82.

  • 32 Boyer and Moore. MJRTY - A Fast Majority Vote Algorithm. Feb 81.

  • 31 Good Reusable Problem Domain Theories. Sep 82.

  • 30 Good. The Proof of a Distributed System in Gypsy. Sep 82.

  • 29 Boyer, Moore, et al. The Use of a Formal Simulator to Verify a Simple Real Time Control Program. Jul 82.

  • 28 Boyer and Moore. A Mechanical Proof of the Unsolvability of the Halting Problem. Jul 82.

  • 27 DiVito. Verification of TCP-Like Data Transport Functions. Aug 82.

  • 26 DiVito. Verification of the Stenning Protocol. Aug 82.

  • 25 DiVito. Verification of Communications Protocols and Abstract Process Models. Aug 82.

  • 24 DiVito. Integrated Methods for Protocol Specification and Verification. Mar 82.

  • 23 Hunter. The First Generation Gypsy Compiler. Jun 81.

  • 22 DiVito. Transcripts for the Proof of the Alternating Bit Protocol. Jun 81.

  • 21 DiVito. A Mechanical Verification of the Alternating Bit Protocol. Jun 81.

  • 15 Good, et al. Principles of Proving Concurrent Programs in Gypsy. Jan 79.

  • 10 Good, Cohen, et al. Report on the Language Gypsy:Version 2.0. Sep 78.

    An effort is underway to put some of the oldest reports, which we now only have in paper form, on line. Inquiries on this topic may be sent to Don Good, dgatx@earthlink.net, 1904 Mistywood Dr., Austin, TX.

    Main page.