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

S. Ray. Scalable Techniques for Formal Verification. Accepted for Publication, 2008. Springer.

Edited Volumes

S. Ray and D. Russinoff, editors, Proceedings of the 8th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2009), May 2009.

Dissertation

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

Journal Articles

M. Kaufmann, J S. Moore, S. Ray, and E. Reeber. Integrating External Deduction Tools with ACL2. Journal of Applied Logic, volume 7(1), March 2009 (Special Issue on ESCoR, Empirically Successful Computerized Reasoning), pages 3-25. 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.)

Publications in Conferences/Symposia

S. Ray and J. Bhadra. Modeling and Verification of Industrial Flash Memories. To Appear in P. Chatterjee and K. Gadepally, editors, Proceedings of the 11th International Symposium on Quality Electronic Design (ISQED 2010), San Jose, CA, March 2010. IEEE.

K. Hao, F. Xie, S. Ray, and J. Yang. Optimizing Equivalence Checking for Behavioral Synthesis. To Appear in Design, Automation & Test in Europe (DATE 2010), Dresden, Germany, March 2010. IEEE Computer Society.

S. Ray and W. A. Hunt, Jr. Connecting Pre-silicon and Post-silicon Verification. In A. Biere and C. Pixley, editors, Proceedings of the 9th International Conference on Formal Methods in Computer-aided Design (FMCAD 2009), Austin, TX, November 2009, pages 160-163. IEEE Computer Society.

S. Ray, K. Hao, Y. Chen, F. Xie, and J. Yang. Formal Verification for High-Assurance Behavioral Synthesis. In Z. Liu and A. P. Ravn, editors, Proceedings of the 7th International Symposium on Automated Technology for Verification and Analysis (ATVA 2009), Macao SAR, China, October 2009, volume 5799 of LNCS, pages 337-351. Springer.

J. L. Ruiz-Reina, D. A. Greve, M. Kaufmann, P. Manolios, J S. Moore, S. Ray, R. Sumners, D. Vroon, and M. Wilding. Efficient Execution in an Automated Reasoning Environment. In G. Moreno and P. Lucio, editors, Proceedings of the 9th Spanish Conference on Programming and Computer Languages (PROLE 2009), San Sebastian, Spain, September 2009. (This is a presentation of the JFP 2008 paper for the Programming Language research community in Spain.)

W. A. Hunt, Jr., R. B. Krug, S. Ray, and W. D. Young. Mechanized Information Flow Analysis through Inductive Assertions. 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, pages 227-230. IEEE Computer Society.

S. Ray and J. Bhadra. Abstracting and Verifying Flash Memories. In K. Campbell, editor, Proceedings of the 9th Non-Volatile Memory Technology Symposium (NVMTS 2008), Pacific Grove, CA, November 2008, pages 100-104. IEEE.

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.

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 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.

Publications in Peer-reviewed Workshops

S. Ray. Abstraction as a Practical Debugging Tool. In M. S. Abadir, L. Wang, and J. Bhadra, editors, Proceedings of the 9th International Workshop on Microprocessor Test and Verification, Common Challenges and Solutions (MTV 2008), Austin, TX, December 2008, pages 45-48. 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.

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.)

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. (An error later identified in this paper has been corrected in the 2008 Technical Report below.)

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, 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.

Book Chapters

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

Submitted Papers

M. J. C. Gordon, M. Kaufmann, and S. Ray. The Right Tools for the Job: Correctness of Cone of Influence Reduction Proved Using ACL2 and HOL4. Submitted, September 2009.

Technical Reports, Drafts, and Miscellaneous Writings

S. Ray. ACL2 2009: Eighth International Workshop on the ACL2 Theorem Prover and Its Applications. News Report in The Reasoner, volume 3(5), June 2009, page 11.

S. Ray, Y. Chen, F. Xie, and J. Yang. Combining Theorem Proving and Model Checking for Certification of Behavioral Synthesis Flows. Technical Report TR-08-48, Department of Computer Sciences, University of Texas at Austin, December 2008. 8 pages.

S. Ray. A Precise Characterization of Extended Tail-recursive Definitions. Technical Report TR-08-47, Department of Computer Sciences, University of Texas at Austin, November 2008. (This paper corrects an error in the ACL2 2006 paper above.)

S. Ray. A Beginner's Guide to Reasoning about Quantification in ACL2. Incorporated in the ACL2 User's Manual, August 2008.

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.