Welcome to my home! Thank you for visiting my homepage. I am working as a Post Doctoral Researcher at University of California, Los Angeles with Rupak Majumdar and Paolo Tabuada. Before that, I have completed my Ph.D. studies under the supervision of Dr. Luca de Alfaro.

I spent the summer of 2009 in SRI International where my mentor was Natarajan Shankar.

I spent the summer of 2007 in NEC Research Lab, USA where my mentor was Chao Wang . I spent the summer of 2005 in Foundations of Software Engineering (FSE) group at Microsoft Research Lab, Redmond, USA where my mentor was Margus Veanes .

I did my undergraduate studies from Computer Science and Engineering at Indian Institue of Technology, Kharagpur. After that I joined for M.S. Program in CS, where my thesis advisor was Dr. Pallab Dasgupta and Dr. P.P. Chakrabarti. I was a part of Formal Verification group at IIT-KGP from 2002-04.

R & D Interests

  • Model Checking : Formal methods for hardware/software verification
  • Testing : Formal methods to create test-suites (offline/online), Model-based Testing
  • Controller Synthesis : Correct-by-construction controller Synthesis
  • Scalable verification techniques as abstraction-refinement,
  • Symbolic Data Structures : BDD/MDD/SMT-based symbolic algorithm
  • Game Theory : Application of Game theory to hardware and software systems
  • Probabilistic System : Solving practical verification problems Markov chains and MDPs
  • Embedded Systems : Interface theory for component based design, and verification

 

Publications

Journal

  • L. deAlfaro, P.Roy. Solving Games via Three-Valued Abstraction Refinement. Information and Computation Journal (Concur 2007 version) PDF

Technical Reports

  • Pritam Roy, Paulo Tabuada, Rupak Majumdar.Safety-Guarantee Controller Synthesis for Cyber-Physical Systems. arXiv:1010.5665v1 [cs.LO] PDF

  • P. Roy. Interface Building for Software by Modular Three-Valued Abstraction Refinement. Technical report : UCSC-SOE-08-19, School of Engineering, University of California, Santa Cruz, 2008. PDF

  • P. Roy, D. Parker, G. Norman, L. deAlfaro. Symbolic Magnifying Lens Abstraction in Markov Decision Processes. Technical report : UCSC-SOE-08-05, School of Engineering, University of California, Santa Cruz, 2008.PDF

  • L. de Alfaro, P. Roy. Magnifying-Lens Abstraction for Markov Decision Processes.Technical report : ucsc-crl-06-15, School of Engineering, University of California, Santa Cruz, 2006. Postscript

Conferences

  • P. Roy and N. Shankar. SimCheck: An Expressive Type System for Simulink. Accepted for 2nd NASA Formal Methods Symposium (NFM 2010), Washington D.C., USA PDF

  • P. Roy, D. Parker, G. Norman, L. deAlfaro. Symbolic Magnifying Lens Abstraction in Markov Decision Processes. Accepted in QEST 2008 at Saint Malo, France. PDF

  • J. Helander, R. Serg, M.Veanes and P. Roy. Adapting Futures: Scalability for Real-World Computing. RTSS 2007 in Tuscon, Arizona, USA PDF

  • L. deAlfaro, P.Roy. Solving Games via Three-Valued Abstraction Refinement.CONCUR 2007 in Lisbon, Portugal PDF

  • L. de Alfaro, P. Roy. Magnifying-Lens Abstraction for Markov Decision Processes. Computer Aided Verification (CAV07) in Berlin, Germany.PDF Technical report : ucsc-crl-06-15, School of Engineering, University of California, Santa Cruz, 2006. Postscript

  • Margus Veanes, Pritam Roy and Colin Campbell, "Online Testing with Reinforcement Learning", in Formal Approaches to Testing and Runtime Verification (FATES/RV06), Seattle, August 15 - 16, 2006, pp. 240-253 PDF

  • B. Thomas Adler, L. de Alfaro, L. Dias Da Silva, M. Faella, A. Legay, V. Raman, P. Roy, "Ticc: A Tool for Interface Compatibility and Composition", in Computer Aided Verification (CAV06) in Seattle, WA, pp 59-62.

  • Wolfgang Grieskamp, Nicolas Kicillof, Colin Campbell, Pritam Roy, Wolfram Schulte, Nikolai Tillman, Margus Veanes , "Behavioral Composition in Symbolic Domains", 7th International Workshop on Aspect-Oriented Modeling - 2005. PDF

  • L.de Alfaro, L. Dias Da Silva, M. Faella, A. Legay, P. Roy, M. Sorea. Sociable Interfaces. In FROCOS 2005: 5th International Workshop on Frontiers of Combining Systems, LNAI 3717, Springer-Verlag, 2005. PDF

  • Roy, P., Dasgupta, P., Chakrabarti, P.P., "An assertion Based Language for Generating Test Sequences for Complex Temporal Behavior", in 8-th VLSI Design and Test Workshop (VDAT 2004) in Mysore, India, August 2004, pp. 482-491. PDF