Sandip Ray

Research Scientist

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

EMAIL: sandip@cs.utexas.edu
WWW: http://www.cs.utexas.edu/~sandip

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.

News

Barbara Jobstmann and I are co-chairing FMCAD 2013, to be held in Portland, OR, USA on October 20-23, 2013 co-located with MEMOCODE 2013. Consider participating!
As of October 2011, I have moved to Strategic CAD Labs, Intel Corporation, where I will be focusing on verification techniques to facilitate post-silicon validation.
My book “Scalable Techniques for Formal Verification” has been published by Springer. The book Web page contains an overview and purchasing information.

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.

Research
Teaching
Professional Services
Personal Information

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.

Research

My chief research interest is in the formal verification, i.e., the use of formal mathematical analysis to ensure the correctness and security of of computing systems. My current focus is on developing scalable techniques for post-silicon verification of industrial designs. In the past, I have worked on developing formal analysis techniques for 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. My work encompasses both mechanical theorem proving techniques and algorithmic decision procedures. 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 have also dabbled a bit into two other theorem provers, Coq and Isabelle. After moving to Intel, I have started focusing more on automated verification approaches based on SAT and SMT techniques and using Intel's Forte system. My other research interests include Model Checking, Distributed Systems, Algorithm Analysis, Complexity Theory, Logic, and Foundations of Mathematics.

The following project pages provide a flavor of some of the research areas that I have worked on. The projects are listed in no particular order. Note that the list of projects is not exhaustive: for a more comprehensive overview of my research activities, see my publications.

[Note: The project pages below are no longer maintained since I left UT Austin. I leave them here as a record of a snapshot of my activities circa 2011. But they have not been updated (beyond cosmetic changes) since.]

Run-time Hardware/Software Co-monitoring

Robust Reasoning Framework for Machine Code Verification

High-Assurance Behavioral Synthesis

Analysis of Reactive Systems

Verification of Analog/Mixed-signal Designs

Post-silicon Verification

My research at UT Austin was funded in part by grants from the following projects. I gratefully acknowledge the support. The project pages above credit the individual fundings associated with each project.

Code Verification for Practical Machine Architectures, Defense Advanced Research Projects Agency, October 2010 – September 2014. Principal Investigator: S. Ray; Co-PI: W. A. Hunt, Jr.

TC: Small: Collaborative Research: Trustworthy Hardware from Certified Behavioral Synthesis, National Science Foundation Grant CCF-0916772, September 2009 – August 2011. Principal Investigator: S. Ray; Co-PI: W. A. Hunt, Jr. (Collaborative Research with Portland State University Grant CCF-0917188. PSU PI: F. Xie)

TC: Large: A Formal Platform for Analyzing Internet Routing, National Science Foundation Grant CNS-0910913, September 2009 – August 2011. Principal Investigator: S. Ray; Co-PIs: W. A. Hunt, Jr. and Y. Zhang

Combined Pre-silicon and Post-silicon Verification for Custom and SoC Designs, Semiconductor Research Corporation Grant 08-TJ-1849, October 2008 – September 2011. Principal Investigator: W. A. Hunt, Jr.; Co-PI: S. Ray

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

Publications

List of Collaborators

Many of the publications above 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.

Teaching

I co-taught the following classes at UT Austin.

CS389R Recursion and Induction, Fall 2010, co-instructor with Warren A. Hunt, Jr.
CS395T Industrial Formal Methods, Fall 2009, co-instructor with Warren A. Hunt, Jr.
CS389R Recursion and Induction, Fall 2008, co-instructor with Warren A. Hunt, Jr.

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.

