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 and J. Bhadra. Semiconductor Memories: Design, Modeling, Abstraction, and Verification. Accepted for Publication, 2010. Springer

S. Ray. Scalable Techniques for Formal Verification, 2010. ISBN 978-4419-5997-3. 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, published as part of ACM International Conference Proceeding Series, ISBN 9781-60558-742-4, 2009. ACM.

Dissertation

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

Journal Articles

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. Journal of Automated Reasoning, volume 47(1), June 2011, pages 1-16. Springer. (This paper eliminates some of the proof complexities discussed in the ACL2 2003 paper below.)

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, J. Bhadra, T. Portlock, and R. Syzdek. Modeling and Verification of Industrial Flash Memories. In P. Chatterjee and K. Gadepally, editors, Proceedings of the 11th International Symposium on Quality Electronic Design (ISQED 2010), San Jose, CA, March 2010, pages 705-712. IEEE. (This paper provides a uniform exposition of the techniques presented in the FMCAD 2007 paper and the NVMTS 2008 paper, and demonstrates their application on industrial designs.)

K. Hao, F. Xie, S. Ray, and J. Yang. Optimizing Equivalence Checking for Behavioral Synthesis. In Design, Automation & Test in Europe (DATE 2010), Dresden, Germany, March 2010. IEEE. (This paper presents several optimizations to scale up the framework presented in the ATVA 2009 paper to large-scale synthesized RTL designs.)

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. (See also the DATE 2010 paper for several optimizations to scale up the techniques discussed in this paper to practical designs.)

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. (This paper and the FMCAD 2007 paper are superceded by the ISQED 2010 paper above.)

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. (This paper and the NVMTS 2008 paper are superceded by the ISQED 2010 paper 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 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

O. Olivo, S. Ray, J. Bhadra, and V. Vedula. A Unified Formal Framework for Analyzing Functional and Speed-path Properties. To Appear in M. S. Abadir, L. Wang, and J. Bhadra, editors, Proceedings of the 12th International Workshop on Microprocessor Test and Verification, Common Challenges and Solutions (MTV 2011), Austin, TX, December 2011.

S. Ray and R. Sumners. A Theorem Proving Approach for Verification of Reactive Concurrent Programs. In S. Burckhardt, S. Chaudhury, A. Farzan, G. Gopalakrishnan, S. Siegel, and H. Veith, editors, 4th International Workshop on Exploiting Concurrency Efficiently and Correctly (EC² 2011), Salt Lake City, UT, USA, July 2011.

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 2009 JAL article.)

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

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. (Some of the proof complexities discussed here were later eliminated in the 2010 JAR article. Also, the connection to external tools advocated here subsequently led the research discussed in the IWIL 2006 paper and the 2009 JAL article.)

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.

Technical Reports, Drafts, and Miscellaneous Writings

S. Goel and S. Ray. A Beginner's Guide to Developing and Polishing ACL2 Proofs. Incorporated in the ACL2 User's Manual, June 2011.

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 Science, 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 Science, 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 Science, 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 Science, 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 Science, 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 Science, 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 Science, 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 Science, University of Texas at Austin, June 1999. 20 pages.