Sandip Ray

Here I am

Research Scientist

Strategic CAD Labs
Intel Corporation
Hillsboro, OR 97124, USA.


Welcome to my electronic den. As you have no doubt guessed, the person staring at you from the picture above is me. This very basic Web page is intended to keep track of my current activities.


I am a CAD Research Scientist at Strategic CAD Labs, Intel Corporation. Prior to this, I was a Research Scientist at the Center for Information Assurance and Security, Department of Computer Science, University of Texas at Austin. I graduated with a Ph.D from the same department in December 2005.

This page is divided into the following sections.

Standard Disclaimer: Any opinion, finding, conclusion, or recommendation expressed in this Web page (or any other Web page authored by me) is mine, and does not necessarily represent the official position of the University of Texas or any part of the government of the state of Texas or any other organization or person in the world. I do not provide any guarantee regarding the accuracy of anything in this Web page; however, if you find any errors or have any other comment or criticism (or, for that matter, appreciation), I will appreciate if you let me know.


My chief research interest is in trustworthy computing, i.e., making sure that our computing systems behave reliably, securely, and according to specification. My work brings in techniques from synthesis, architecture, verification, and validation. In most recent work, I have been focusing on techniques for security validation and post-silicon validation for System-on-Chip designs. I have also been looking at future computing systems, e.g., wearables, and Internet-of-Things, and trying to understand how the security and validation problems change in that regime.

In my past life, I worked chiefly on formal verification. I focused on developing scalable custom techniques for verifying a slew of applications, including software correctness, concurrent protocol verification, formalization and verification of information flow properties, certification of behavioral synthesis transformations, and verification of analog and mixed signal designs. Much of this work married mechanical theorem proving with more automated tools. While at UT Austin, I was a member of the UT Austin Automatic Theorem Proving Research Group. My Ph.D advisor was J Strother Moore, and a large chunk of my research, both during my Ph.D. and afterwards, has revolved around the ACL2 theorem prover that he has co-authored with Matt Kaufmann. I also dabbled a bit into two other theorem provers, Coq and Isabelle. My projects at UT Austin were sponsored by NSF, DARPA, and SRC, and found application in the verification tool-flow of a number of companies including AMD, Freescale, Galois, IBM, Intel, and Rockwell-Collins.

After moving to Intel, while I still sometimes use formal methods, I have developed a deep appreciation for semi-formal methods and dynamic verification techniques. I have continued to do formal verification work, in particular using SAT and SMT techniques and Intel's Forte system, and have also worked on combining mechanical theorem proving with these approaches to develop robust, domain-specific verification strategies. But I have also learned to see verification as one component in the scheme of a larger collection of methods to ensure correctness and resiliency. My current work therefore focuses on marrying verification and validation techniques with resiliency infrastructures, e.g., those based on architecture and synthesis. Such combination can be incredibly powerful, and provide promising approaches to handle complex system security infrastructures. I believe they will be even more important in future, with wearables, fashionable implants, and IoTs.

My other research interests include Distributed Systems, Algorithm Analysis, Complexity Theory, Logic, and Foundations of Mathematics.

Additional details about my research and professional colleagues are available from the following pages.

Many of the publications, particularly those pertaining to research I did during my tenure at UT Austin, have to do with ACL2. Such papers are also linked from the Web page “Books and Papers About ACL2 and Its Application” maintained by Matt Kaufmann and J Strother Moore. That Web page contains a comprehensive listing of (and links to) a number of books and papers written by several ACL2 users. If you are interested in the ACL2 and its applications, I strongly recommend that you visit the page.

I have compiled a list of interesting papers about verification of microprocessors and digital hardware designs here. If you are doing research in this area, I hope you find the list useful.

As a researcher, I find Dijkstra's three golden rules for successful scientific research very illuminating.


I co-taught the following classes at UT Austin. My teaching style has been significantly inspired by the Ten Commandments of Yale Patt.

Professional Services

The following list tracks my editorial and conference committee activities.

Jason Baumgartner, Ganesh Gopalakrishnan, Warren A. Hunt, Jr., and I maintain the FMCAD Mailing List. This list is intended to provide an open mechanism for researchers to communicate on topics related to the use of formal methods in computer-aided design. If you are interested in this area, I urge you to join the mailing list.

Warren A. Hunt, Jr. and I maintain the FMCAD Organization Home Page. FMCAD is a major conference, providing a forum for researchers to present cutting-edge research related to the use of formal methods in computer-aided design. FMCAD 2012 will be held in Cambridge, United Kingdom.

I am a Senior Member of IEEE, Professional Member of ACM, and Full Member of the Sigma Xi Scientific Research Society.


As you can see, I am thoroughly overworked (tongue in cheek) and have little time to indulge in other activities. When I do have time, I like to do the following. Note especially the third item. At some point in my past life, I used to love writing (non-technical) essays and poetry. I do not find time for that any more, mostly because I am lazy and that kind of work requires more mental exertion than I am prepared to execute. Well, that should tell you what I like most in my day-to-day life, namely “lolling in the sofa” doing nothing.