industrial or academic
- Formal methods
- Specification, verification, analysis and testing of software
- Concurrency and software security
- Publish-subscribe systems
|Ph.D., Computer Science
Dissertation topic: A counterexample guided abstraction
refinement framework for verifying concurrent C programs
Adviser: Prof. Edmund M. Clarke
Microsoft Graduate Student Fellow
of Technology (IIT)
Science & Engineering
Dissertation: Symbolic and automata-theoretic model
checking for timed abstraction of Verilog descriptions.
Advisers: Prof. P. P. Chakrabarti & Prof. P. Dasgupta
GPA: 9.82/10, President of India Gold Medal
|1995 - 1999
Professional and research experience:
- MAGIC project at CMU (December 2001 - present) Developed a
framework for automated and compositional verification of concurrent C
programs. Basis of my Ph.D. dissertation. Details and download at:
- SPEAR project at CMU (December 1999 - present) Developed
implemented algorithms for efficient matching in publish-subscribe
systems using Binary Decision Diagrams (BDDs). Details and download
- Summer Intern at Microsoft Research (MSR) (May 2001 - July
Worked in the Software Productivity Tools (SPT) group on type-based
model extraction and verification of concurrent -Calculus
programs. Implemented a tool, PIPER, that (i) extracts
model from a -Calculus
program using user-supplied annotations,
(ii) translates the CCS model to Promela and (iii) verifies it using
the SPIN model checker.
- Summer Intern at MSR (May 2000 - July 2000) Worked in the SLAM
project (SPT group) on the verification of
Boolean programs. Implemented a tool, BEACON, for
safety properties of thread-safe libraries and used it to verify
critical safety properties of a thread-safe memory manager developed
- Computer Architecture Project at CMU (October 1999 -
1999) Worked on a technique for hiding load latencies using previous
register values in modern superscalar processors. Simulations done
using the Simplescalar toolkit indicated considerable
performance gains for Spec95 benchmarks. Project report at
- B.Tech. Dissertation at IIT (July 1997 - April 1998)
symbolic model checker using the CUDD BDD package to verify timed
properties of Verilog descriptions of systems.
- Design Lab project at IIT (January 1999 - April 1999)
C++ libraries similar to Parallel Virtual Machine (PVM) to support
distributed applications on a network of workstations.
- Other Projects at IIT (1995 - 1999) Compiler for a subset
hardware implementation of a 4-bit CPU; hardware/firmware for a real
time object counter; design and implementation of a time division
multiplexer; development of a graphical editor using X-Motif etc.
- Summer Intern at Tata Consultancy Services (TCS), Calcutta,
India. (May 1998 - July 1998) Developed web-based Problem
Utility using Lotus Notes to maintain a database of hardware and
software problems faced by TCS, their solutions and other details.
Awards and Honors:
- Vulnerability Analysis Branch, US Department of Defense, November
- Microsoft Research, February 6, 2003.
- Microsoft Graduate Fellowship, 2001-2003.
- Carnegie Mellon Computer Science Departmental Fellowship, Sep
1999 to present.
- President of India Gold Medal at IIT for best academic
performance in batch.
- President of India Silver Medal at IIT for best academic
performance in department.
- Jagadis Bose National Science Talent Search (JBNSTS) scholarship,
1995 to June 1999
- B. P. Poddar Merit Scholarship, July 1998 to April 1999.
- Annual awards at IIT for best academic performance in the batch.
- OS: Unix and variants, Windows (Win32), MS DOS development.
- Languages: C, C++, Lex, Yacc, Java, Ocaml, Promela,
Fortran 77, HTML, and MIPS / Alpha / x86 assembly.
- Development: Verification using CUDD; programmable logic
micro-controller based logic design; development of parallel programs
using threads; development of network applications using Berkeley
sockets; GUI development using X-Motif.
(Details and download at
Refereed Journal Papers
- Modular Verification of Software Components in C, to appear
invited article in special issue of Transactions on Software
Engineering (TSE), Sagar Chaki, Edmund Clarke, Alex Groce,
Jha, Helmut Veith.
Refereed Conference and Workshop Papers
- Efficient Verification of Sequential and Concurrent C Programs, to
appear in special issue of Formal Methods in System Design (FMSD),
Sagar Chaki, Edmund Clarke, Alex Groce, Jöel Ouaknine, Ofer
Strichman, Karen Yorav.
- Automated, compositional and iterative deadlock detection, to
appear in the Second ACM-IEEE International Conference on Formal
Methods and models for Codesign (MEMOCODE) 2004, Sagar Chaki,
Edmund Clarke, Jöel Ouaknine, Natasha Sharygina.
- State/Event-based Software Model Checking, to appear in the
Fourth International Conference on Integrated Formal Methods (IFM)
2004, Sagar Chaki, Edmund Clarke, Jöel Ouaknine, Natasha
Sharygina, Nishant Sinha.
- Predicate Abstraction with Minimum Predicates, in Proc. of
12th Advanced Research Working Conference on Correct Hardware Design
and Verification Methods (CHARME) 2003, Sagar Chaki, Edmund
Clarke, Alex Groce, Ofer Strichman.
- Automated Compositional Abstraction Refinement for Concurrent C
Programs: A Two-Level Approach, in Proc. of the 2nd Workshop on
Software Model Checking (SoftMC) 2003, Sagar Chaki, Jöel
Ouaknine, Karen Yorav, Edmund Clarke.
- Integrating Publish/Subscribe into a Mobile Teamwork Support
Platform, in Proc. of the 15th International Conference on
Engineering and Knowledge Engineering (SEKE) 2003, Sagar
Pascal Fenkam, Harald Gall, Somesh Jha, Engin Kirda, Helmut Veith.
- Modular Verification of Software Components in C, an
Distinguished Paper in the 25th International Conference on Software
Engineering (ICSE) 2003, pages 385-395, Sagar Chaki, Edmund
Clarke, Alex Groce, Somesh Jha, Helmut Veith.
- Types as Models: Model Checking Message Passing Programs, in
Proc. of the 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of
Programming Languages (POPL) 2002, Sagar Chaki, Sriram
K. Rajamani, Jakob Rehof.
- Parameterized Verification of Multithreaded Software Libraries, in
Proc. of Tools and Algorithms for the Construction and Analysis of
Systems (TACAS) 2001, Thomas Ball, Sagar Chaki, Sriram
- Efficient Filtering in Publish-Subscribe Systems using Binary
Diagrams, in Proc. of the 23rd International Conference on
Software Engineering (ICSE) 2001, Alexis Campailla, Sagar
Edmund Clarke, Somesh Jha, Helmut Veith.
- Abstractions for Model Checking of Event Timings, in Proc.
IEEE International Symposium on Circuits and Systems (ISCAS) 2001,
Jatindra K. Deka, S. Chaki, Pallab Dasgupta, P. P. Chakrabarti.
Fluent English, native
Hindi and Bengali music,
playing cricket, reading novels, puzzle solving.
- Prof. Edmund M. Clarke, Carnegie Mellon University, USA, email: email@example.com.
- Dr. Sriram Rajamani, Microsoft Research, USA, email: firstname.lastname@example.org.
- Dr. Thomas Ball, Microsoft Research, USA, email: email@example.com.
- Prof. Randal E. Bryant, Carnegie Mellon University, USA, email: firstname.lastname@example.org.
Others available upon request.