Papers available from this Web page may be covered by copyright. We offer them here in the interest of free distribution and to facilitate advancement of knowledge, but not to provide any commercial advantage. Please feel free to browse them in that spirit. To copy, to republish, to post on servers, or to redistribute to lists requires prior specific permission from the respective copyright owners.

Books

• S. Ray and M. R. Kabir, Virutal Prototyping for Distributed IoT applications, 2023 (To Appear). Springer.
• S. Ray, A. Basak, and S. Bhunia, Security Policy in System-on-Chip Designs: Specification, Implementation and Verification, 2018. ISBN 978-3-319-93464-8. Springer.
• S. Bhunia, S. Ray and S. Sur-Kolay editors, Fundamentals of IP and SoC Security: Design, Verification, and Debug, 2017. ISBN 978-3-319-50055-3. Springer.
• S. Ray, Scalable Techniques for Formal Verification, 2010. ISBN 978-4419-5997-3. Springer.

Edited Conference Proceedings

• B. Jobstmann and S. Ray editors, Proceedings of the 13th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2013), ISBN 978-0-9835678-3-7, October 2013.
• S. Ray and D. Russinoff editors, Proceedings of the 8th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2009), published as part of ACM International Conference Proceeding Series, ISBN 9781-60558-742-4, May 2009. ACM.

Dissertations

• 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