Program Committee Member DATE 2014, Dresden, Germany, March 2013
Co-chair (with B. Jobstmann) FMCAD 2013, Portland, OR, USA, October 2013
Guest editor (with J. Bhadra, M. Abadir, and L.-C Wang), JETTA Special Issue on Verification and Testing Challenges in Future Microprocessor and SoC Designs (CFP)
Program Committee Member ACL2 2013, Laramie, WY, USA, May 2013
Program Committee Member FMCAD 2012, Cambridge, United Kingdom, October 2012
Program Committee Member MTV 2011, Austin, TX, USA, December 2011
Program Committee Member CPP 2011, Taiwan, December 2011
Program Committee Member ACL2 2011, Austin, TX, USA, November 2011
Program Committee Member FMCAD 2011, Austin, TX, USA, November 2011
Program Committee Member ITP 2011, Nijmegen, the Netherlands, August 2011
Publicity Chair CAV 2011, Snowbird, UT, USA, July 2011
Guest editor (with J. Bhadra, M. Abadir, L.-C Wang, and A. Gupta), ACM TODAES Special Issue on Verification Challenges with Multicore Systems (CFP)
Program Committee Member MTV 2010, Austin, TX, USA, December 2010
Program Committee Member ITP 2010, Edinburgh, United Kingdom, August 2010
Session Organizer (with J. Bhadra) VTS 2010, Santa Cruz, CA, USA, April 2010 (Innovative Practices session on verification/testing challenges in high-level synthesis)
Program Committee Member MTV 2009, Austin, TX, USA, December 2009
Session Organizer and Chair MTV 2009, Austin, TX, USA, December 2009 (Invited session on verification issues for multicore systems)
Program Committee Member FMCAD 2009, Austin, TX, USA, November 2009
Local Arrangements Co-chair (with A. Slobodová) FMCAD 2009, Austin, TX, USA, November 2009
Steering Committee Member International Workshop on the ACL2 Theorem Prover and Its Applications, May 2009 -- Present
Co-chair (with D. Russinoff) ACL2 2009, Boston, MA, USA, May 2009
Session Organizer and Chair MTV 2008, Austin, TX, USA, December 2008 (Invited session on post-silicon verification)
Program Committee Member FMCAD 2008, Portland, OR, USA, November 2008
Scientific Committee Member MS 2008, Petra, Jordan, November 2008
Program Committee Member ESHOL 2008, Sydney, Australia, August 2008
Webmaster (with H. Mony) FMCAD 2007, Austin, TX, USA, November 2007

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 full member of the Sigma Xi Scientific Research Society.

Personal

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.

Reading: I love to read, as long as what I read is well-written. I will cheerfully read anything under the sun, but I am a particularly voracious reader of Novels, Social writings, Philosophy, History, Evolution, and Science Nonfictions (not necessarily in that order). Here are some books that I highly recommend. Also, for people who like books, Project Gutenberg might be of interest.

Music: I love to listen to music, both Indian and Western. But I do not believe that mere shouting is music. This discrimination sometimes stops me from listening to certain songs that I do not want to qualify or discuss. I am completely ignorant of classical grammar of songs, Indian or western, and hence classical music is not quite in my palate though once in a blue moon I do get in the mood for Bach, Mozart, or Indian classical. I mostly listen to soft rock western music and similar Indian songs, where the words provide more meaning. My favorites in Western music are Joan Baez, Leonard Cohen, Judy Collins, Bob Dylan, Pink Floyd, Norah Jones, Richard Thompson, and Neil Young. Among Indian music, I like Rabindrasangeet, Jiban-mukhi Bengali songs (Mohiner Ghoraguli, Mousumi Bhowmik, Suman Chattopadhyay, or Anjan Dutta, in that order), and Ghazals (Ghulam Ali and Jagjit Singh). Among instrumental music, I love the percussion of the tabla, and the melody of the flute.

Food: I love food, as is obvious to anybody who has seen me in person. I make no discrimination on the ethnicity or nationality of food, as long as it tastes good. Very recently I have also picked up an interest in cooking. It sure feels good when a dish you cook is appreciated (by yourself or someone else).

Travel: I love to travel. I tend to travel to places of scenic interest. Having grown up in a big city, I am not a big fan of going to another big city on excursion (although I do get in that mood on occasions). I also like to go for cross-country road trips along desolate highways, which I find to be a great way of relieving stress. The United States provide a great opportunity for road trips, and I try to take one at least once a year. My US travel destinations typically tend to be the national parks. I have also visited some places in Europe, such as the Bavarian Alps and the Scottish Highlands. I plan put up my pictures and travel logs when I get the time, which does not seem to be forthcoming.

Art: I do not have background in art, but I love Escher for the mathematics in his art. And I guess almost everybody has been deeply impacted at some time or the other (if they had given themselves half the chance) by surrealism and Salvador Dali.

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.