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 a copyright of, I hereby give permission to quote freely any portion of the paper 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 a tarball of ACL2 script or tool 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.

Dissertation

S. Ray. Using Theorem Proving and Algorithmic Decision Procedures for Large-Scale System Verification, Department of Computer Sciences, The University of Texas at Austin, December 2005.

Book Chapters

S. Ray. Verifying Java Programs through a Formal JVM Model. To Appear in F. Columbus, editor, Java Software, 2009. Nova Publishers.

Journal Articles

M. Kaufmann, J S. Moore, S. Ray, and E. Reeber. Integrating External Deduction Tools with ACL2. To Appear in Journal of Applied Logic (Special Issue on ESCoR, Empirically Successful Computerized Reasoning). Elsevier. (This article superecedes the IWIL 2006 paper below.)

S. Ray, W. A. Hunt, Jr., J. Matthews, and J S. Moore. A Mechanical Analysis of Program Verification Strategies. Journal of Automated Reasoning, volume 40(4), May 2008, pages 245-269. Springer. (This paper significantly generalizes the results in 2003 Draft and FMCAD 2004 paper, and presents them in terms more accessible to the general audience.)

D. A. Greve, M. Kaufmann, P. Manolios, J S. Moore, S. Ray, J. L. Ruiz-Reina, R. Sumners, D. Vroon, and M. Wilding. Efficient Execution in an Automated Reasoning Environment. Journal of Functional Programming, volume 18(1), January 2008, pages 15-46. Cambridge University Press. (For a more detailed version of this work, see the 2006 Technical Report below.)

J. Bhadra, M. S. Abadir, L. Wang, and S. Ray. A Survey of Hybrid Technques for Functional Verification. IEEE Design & Test of Computers, volume 24(2), March-April 2007 (Special Issue on Advances in Functional Validation through Hybrid Techniques), pages 112-122. IEEE Computer Society.

S. Ray and R. Sumners. Combining Theorem Proving with Model Checking through Predicate Abstraction. IEEE Design & Test of Computers, volume 24(2), March-April 2007 (Special Issue on Advances in Functional Validation through Hybrid Techniques), pages 132-139. IEEE Computer Society. (This article provides extensions and a high-level presentation of the techniques described in the ACL2 2004 paper and the 2005 Technical Report below.)

Conference/Workshop Publications

W. A. Hunt, Jr., R. B. Krug, S. Ray, and W. D. Young. Mechanized Information Flow Analysis through Inductive Assertions. To Appear in A. Cimatti and R. B. Jones, editors, Proceedings of the 8th International Conference on Formal Methods in Computer-aided Design (FMCAD 2008), Portland, OR, November 2008. IEEE Computer Society.

S. Ray and J. Bhadra. Abstracting and Verifying Flash Memories. To Appear in J. Peloquin, editor, Proceedings of the 9th Non-Volatile Memory Technology Symposium (NVMTS 2008), Pacific Grove, CA, November 2008. IEEE Computer Society.

S. Ray and W. A. Hunt, Jr. Mechanized Certification of Secure Hardware Designs. In M. S. Abadir, L. Wang, and J. Bhadra, editors, Proceedings of the 8th International Workshop on Microprocessor Test and Verification, Common Challenges and Solutions (MTV 2007), Austin, TX, December 2007, pages 25-32. IEEE Computer Society.

S. Ray. A Generalized Solution for the While Challenge. Rump Session Presentation. In R. Gamboa, J. Sawada, and J. Cowles, editors, Proceedings of the 7th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2007), Austin, TX, November 2007, pages 83-84.

S. Ray and J. Bhadra. A Mechanized Refinement Framework for Analysis of Custom Memories. In J. Baumgartner and M. Sheeran, editors, Proceedings of the 7th International Conference on Formal Methods in Computer-aided Design (FMCAD 2007), Austin, TX, November 2007, pages 239-242. IEEE Computer Society.

M. Kaufmann, J S. Moore, S. Ray, and E. Reeber. Integrating External Deduction Tools with ACL2. In C. Benzmüller, B. Fischer, and G. Sutcliffe, editors, Proceedings of the 6th International Workshop on the Implementation of Logics (IWIL 2006), Phnom Penh, Cambodia, November 2006, volume 212 of CEUR Workshop Proceedings, pages 7-26. (This paper is superceded by the JAL article above.)

J. Matthews, J S. Moore, S. Ray, and D. Vroon. Verification Condition Generation via Theorem Proving. In M. Hermann and A. Voronkov, editors, Proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2006), Phnom Penh, Cambodia, November 2006, volume 4246 of LNCS, pages 362-376. Springer. (Some preliminary results of this paper are described in the 2005 draft below.)