• S. S. Miftah, K. Raj, X. Meng, S. Ray, and K. Basu. System-on-Chip Information Flow Validation under Asynchronous Resets. To Appear In IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. IEEE.
• X. Chen, D. Halder, K. M. Islam, and S. Ray. Guarding Deep Learning Systems with Boosted Evasion Attack Detection and Model Update. To Appear In IEEE Internet of Things Journal. IEEE.
• J. Yang, Z. Yang, J. Casas, and S. Ray. Correct-by-Construction Design of Custom Accelerator Microarchitectures. IEEE Transactions on Computers volume 73(1), January 2024, pages 278–291.IEEE.
• D. Halder, M. Merugu, and S. Ray. ObNoCs: Protecting Network-on-Chip Fabrics Against Reverse-Engineering Attacks. ACM Transactions on Embedded Computing Systems volume 22(5), September 2023, pages 112:1-112:21. ACM.
• M. R. Kabir, B. B. Yedla Ravi, and S. Ray. A Virtual Prototyping Platform for Exploration of Vehicular Electronics. To Appear In IEEE Internet of Things Journal. IEEE.
• P. SLPSK, S. Ray, and S. Bhunia. TREEHOUSE: A Secure Asset Management Infrastructure for Protecting 3DIC Designs. To Appear In IEEE Transactions on Computers. IEEE.
• M. R. Kabir and S. Ray. Virtual Prototyping for Modern Internet-of-Things Applications: A Survey. IEEE Access volume 11, 2023, pages 31384-31398. IEEE.
• X. Chen, M. Merugu, J. Zhang, and S. Ray. AroMa: Evaluating Deep Learning Systems for Stealthy Integrity Attacks on Multi-tenant Accelerators. ACM Journal on Emerging Technologies in Computing Systems volume 19(2), April 2023, pages 1-17. ACM.
• X. Meng, K. Raj, S. Ray, and K. Basu. SeVNoC: Security Validation of System-on-Chip Designs with NoC Fabrics. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems volume 42(2), February 2023, pages 672-682. IEEE.
• J. Zhang, X. Chen, and S. Ray. AINNS: All-Inclusive Neural Network Scheduling via Accelerator Formalization. IEEE Transactions on Computers volume 72(2), February 2023, pages 559-571. IEEE.
• R. Owoputi and S. Ray. Security of Multi-Agent Cyber-Physical Systems: A Survey. IEEE Access volume 10, 2022, pages 121465-121479. IEEE.
• X. Chen, J. Zhang, and S. Ray. Dandelion: Boosting DNN Usability under Dataset Scarcity. IEEE Transactions on Computers volume 71(10), October 2022, pages 2487–2498. IEEE.
• S. Boddupalli, A. S. Rao, and S. Ray. Resilient Cooperative Adaptive Cruise Control for Autonomous Vehicles Using Machine Learning. IEEE Transactions on Intelligent Transportation systems volume 23(9), September 2022, pages 15655–15672. IEEE.
• J. Zhang, X. Chen, and S. Ray. GCONV Chain: Optimizing the Whole-life Cost in End-to-end CNN Acceleration. IEEE Transactions on Computers volume 71(9), September 2022, pages 2300–2312. IEEE.
• P. Chakraborty, J. Cruz, C. Posada, S. Ray, and S. Bhunia. HASTE: Software Security Analysis for Timing Attacks on Clear Hardware Assumption. IEEE Embedded Systems Letters volume 14(2), June 2022, pages 71-74. IEEE.
• A. P. Deb Nath, K. Raj, S. Bhunia, and S. Ray. SoCCom: Automated Synthesis of System-on-Chip Architectures. IEEE Transactions on VLSI systems volume 30(4), April 2022, pages 449–462. IEEE
• A. P. Deb nath, S. Boddupalli, S. Bhunia, and S. Ray. Resilient System-on-Chip Designs with NoC Fabrics. IEEE Transactions on Information Forensics and Security volume 15(1), March 2020, pages 2808-2823. IEEE.
• A. B. Lopez, A. V. Malawade, M. A. Al Faruque, S. Boddupalli, and S. Ray. Security of Emergent Automotive Systems: A Tutorial Introduction and Perspectives on Practice. IEEE Design & Test volume 36(6), December 2019, pages 10-38. IEEE.
• H. Nejatollahi, N. Dutt, S. Ray, F. Regazzoni, I. Banerjee, and R. Cammarota. Post-quantum Lattice-based Cryptography Implementations: A Survey. ACM Computing Surveys volume 51(6), pages 129:1–129:41. ACM.
• K. Chen, S. Zhang, Z. Li, Y. Zhang, Q. Deng, S. Ray, and Y. Jin. Internet-of-Things Security and Vulnerabilities: Taxonomy, Challenges, and Practice. Journal of Hardware and Systems Security volume 2(2), June 2018, pages 97-110. Springer.
• S. Ray, E. Peeters, M. Tehranipoor, and S. Bhunia. System-on-Chip Platform Security Assurance: Architecture and Validation. Proceedings of the IEEE volume 106(1), January 2018, pages 21-37. IEEE.
• S. Ray, A. Basak, and S. Bhunia. Patching the Internet of Things. IEEE Spectrum: Technology, Engineering, and Science News volume 54(11), November 2017, pages 31-35. IEEE.
• W. Chen, S. Ray, M. S. Abadir, J. Bhadra, and L. Wang. Challenges and Trends in Modern SoC Design Verification. IEEE Design & Test volume 34(5), September-October 2017, pages 7-22. IEEE.
• P. Mishra, R. Morad, A. Ziv, and S. Ray. Post-silicon Validation in the SoC Era: A Tutorial Introduction. IEEE Design & Test volume 34(3), May-June 2017, pages 68-92. IEEE.
• A. Basak, S. Bhunia, T. Tkacik, and S. Ray. Security Assurance in System-on-Chip Designs with Untrusted Components. IEEE Transactions on Information Forensics and Security volume 12(7), 2017, pages 1515-1528. IEEE.
• K. Rahmani, S. Ray, and P. Mishra. Post-silicon Trace Signal Selection Using Machine Learning Techniques. IEEE Transactions on VLSI Systems volume 25(2), February 2017, pages 570-580. IEEE.
• S. Ray, J. Park, and S. Bhunia. Wearables, Implants, and Internet of Things: The Technology Needs in the Evolving Landscape. IEEE Transactions on Multi-Scale Computing Systems volume 2(2), April-June 2016, pages 123-128. IEEE Computer Society. Featured Paper for April-June 2016 Issue
• S. Ray, Y. Jin, and A. Raychowdhury. The Changing Computing Paradigm with Internet of Things: A Tutorial Introduction. IEEE Design & Test volume 33(2), March-April 2016, pages 76-96. IEEE Computer Society.
• S. Ray and R. Sumners. Specification and Verification of Concurrent Programs through Refinements. Journal of Automated Reasoning, volume 51(3) Septmber 2013, pages 241-280. Springer. (This paper supercedes the EC² 2011 paper below. In particular, it puts the framework described there in context, provides a detailed technical description, and presents several interesting applications.)
• 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 Conference/Symposia

