Publications


Note and Disclaimer

For most of the papers listed here, there is a link which contains the abstract, and possibly one or more of (a) a preprint of the paper in postscript and/or pdf format, (b) slides for the presentations relevant to the paper (for conference/workshop papers), (c) a BibTex entry (for peer-reviewed works), and (d) supporting materials (wherever applicable). Most supporting materials are proof scripts or tools (described in the paper) formalized or implemented with the ACL2 theorem prover. Note that many of the papers accessible here are authors' preprints and not the authoritative, published versions. Some of the papers might be copyrighted by the corresponding publishers, and you should look at the relevant copyright notices to figure out how to make legal use of the preprints. For the papers that I hold the copyright of, I hereby give permission to quote freely any portion of the papers for any purpose, provided none of the text is modified and the quotation is properly delineated and credited to the original authors. I also give permission to make legal use of the supporting materials (software or proof scripts) that you can obtain from this site, for any purpose with or without modification, provided proper attribution is given to the authors of the original materials and as long as such use does not violate other relevant copyrights (for instance obligations derived from the ACL2 license for materials distributed with ACL2). Of course I offer no warranty for the use of the materials, whether express or implied; use them at your risk. If you get an ACL2 script from my Web page, then it was certified with the version of ACL2 which was current as of the time of the writing of the associated paper. I try to keep up with the ACL2 releases in updating these scripts so that they work with the current version of ACL2, but I might sometimes falter. If you have trouble using something, please let me know. In case a script or tool is distributed with ACL2, either as a distributed book or as supporting materials for the ACL2 workshop, the corresponding page will sometimes point to the distributed version.


Books

Edited Volumes

Dissertation

Journal Articles

Publications in Conferences/Symposia

Publications in Peer-reviewed Workshops

Technical Reports, Drafts, and Miscellaneous Writings