From: boyer@cs.utexas.edu Date: Tue, 21 Oct 1997 10:54:25 -0500 (CDT) To: nqthm-users@cs.utexas.edu Subject: Second Edition of A Computational Logic Handbook Content-Type: text Content-Length: 2270 The second edition of the book "A Computational Logic Handbook" is now in print. Robert S. Boyer and J Strother Moore, A Computational Logic Handbook, Second Edition, Academic Press, 1997, ISBN 0121229556. 518+xxv pages. Be sure to mention "second edition". It could be hard to find it in book stores just yet, so we mention the Academic Press 800 number, 1-800-321-5068. $69.95. The second edition is the authoritative documentation for Nqthm-1992, the most recent edition of the Boyer-Moore prover, which may be obtained with sources and without fee at ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/index.html. In addition to a very large number of minor corrections and improvements to the first edition, here are some of the major differences of the second edition over the first describes new syntax, including COND, CASE, LET, LIST*, and backquote describes some "higher order" inference procedures, including "constrained functions" and "functional instantiation" documents more sophisticated control machinery for manipulating very large theories introduces a "secure" proof-checking environment describes thousands of pages of fascinating example input dealing with very difficult questions in formal methods and mathematics provides a formal parser for the syntax compares the proof complexity of many interesting checked examples includes much new tutorial help, especially for the many new features contains a thorough bibliography of interesting Nqthm applications Bob Boyer and J Moore P. S. There is a "new" release of Nqthm-1992 available at ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/index.html. However, this is actually only a "bureaucratic" update to make slightly easier the life of folks who wish to install Nqthm from scratch. This new release combines the Nqthm-1992 "release" of 1994 with the "examples" of 1995. In other words, if you already have a working Nqthm-1992 and the 1995 examples release, it's probably a waste of your time to do a reinstallation. (There is actually something new included: the ancient and crufty but operational Lisp code for our Fortran Verification Condition Generator, in directory examples/fortran-vcg.) From: boyer@cs.utexas.edu Date: Tue, 21 Oct 1997 10:54:25 -0500 (CDT) To: nqthm-users@cs.utexas.edu Subject: Second Edition of A Computational Logic Handbook Content-Type: text Content-Length: 2270 The second edition of the book "A Computational Logic Handbook" is now in print. Robert S. Boyer and J Strother Moore, A Computational Logic Handbook, Second Edition, Academic Press, 1997, ISBN 0121229556. 518+xxv pages. Be sure to mention "second edition". It could be hard to find it in book stores just yet, so we mention the Academic Press 800 number, 1-800-321-5068. $69.95. The second edition is the authoritative documentation for Nqthm-1992, the most recent edition of the Boyer-Moore prover, which may be obtained with sources and without fee at ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/index.html. In addition to a very large number of minor corrections and improvements to the first edition, here are some of the major differences of the second edition over the first describes new syntax, including COND, CASE, LET, LIST*, and backquote describes some "higher order" inference procedures, including "constrained functions" and "functional instantiation" documents more sophisticated control machinery for manipulating very large theories introduces a "secure" proof-checking environment describes thousands of pages of fascinating example input dealing with very difficult questions in formal methods and mathematics provides a formal parser for the syntax compares the proof complexity of many interesting checked examples includes much new tutorial help, especially for the many new features contains a thorough bibliography of interesting Nqthm applications Bob Boyer and J Moore P. S. There is a "new" release of Nqthm-1992 available at ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/index.html. However, this is actually only a "bureaucratic" update to make slightly easier the life of folks who wish to install Nqthm from scratch. This new release combines the Nqthm-1992 "release" of 1994 with the "examples" of 1995. In other words, if you already have a working Nqthm-1992 and the 1995 examples release, it's probably a waste of your time to do a reinstallation. (There is actually something new included: the ancient and crufty but operational Lisp code for our Fortran Verification Condition Generator, in directory examples/fortran-vcg.) From: hunt@cli.com (Warren A. Hunt Jr.) Date: Tue, 23 May 95 10:06:19 CDT To: clt@sail.stanford.edu Subject: FM9001 Announcement Dear Carolyn, Bob Boyer suggested that I convey the announcement of the public release of the FM9001 microprocessor: its specification, design, and correctness proof. We hope that you may find the results of this research to be valuable, and we look forward to any feedback you may have. Warren ++++++ The FM9001 Microprocessor: Its Formal Specification and Mechanical Correctness Proof Spring 1995 We are releasing the mechanically checked proof scripts for the FM9001 microprocessor. The FM9001 is a general-purpose 32-bit microprocessor which has been implemented as a CMOS ASIC. The proof being released rigorously connects the expression of the FM9001 as a netlist with the characterization of the FM9001 at the machine-code programmer's level. (The FM9001 is the foundation of the `CLI Stack', which also includes several verified compilers and applications all running on the FM9001. Other parts of the `CLI Stack' are separately released.) To obtain information about the FM9001 microprocessor and proof, please examine the URL http://www.cli.com/hardware/fm9001.html To obtain the FM9001 system, connect to Internet site ftp.cli.com by anonymous ftp, giving your email address as the password, `get' the file /pub/fm9001/README and follow the instructions therein. Or get the URL ftp://ftp.cli.com/pub/fm9001/README via your WWW browser. Bishop C. Brock and Warren A. Hunt, Jr. brock@cli.com hunt@cli.com