• A. Bhadra and S. Ray. Adaptive Robotic Arm System for Wheelchair Assistance in Autonomous Vehicles. In C. Fan, S. Sugawara, K. Ueda, Y. Fan, K. Tsang, N. Herencsar, and K. Kikuma editors 42nd IEEE International Conference on Consumer Electronics (ICCE 2024), Las Vegas, NV, USA, January 2024. IEEE.
• D. Halder, M. Merugu, and S. Ray. ObNoCs: Protecting Network-on-Chip Fabrics Against Reverse-Engineering Attacks. In S. Bhunia and J. Doppa editors, International Conference on Compilers, Architectures, and Synthesis for Embedded Systems (CASES 2023), Hamburg, Germany, September 2023.
• X. Chen, D. halder, K. M. Islam, and S. Ray. Work-In-Progress: Towards Evaluating CNNs Against Integrity Attacks on Multi-tenant Computation. In S. Bhunia and J. Doppa editors, International Conference on Compilers, Architectures, and Synthesis for Embedded Systems (CASES 2023), Hamburg, Germany, September 2023.
• P. SLPSK, J. Cruz, S. Ray, and S. Bhunia. PROTECTS: Secure Provisioning of System-on-Chip Assets in Untrusted Testing Facility. In. S. Chillarige, K. Pandey, V. R. Totakura, K. Shankar, S. Sivanantham, and P. Kalla editors, 7th IEEE International Test Conference India (ITC India 2023), Bangalore, India, July 2023. IEEE.
• D. M. Prakash, B. B. Yedla Ravi, S. Boddupalli, and S. Ray. VeCAEP: A Hands-on Exploration Platform for Vehicular Communication Attacks. In A. Reatti, L. Ciani, G. M. Lozito, F. Corti, R. Dinis, A.Trivino, L. Pugi, and S. Musumeci editors, IEEE 97th Vehicular Technology Conference (VTC 2023), Florence, Italy, June 2023. IEEE.
• R. Owoputi, M. R. Kabir, and S. Ray. IVE: An Immersive Virtual Environment for Automotive Security Exploration. In 9th International Conference of the Immersive Learning Research Network (iLRN 2023), San Luis Obispo, CA, USA, June 2023.
• X. Chen and S. Ray. Geralt: Real-time Detection of Evasion Attacks in Deep Learning Systems. In J. Rabaey, B. Murmann, K. Gunnam, and M. Alioto editors, IEEE International Symposium on Circuits and Systems (ISCAS 2023), Monterey, CA, USA, May 2023. IEEE.
• M. R. Kabir and S. Ray. Virtualization for Automotive Safety and Security Exploration. In G. Mehta, H. Lee, B. C. Schaefer, J. Kim, and P. Indic editors, 16th IEEE Dallas Circuits and Systems (DCAS 2023), Dallas, TX, USA, April 2023. IEEE.
• S. A. Mila, M. R. Kabir, and S. Ray. Continuous Monitoring for Diagnosis: A Wearable for Covid-19 Detection in Symptomatic Patients. In I. Gedeon, S. Rajan, A. Anvari-Moghaddam, and M. Sode editors, 41st International Conference on Consumer Electronics (ICCE 2023), Las Vegas, NV, USA, January 2023. IEEE.
• V. S. G. Chamarthi, X. Chen, B. B. Yedla Ravi, and S. Ray. Exploration of Machine Learning Attacks in Automotive Systems Using Physical and Mixed Reality Platforms. In I. Gedeon, S. Rajan, A. Anvari-Moghaddam, and M. Sode editors, 41st International Conference on Consumer Electronics (ICCE 2023), Las Vegas, NV, USA, January 2023. IEEE.
• S. Boddupalli, V. S. G. Chamarthi, C. Lin, and S. Ray. CAVeliEr: Automated Security Evaluation for Connected Autonomous Vehicle Applications. In J. H. Lee and F. Wang editors, 25th IEEE International Conference on Intelligent Transportation (ITSC 2022), Macau, China, October 2022. IEEE.
• S. Boddupalli, R. Owoputi, C. Duan, T. Choudhury, and S. Ray. Resiliency in Connected Vehicle Applications: Challenges and Approaches for Security Validation. In I. Savidis, A. Sasan, H. Thapliyal, and R. F. DeMara editors, 31st ACM Great Lakes Symposium on VLSI (GLSVLSI 2022), Irvine, CA, USA, June 2022. ACM.
• S. Wang, C. Lin, S. Boddupalli, C. Lin, and S. Ray. Deep Learning Based Anomaly Detection for Lane Changing Decision. In L. Eckstein, C. Stiller, B. Morris, and L. Vlacic editors, 33rd IEEE Intelligent Vehicles Symposium (IV 2022), Aachen, Germany, June 2022. IEEE.
• T. Alam, Z. Yang, B. Chen, N. Armour, and S. Ray. FirVer: Concolic Testing for Systematic Validation of Firmware Binaries. In T. Wang and M. Hashimoto editors, 27th Asia and South Pacific Design Automation Conference (ASP-DAC 2022), Virtual Conference, January 2022. ACM.
• B. Yedla Ravi, M. R. Kabir, N. Mishra, S. Boddupalli, and S. Ray. AutoHaL: An Exploration Platform for Ranging Sensor Attacks on Automotive Systems. In I. Gedeon, J. Chung, and S. Pack editors, 40th International Conference on Consumer Electronics (ICCE 2022), Virtual Conference, January 2022. IEEE.
• K. Raj, A. Hegde, A. P. Deb Nath, S. Bhunia, and S. Ray. SSEL: An Extensible Specification Language for SoC Security. In X. Li, D. Mukhopadhyay, P. Zhou, and Y. Cao editors, Asian Hardware Oriented Security and Trust (AsianHOST 2021), Shanghai, P.R. China, December 2021. IEEE.
• X. Meng, K. Raj, A. P. Deb Nath, K. Basu, and S. Ray. SoCCAR: Detecting System-on-Chip Security Violations Under Asynchronous Resets. In 58th ACM/IEEE Design Automation Conference (DAC 2021), San Francisco, CA, USA, December 2021, pages 625-630. ACM.
• J. Zhang, X. Chen, and S. Ray. Universal Neural Network Acceleration via Real-Time Loop Blocking. In M. Ciesielski, R. Sendag, G. P. Venkataramani, and R. Jayabharathi editors, 39th IEEE International Conference on Computer Design (ICCD 2021), Virtual Conference, October 2021. IEEE.
• M. R. Kabir, N. Mishra, and S. Ray. ViVE: Virtualization of Vehicular Electronics for System-level Exploration. In Y. Chen, N. Zheng, M. A. Sotelo, S. Barbat, and L. Li editors, 24th IEEE International Conference on Intelligent Transportation (ITSC 2021), Indianapolis, IN, USA, September 2021, pages 3307-3312. IEEE.
• S. Boddupalli, A. Hegde, and S. Ray. RePLACe: Real-time Security Assurance in Vehicular Platoons Against V2V Attacks. In Y. Chen, N. Zheng, M. A. Sotelo, S. Barbat, and L. Li editors, 24th IEEE International Conference on Intelligent Transportation (ITSC 2021), Indianapolis, IN, USA, September 2021, pages 1179-1185. IEEE.
• S. Wang, S. Wu, C. Lin, S. Boddupalli, P. Chang, C. Lin, C. Shih, and S. Ray. Deep-Learning-Based Intrusion Detection for Autonomous Vehicle-Following Systems. In Y. Chen, N. Zheng, M. A. Sotelo, S. Barbat, and L. Li editors, 24th IEEE International Conference on Intelligent Transportation (ITSC 2021), Indianapolis, IN, USA, September 2021, pages 865-872. IEEE.
• S. Ray, A. P. Deb Nath, K. Raj, and S. Bhunia. The Curious Case of Trusted IC Provisioning in Untrusted Testing Facilities. In Y. Chen, V. Zhimov, A. Sasan, and I. Savidis editors, 31st ACM Great Lakes Symposium on VLSI (GLSVLSI 2021), Virtual Conference, June 2021, pages 207-212. ACM.
• S. Ray and A. Sinha. Synergies Between Delay Test and Post-silicon Speed Path Validation: A Tutorial Introduction. In Y. Chen, V. Zhimov, A. Sasan, and I. Savidis editors, 31st ACM Great Lakes Symposium on VLSI (GLSVLSI 2021), Virtual Conference, June 2021. IEEE.
• S. Ray, A. P. Deb Nath, K. Raj, and S. Bhunia. CASTLE: Architecting Assured System-on-Chip Firmware Integrity. In F. Fummi, I. O’Connor, and I. Verbauwhede editors, Design, Automation & Test in Europe (DATE 2021), Virtual Conference, February 2021. IEEE.
• D. Chhibber, A. Tripathi, and S. Ray. DoVir: Virtualizing Food Donation Distribution through Mobile Application and Cloud-Based Supply Chain Management. In I. Gedeon, S. Katkoori, J. Chung, and Y. Fan editors, 39th International Conference on Consumer Electronics, Virtual Conference, January 2021. IEEE.
• S. Boddupalli and S. Ray. REDEM: Real-Time Detection and Mitigation of Communication Attacks in Connected Autonomous Vehicle Applications. In A. Casaca, S. Katkoori, S. Ray, and L. Strous editors, Internet of Things, A Confluence of Many Disciplines: Proceedings of the 2nd IFIP International Conference on Internet of Things (IFIPIoT 2019), Tampa, FL, USA, October 2019, volume 574 of AICT, pages 105-122. Springer.
• Y. Cao, H. Zheng, and S. Ray. A Communication-Centric Observability Selection for Post-silicon System-on-Chip Integration Debug. In 20th International Symposium on Quality Electronic Design (ISQED 2019), Santa Clara, CA, USA, March 2019.
• S. Ray. Safety, Security, and Reliability: The Automotive Robustness Problem and an Architectural Solution. In A. Sengupta and D. Kudithipudi editors, 37th IEEE International Conference on Consumer Electronics (ICCE 2019), Las Vegas, NV, USA, January 2019. IEEE.
• A. P. Deb Nath, S. Bhunia, and S. Ray. ArtiFact: Architecture and CAD Flow for Efficient Formal Verification of SoC Security Policies. In W. Zhang, J. Xue, Z. Shao, H. Li, Y. Wang, and W. Wen editors, IEEE Computer Society Annual Symposium on VLSI (ISVLSI 2018), Hong Kong SAR, China, July 2018. IEEE.
• Y. Cao, H. Palombo, H. Zheng, and S. Ray. Enhanced Observability for Post-Silicon Debug with On-Chip Communication Monitors. In W. Zhang, J. Xue, Z. Shao, H. Li, Y. Wang, and W. Wen editors, IEEE Computer Society Annual Symposium on VLSI (ISVLSI 2018), Hong Kong SAR, China, July 2018. IEEE.
• S. Ray, W. Chen, and R. Cammarota. Protecting the Supply Chain for Automotives and IoTs. In X. S. Hu, R. Aitken, V. Bertacco, and A. Raghunathan editors 55th Design Automation Conference (DAC 2018), San Fancisco, CA, USA, June 2018, pages 89:1-89:4. ACM.
• D. Pal, A. Sharma, S. Ray, F. M. de Paula, and S. Vasudevan. Application Level Hardware Tracing for Scaling Post-silicon Debug. In X. S. Hu, R. Aitken, V. Bertacco, and A. Raghunathan editors 55th Design Automation Conference (DAC 2018), San Fancisco, CA, USA, June 2018, pages 92:1-92:6. ACM. Best Paper Nomination
• A. P. Deb Nath, S. Ray, A. Basak, and and S. Bhunia. System-on-Chip Security Architecture and CAD Framework for Hardware Patch. In Y. Shin, A. Takahashi, T. Kim, and Y. Chen editors, 23rd Asia and South Pacific Design Automation Conference (ASP-DAC 2018), Jeju Island, Korea, January 2018. ACM.
• S. Ray. Transportation Security in the Era of Autonomous Vehicles: Challenges and Practice. In S. Parameswaran, I. Bahar, and D. Pan editors, 36th International Conference on Computer-Aided Design (ICCAD 2017), Irvine, CA, USA, November 2017. IEEE.
• Y. Cao, H. Palombo, H. Zheng, S. Ray, and J. Yang. A Post-silicon Trace Analysis Approach for System-on-Chip Protocol Debug. In O. Khan, S. Ozev, O. Sinanoglu, and U. Ogras editors, 35th IEEE International Conference on Computer Design (ICCD 2017), Boston, MA, USA, November 2017, pages 177-184. IEEE.
• S. Ray, W. Chen, J. Bhadra, and M. A. Al Faruque. Extensibility in Automotive Security: Current Practice and Challenges. In M. McNamara, X. S. Hu, R. Aitken, and V. Bertacco editors, 54th International ACM/EDAC/IEEE Design Automation Conference (DAC 2016), Austin, TX, USA, June 2016. ACM.
• S. Ray. System-on-Chip Security Assurance for IoT Devices: Cooperations and Conflicts. In D. Thelen, K. Tam, and A. Pivoccari editors, IEEE Custom Integrated Circuits Conference (CICC 2017), Austin, TX, USA, April-May 2017. IEEE.
• R. Karam, T. Hoque, S. Ray, M. Tehranipoor, and S. Bhunia. MUTARCH: Architectural Diversity for FPGA Device and IP Security. In N. Takagi and D. Pan editors, 22nd Asia and South Pacific Design Automation Conference (ASP-DAC 2017), Tokyo, Japan, January 2017. ACM.
• R. Karam, T. Hoque, S. Ray, M. Tehranipoor, and S. Bhunia. Robust Bitstream Protection in FPGA-based Systems through Low-Overhead Obfuscation. In R. Cumplido, P. Athanas, and R. Sass editors, 2016 International Conference on Reconfigurable Computing and FPGAs (ReConFig 2016), Cancun, Mexico, November 2016. IEEE.
• S. Ray, I. Harris, G. Fey, and M. Soeken. Multilevel Design Understanding: From Specification to Logic. In F. Liu, S. Parameswaran, and I. Bahar editors, 35th International Conference on Computer-Aided Design (ICCAD 2016), Austin, TX, USA, November 2016. IEEE.
• S. Ray, T. Hoque, A. Basak, and S. Bhunia. The Power Play: Security-Energy Trade-offs in the IoT Regime. In S. Ozev, R. Karri, O. Khan, and O. Sinanoglu editors, Proceedings of the 34th IEEE International Conference on Computer Design (ICCD 2016), Phoenix, AZ, USA, October 2016, pages 690-693. IEEE.
• S. Ray and J. Bhadra. Security Challenges in Mobile and IoT Systems. In D. Zhao, A. Marshall, K. Bhatia, and M. Alioto editors, Proceedings of the 29th IEEE International System-on-Chip Conference (SOCC 2016), Seattle, WA, USA, September 2016. IEEE.
• A. Basak, S. Bhunia, and S. Ray. Exploiting Design-for-Debug for Flexible SoC Security Architecture. In C. Alpert, M. McNamara, X. S. Hu, N. Chang, and V. Bertacco editors, 53rd International ACM/EDAC/IEEE Design Automation Conference (DAC 2016), Austin, TX, USA, June 2016, pages 167:1-167:6. ACM.
• S. Ray, S. Bhunia, Y. Jin, and M. Tehranipoor. Security Validation in IoT Space. In Y. Makris, S. Ravi, and L. Anghel editors, Proceedings of the 34th IEEE VLSI Test Symposium (VTS 2016), Las Vegas, NV, USA, April 2016, page 1. IEEE Computer Society.
• Z. Yang, K. Hao, K. Cong, L. Lei, S. Ray, and F. Xie. Validating Scheduling Transformations for Behavioral Synthesis. In Design, Automation & Test in Europe (DATE 2016), Dresden, Germany, March 2016, pages 1652-1657. IEEE.
• F. Farahmandi, P. Mishra, and S. Ray. Exploiting Transaction-Level Models for Observability-Aware Post-silicon Test Generation. In Design, Automation & Test in Europe (DATE 2016), Dresden, Germany, March 2016, pages 1477-1480. IEEE.
• H. Zheng, Y. Cao, S. Ray, and J. Yang. Protocol-Guided Analysis of Post-silicon Traces Under Limited Observability. In P. Wright, S. Mukhopadhyay, and B. Cline editors, 17th International Symposium on Quality Electronic Design (ISQED 2016), Santa Clara, CA, USA, March 2016. IEEE.
• A. Basak, S. Bhunia, and S. Ray. A Flexible Architecture for Systematic Implementation of SoC Security Policies. In D. Marculescu, F. Liu, and S. Parameswaran editors, 34th International Conference on Computer-Aided Design (ICCAD 2015), Austin, TX, USA, November 2015, pages 536-543. IEEE.
• S. Ray and Y. Jin. Security Policy Enforcement in Modern SoC Designs. In D. Marculescu, F. Liu, and S. Parameswaran editors, 34th International Conference on Computer-Aided Design (ICCAD 2015), Austin, TX, USA, November 2015, pages 345-350. IEEE.
• S. Ma, D. Pal, R. Jiang, S. Ray, and S. Vasudevan. Can’t See the Forest for Trees: State Restoration’s Limitations in Post-silicon Trace Signal Selection. In D. Marculescu, F. Liu, and S. Parameswaran editors, 34th International Conference on Computer-Aided Design (ICCAD 2015), Austin, TX, USA, November 2015, pages 1-8. IEEE. Best Paper Nomination
• M. Talupur, S. Ray, and J. Erickson. Transaction Flows and Executable Models: Formalization and Analysis of Message Passing Protocols. In R. Kaivola and T. Wahl editors, Proceedings of the 15th International Conference on Formal Methods in Computer-aided Design (FMCAD 2015), Austin, TX, USA, September 2015, pages 168-175.
• R. Kannavara, C. J. Havlicek, B. Chen, M. R. Tuttle, K. Cong, S. Ray, and F. Xie. Challenges and Opportunities with Concolic Testing. In N. Bourbakis and S. Boddhu editors, 2015 IEEE National Aerospace Conference / Ohio Innovation Summit & IEEE Symposium on Monitoring & Surveillance Research (NAECON-OIS 2015), Dayton, OH, USA, June 2015. IEEE.
• S. Ray, J. Yang, A. Basak, and S. Bhunia. Correctness and Security at Odds: Post-silicon Validation of Modern SoC Designs. In A. Cirkel, X. S. Hu, and R. Aitken editors, 52nd International ACM/EDAC/IEEE Design Automation Conference (DAC 2015), San Francisco, CA, USA, June 2015. ACM.
• D. Puri, K. Hao, S. Ray, and F. Xie. Mechanical Certification of Loop Pipelining Transformations: A Preview. In R. Gamboa and G. Klein editors, Proceedings of the 5th International Conference on Interactive Theorem Proving (ITP 2014), Vienna, Austria, July 2014, volume 8558 of LNCS, pages 549-554. Springer.
• Z. Yang, K. Hao, K. Cong, L. Lei, S. Ray, and F. Xie. Scalable Certification Framework for Behavioral Synthesis Front-End. In S. Hassoun, C. Alpert, and S. Hu editors, 51st International ACM/EDAC/IEEE Design Automation Conference (DAC 2014), San Francisco, CA, USA, June 2014. ACM.
• K. Rahmani, P. Mishra, and S. Ray. Efficient Trace Signal Selection Using Augmentation and ILP Techniques. In M. Budnik, S. A. Alam, and P. Wright editors, 15th International Symposium on Quality Electronic Design (ISQED 2014), Santa Clara, CA, USA, March 2014, pages 148-155. IEEE.
• K. Hao, S. Ray, and F. Xie. Equivalence Checking for Function Pipelining in Behavioral Synthesis. In Design, Automation & Test in Europe (DATE 2014), Dresden, Germany, March 2014. IEEE.
• Z. Yang, K. Hao, K. Cong, S. Ray, and F. Xie. Equivalence Checking for Compiler Transformations in Behavioral Synthesis. In G. Byrd, K. Schneider, N. Chang, and S. Ozev editors, Proceedings of the 31st IEEE International Conference on Computer Design (ICCD 2013), Asheville, NC, USA, October 2013, pages 491-494. IEEE.
• K. Rahmani, P. Mishra, and S. Ray. Scalable Trace Signal Selection Using Machine Learning. In G. Byrd, K. Schneider, N. Chang, and S. Ozev editors, Proceedings of the 31st IEEE International Conference on Computer Design (ICCD 2013), Asheville, NC, USA, October 2013, pages 384-389. IEEE.
• Z. Yang, K. Hao, S. Ray, and F. Xie. Handling Design and Implementation Optimizations in Equivalence Checking for Behavioral Synthesis. In D. Sciuto and C. Alpert editors, 50th International ACM/EDAC/IEEE Design Automation Conference (DAC 2013), Austin, TX, USA, June 2013. ACM.
• K. Hao, S. Ray, and F. Xie. Equivalence Checking for Behaviorally Synthesized Pipelines. In P. Groeneveld, D. Sciuto, and S. Hassoun, editors, 49th International ACM/EDAC/IEEE Design Automation Conference (DAC 2012), San Francisco, CA, USA, June 2012, pages 344-349. ACM.
• S. Ray and J. Bhadra. Verification and Testing Challenges with High-level Synthesis. In M. Renovell and C. Thibeault, editors, Proceedings of the 28th IEEE VLSI Test Symposium (VTS 2010), Santa Cruz, CA, USA, April 2010, page 250. IEEE Computer Society.
• 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, USA, 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, USA, 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, USA, 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, USA, 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, USA, November 2007, pages 239-242. IEEE Computer Society. (This paper and the NVMTS 2008 paper are superceded by the ISQED 2010 paper above.) Best Paper Nomination
• 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, USA, 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, USA, July 2004, volume 3114 of LNCS, pages 31-43. Springer.

