Pritam Roy, PhD

Over 8 years of experience in research, development and maintenance of Formal Verification algorithms and tools. Good communication and writing skills.

Operating Systems : Unix/Linux, Windows, Mac-OSX

Languages : C, Lex, Yacc, Perl, Verilog, Matlab, Simulink,C++, Python, Java, Ocaml, C#

Tools : CUDD, GLU, FSoft, CIL, SMV, YICES,PRISM

2004-2009 PhD in Computer Engineering, University of California, Santa Cruz, USA.

Topic : Verification of large systems using abstraction-refinement algorithms.

2002-2004 M.S. in Computer Science and Engineering, IIT, Kharagpur, India,

Topic : Development of Open-CTL Module Verifier and Stimulus Generation Tool

1998- 2002 B.Tech (Hons.) in Computer Science and Engineering, IIT Kharagpur, India,

Topic : Mobile Hand-off and Channel Allocation Algorithm

Jan 2010-Present    Postdoctoral Researcher, Cyber-Physical Lab, UCLA

• Controller Synthesis via Game-theoretic Algorithms.
• Developed and implemented efficient, scalable algorithms to synthesize the controllers, implemented symbolic algorithms for the tool Pessoa.
• Developed algorithms to synthesize the controllers with respect to  safe-Linear Temporal Logic  specifications
• Applied SPLAT test-generation tool to create test-cases on the source code of Toyota engine controller

2004 – 2009 Graduate Researcher, UCSC

• explored new algorithms for scalable verification techniques for non-probabilistic and probabilistic systems.
• applied two-player game-semantics to model the interactions among components as interface theory
• developed symbolic algorithms for compatibility, and refinement, and implemented the algorithms in the tool TICC.
• developed the wrapper from Ocaml to C BDD/MDD functions (CUDD, GLU).
• developed a novel symbolic three-valued abstraction algorithm to solve  transition systems and two-player games with reachability or safety goals.
• Implemented three-valued abstraction algorithms in the tool TICC to show significant space savings as well as speedup
• developed a novel abstraction technique, called magnifying-lens abstraction (MLA), to  analyse reachability and safety properties of MDPs.
• prototyped a python implementation to show that MLA can provide accurate answers, with savings in memory .
• provided a symbolic version of algorithm MLA that combines the symbolic techniques with the abstraction techniques to handle the space-explosion problem better.
• developed, implement, and test a symbolic version (called SMLA) inside PRISM model checker.

July 2009-Sept 2009

Summer Intern, SRI International, USA

• Developed a tool that type-checks, verifies, generates tests for Simulink designs.
• Modeled the tele-surgery robot  M7 in Simulink/Matlab for the purpose of certification
• The type-checker accepts expressive types such as measurement units as types, dependent types, and refinement-types.
• Used SMT Solver YICES.

June 2007-Sept 2007

Summer Intern, NEC Research Lab, USA,

• Developed algorithms to verify C library functions by summarizing functions via creating an interface (function call graph)
• Computed an interface graph to specify the safe (not leading the library to error) calls in the library.
• applied purely modular approach to create the interface graphs.
• developed and implemented symbolic abstraction-refinement based algorithms by summarizing every function in a purely modular approach.
• used the software model checking tool FSoft, CIL

June 2005-Sept 2005, May 2007

Summer Intern, MSR Research, Redmond, USA,

• Developed algorithms to maximize the software testing coverage in online testing in XRT, and Spec Explorer.
• implemented novel online-testing algorithms based on Reinforcement Learning in Spec-Explorer and XRT tools
• developed algorithms to maximize the software testing coverage given the number of runs and number of steps in the online testing.
• Developed probabilistic learning algorithms in NModel open source tool.

Aug 2002- Aug 2004

Research Assistant, IIT Kharagpur, India,

• Developed a BDD-based Open-RTCTL model checker with BLIF/ISCAS front-end.
• Used LEX/YACC to parse hardware circuits, CUDD package for BDD manipulation
• worked on sequential automatic test-pattern generation (ATPG) for hardware circuits
• directed test-bench generation of hardware designs by assertion-based verification techniques.
• extended the basic philosophy of the Open family of temporal logics to develop a language Stimulus Generation Logic (SGL) for annotating specific behavioral properties with input constraints
• used model checking algorithms to generate sequential input stimuli that satisfy the properties given in SGL.
• implemented those algorithms in the Stimulus Generation Tool (SGT)

May 2001- July 2001

Summer Intern, Dortmund University, Germany,

• Compiler Optimization Tool for LANCE Embedded Processor,
• Worked on optimization of the LANCE compiler project.
• Developed and tested code optimization techniques for embedded processors.

• NFM 2010, SimCheck: An Expressive Type System for Simulink, with N. Shankar.
• QEST 2008. Symbolic Magnifying Lens Abstraction in Markov Decision Processes, with D.Parker, G. Norman, L. deAlfaro.
• RTSS 2007, Adapting Futures: Scalability for Real-World Computing, with J. Helander, R.Serg, M. Veanes.
• CONCUR07, Solving Games via Three-Valued Abstraction Refinement, with L. deAlfaro.
• CAV07, Magnifying-Lens Abstraction for Markov Decision Processes, with L. de Alfaro.
• FATES/RV 06, Online Testing with Reinforcement Learning, with M. Veanes, C. Campbell.
• CAV06, TICC: A Tool for Interface Compatibility and Composition, with B. Adler, L.de Alfaro, L. Dias Da Silva, M. Faella, A. Legay, V.Raman.
• IWAOM05, Behavioral Composition in Symbolic Domains, with W. Grieskamp, N. Kicillof, C. Campbell, W. Schulte, N. Tillman, M. Veanes.
• FROCOS05,Sociable Interfaces, with L.de Alfaro, L. Dias Da Silva, M. Faella, A. Legay,M. Sorea
• VDAT04,An Assertion Based Language for Generating Test Sequences for Complex Temporal Behavior, with P.Dasgupta, P.P. Chakrabarti.

• SimCheck : Developer and maintainer of Simulink Type-checker tool
• SPLAT : Developer and maintainer of SPLAT test-case generation tool for C
• Pessoa : Developer of the safe-LTL controller synthesis
• TICC : Developer and maintainer of the game-based interface composition and compatibility tool.
• Stimulus Generator : Developer of the input generator of the hardware circuits with respect to temporal assertions.
• OpenCTL Model Checker: Developer of the model checker for Open-Computation Tree Logic
• NModel : Developer of the open-source project NModel for maximization of coverage in model-based software testing.

• Model Checking : Formal methods for hardware/software verification
• Testing : Formal methods to create test-suites (offline/online), Model-based Testing
• 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