S. Ray. Quantification in Tail-recursive Function Definitions. In P. Manolios and M. Wilding, editors, Proceedings of the 6th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2006), Seattle, WA, August 2006, volume 205 of ACM International Conference Proceeding Series, pages 95-98. ACM.

R. Sumners and S. Ray. Reducing Invariant Proofs to Finite Search via Rewriting. In M. Kaufmann and J S. Moore, editors, 5th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2004), Austin, TX, November 2004. (For follow-up extensions, see the 2005 Technical Report below. See also the 2007 D&T article above for further extensions and a high-level presentation.)

S. Ray. Attaching Efficient Executability to Partial Functions in ACL2. In M. Kaufmann and J S. Moore, editors, 5th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2004), Austin, TX, November 2004.

S. Ray and J S. Moore. Proof Styles in Operational Semantics. In A. J. Hu and A. K. Martin, editors, Proceedings of the 5th International Conference on Formal Methods in Computer-aided Design (FMCAD 2004), Austin, TX, November 2004, volume 3312 of LNCS, pages 67-81. Springer. (For a more detailed presentation, see the 2003 draft below. See also the 2008 JAR article above for significant generalizations of the results.)

S. Ray and W. A. Hunt, Jr. Deductive Verification of Pipelined Machines Using First-order Quantification. In R. Alur and D. A. Peled, editors, Proceedings of the 16th International Conference on Computer-aided Verification (CAV 2004), Boston, MA, July 2004, volume 3114 of LNCS, pages 31-43. Springer.

S. Ray, J. Matthews, and M. Tuttle. Certifying Compositional Model Checking Algorithms in ACL2. In W. A. Hunt, Jr., M. Kaufmann, and J S. Moore, editors, 4th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2003), Boulder, CO, July 2003.

S. Ray and R. Sumners. Verification of an In-place Quicksort in ACL2. In D. Borrione, M. Kaufmann, and J S. Moore, editors, Proceedings of the 3rd International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2002), Grenoble, France, April 2002, pages 204-212.

Submitted Papers

S. Ray. Verifying Java Programs through a Formal JVM Model. Submitted, September 2008.

S. Ray. Abstraction as a Practical Debugging Tool. Submitted, September 2008.

Technical Reports, Drafts, and Other Papers

S. Ray. Towards a Formalization of the X86 Instruction Set Architecture. Technical Report TR-08-15, Department of Computer Sciences, University of Texas at Austin, March 2008. 10 pages.

W. A. Hunt, Jr., M. Kaufmann, R. B. Krug, and S. Ray. Formalizing Routing Models in ACL2. Technical Report TR-08-11, Department of Computer Sciences, University of Texas at Austin, March 2008. 54 pages.

D. A. Greve, M. Kaufmann, P. Manolios, J S. Moore, S. Ray, J. L. Ruiz-Reina, R. Sumners, D. Vroon, and M. Wilding. Efficient Execution in an Automated Reasoning Environment. Technical Report TR-06-59, Department of Computer Sciences, University of Texas at Austin, November 2006. 53 pages. (This paper provides a more detailed presentation of the work described in the 2008 JFP article above.)

R. Sumners and S. Ray. Proving Invariants via Rewriting and Abstraction. Technical Report TR-05-35, Department of Computer Sciences, University of Texas at Austin, July 2005. 13 pages. (This paper extends the ACL2 2004 paper above. See also the 2007 D&T article above for further extensions and a high-level presentation of the techniques.)

J. Matthews, J S. Moore, S. Ray, and D. Vroon. A Symbolic Simulation Approach to Assertional Program Verification. Draft, January 2005. 13 pages. (The results of this paper are improved in the LPAR 2006 paper above.)

S. Ray and J S. Moore. Proof Styles in Operational Semantics. Draft, December 2003. 29 pages. (This paper is a more detailed version of the FMCAD 2004 paper above, and explains most of the proofs involved. See also the JAR article above for significant generalizations of the results.)

S. Ray. Using Theorem Proving with Algorithmic Techniques for Large-Scale System Verification. Ph.D. Oral Proposal, Department of Computer Sciences, University of Texas at Austin, November 2003. 33 pages.

R. D. Blumofe, C. G. Plaxton, and S. Ray. Verification of a Concurrent Deque Implementation. Technical Report TR-99-11, Department of Computer Sciences, University of Texas at Austin, June 1999. 20 pages.