Publications in Peer-reviewed Workshops

• B. B. Yedla Ravi, M. R. Kabir, S. A. Mila, and S. Ray. IoT-based Onboard Prognostic Health Evaluation System for Automotive Suspensions. In Y. Zorian, D. Appello, R. Cantoro, and W. Dobbelaere editors, 3rd European Workshop on Automotive Reliability, Test and Safety in Europe (eARTS 2023), Venice, Italy, May 2023. IEEE.
• M. R. Kabir and S. Ray. Exploring System-level Coordination of Vehicular Electronics: A Case Study for Traction Control. In Y. Zorian, N. Maor, D. Appello, and P. Bernardi editors, 6th IEEE Automotive Reliability, Test, and Safety Workshop (ARTS 2021), Virtual Conference, October 2021. IEEE.
• D. Puri, S. Ray, K. Hao, and F. Xie. Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis. In F. Verbeek and J. Schmaltz, editors, Proceedings of the 12th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2014), Vienna, Austria, July 2013. volume 152 of EPTCS, pages 111-128.
• D. Puri, S. Ray, and F. Xie. Towards Certifiable Loop Pipelining Transformations in Behavioral Synthesis. In M. Velev, editor, Proceedings of the 8th International Workshop on Constraints in Formal Verification (CFV 2013), San Jose, CA, USA, November 2013.
• O. Olivo, S. Ray, J. Bhadra, and V. Vedula. A Unified Formal Framework for Analyzing Functional and Speed-path Properties. 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, USA, December 2011, pages 44-45. IEEE.
• 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. (This is a short five-page initial summary of the work. For a detailed presentation, see the 2012 JAR article.)
• 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, USA, 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, USA, 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, USA, 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, USA, 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, USA, 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, USA, 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, USA, 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.

