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.