Book Chapters

• S. Boddupalli, R. Owoputi, C. Duan, T. Choudhury, and S. Ray. Machine Learning for Security Resiliency in Connected Vehicle Applications. To Appear In V. K. Kukkala and S. Pasricha editors, Machine Learning and Optimization Techniques for Automotive Cyber-Physical Systems, 2022. Springer.
• S. Goel and S. Ray. Theorem Proving for Microarchitecture Assurance. To Appear In A. Chattopadhyay editor, Handbook of Computer Architecture, 2022. Springer.
• S. Ray. System-on-Chip Security in the IoT Regime: Challenges and Recent Trends. In A. Sheikholeslami, J. Van der Spiegel, and Y. Wang editors, IC Design Insights: Tutorials in Solid State Circuits, ISBN 978-87-7022-049-1 (print) and 978-87-7022-048-4 (e-book), pages 619-635, 2019. IEEE Solid State Circuits Society.
• S. Ray. SoC Instrumentations: Pre-silicon Preparation for Post-silicon Readiness. In F. Farahmandi and P. Mishra editors, Post-silicon Validation and Debug, ISBN 978-3-319-98115-4, pages 19-32, 2018. Springer.
• A. P. Deb Nath, T. Hoque, S. Ray, and S. Bhunia. An Adaptable System-on-Chip Security Architecture for Internet of Things Applications. In R. S. Chakraborty, J. Mathew, and A. V. Vasilakos editors, Security and Fault Tolerance in Internet of Things, 2018, ISBN 978-3-030-02806-0 (print) and 978-3-030-02807-7 (e-book), pages 61-85. Springer.
• S. Ray. Hardware Trust in Industrial SoC Designs: Current Practice and Challenges. In S. Bhunia and M. Tehranipoor editors, The Hardware Trojan War: Attacks, Myths, and Defenses, 2017, ISBN 978-3-319-68511-3, pages 371-383. Springer.
• S. Ray, S. Sur-Kolay, and S. Bhunia. The Landscape of IP and SoC Security. In S. Bhunia, S. Ray, and S. Sur-Kolay editors, Fundamentals of IP and SoC Security: Design, Verification, and Debug, 2017, pages 9-27. Springer.
• S. Ray, P. Mishra, and S. Bhunia. Security Validation in Modern SoC Designs. In S. Bhunia, S. Ray, and S. Sur-Kolay editors, Fundamentals of IP and SoC Security: Design, Verification, and Debug, 2017, pages 9-27. Springer.
• S. Bhunia, S. Sur-Kolay, and S. Ray. SoC Security: Summary and Future Directions. In S. Bhunia, S. Ray, and S. Sur-Kolay editors, Fundamentals of IP and SoC Security: Design, Verification, and Debug, 2017, pages 9-27. Springer.

Technical Reports, Drafts, and Miscellaneous Writings

• S. Ray, J. Park, and S. Bhunia. Wearables, Implants, and Internet of Things. Guest Editorial, IEEE Transactions on Multi-Scale Computing Systems. IEEE Computer Society.
• S. Ray, J. Bhadra, M. S. Abadir, and L. Wang. Test and Verification Challenges in Future Microprocessor and SoC Designs. Guest Editorial, Journal of Electronic Testing: Theory and Applications, volume 29(5), October 2013, pages 621-623. Springer.
• B. Jobstmann and S. Ray, Preface, Proceedings of the 13th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2013), October 2013.
• S. Ray, J. Bhadra, M. S. Abadir, L. Wang, and A. Gupta. Verification Challenges in the Concurrent World. Guest Editorial, ACM Transactions on Design Automation of Electronic Systems (ACM TODAES), volume 17(3), June 2012, pages 19.1-19.3. ACM.
• 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.