SAGAR  JYOTI  CHAKI

Home	Office
5700 Bunkerhill Street, Apt. 1005	Wean Hall 4212
Pittsburgh, PA - 15206-1166, USA	Carnegie Mellon University
Phone: +1 (412) 661-1030	Pittsburgh, PA - 15213, USA
email: chaki+@cs.cmu.edu	Phone: +1 (412) 268-5942
URL: http://www.cs.cmu.edu/~chaki	Fax: +1 (412) 268-5576

Objective: Full-time industrial or academic researcher position.

Research Interests:

• Formal methods
• Specification, verification, analysis and testing of software
• Concurrency and software security
• Publish-subscribe systems

Education:

Carnegie Mellon University (CMU) Pittsburgh, USA	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	1999 - present
Indian Institute of Technology (IIT) Kharagpur, India	B.Tech.(Hons.), Computer 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: http://www.cs.cmu.edu/~chaki/magic.

• SPEAR project at CMU (December 1999 - present) Developed and implemented algorithms for efficient matching in publish-subscribe systems using Binary Decision Diagrams (BDDs). Details and download at: http://www.cs.cmu.edu/~chaki/spear.

• Summer Intern at Microsoft Research (MSR) (May 2001 - July 2001) 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 a CCS 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 concurrent Boolean programs. Implemented a tool, BEACON, for verifying safety properties of thread-safe libraries and used it to verify critical safety properties of a thread-safe memory manager developed at MSR.

• Computer Architecture Project at CMU (October 1999 - November 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 http://www.cs.cmu.edu/~chaki/740proj.

• B.Tech. Dissertation at IIT (July 1997 - April 1998) Developed 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) Developed 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 of C; 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 Management Utility using Lotus Notes to maintain a database of hardware and software problems faced by TCS, their solutions and other details.

Invited Talks:

• Vulnerability Analysis Branch, US Department of Defense, November 21, 2003.
• Microsoft Research, February 6, 2003.

Awards and Honors:

• 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, June 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.

Development Skills:

• OS: Unix and variants, Windows (Win32), MS DOS development.
• Languages: C, C++, Lex, Yacc, Java, Ocaml, Promela, Verilog, SQL, Fortran 77, HTML, and MIPS / Alpha / x86 assembly.
• Development: Verification using CUDD; programmable logic and micro-controller based logic design; development of parallel programs using threads; development of network applications using Berkeley sockets; GUI development using X-Motif.

Publications: (Details and download at http://www.cs.cmu.edu/~chaki/academics).

Refereed Journal Papers

• Modular Verification of Software Components in C, to appear as invited article in special issue of Transactions on Software Engineering (TSE), Sagar Chaki, Edmund Clarke, Alex Groce, Somesh Jha, Helmut Veith.

• 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.

Refereed Conference and Workshop Papers

• 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 the 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 Software Engineering and Knowledge Engineering (SEKE) 2003, Sagar Chaki, Pascal Fenkam, Harald Gall, Somesh Jha, Engin Kirda, Helmut Veith.

• Modular Verification of Software Components in C, an ACM-SIGSOFT 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 K. Rajamani.

• Efficient Filtering in Publish-Subscribe Systems using Binary Decision Diagrams, in Proc. of the 23rd International Conference on Software Engineering (ICSE) 2001, Alexis Campailla, Sagar Chaki, Edmund Clarke, Somesh Jha, Helmut Veith.

• Abstractions for Model Checking of Event Timings, in Proc. of IEEE International Symposium on Circuits and Systems (ISCAS) 2001, Jatindra K. Deka, S. Chaki, Pallab Dasgupta, P. P. Chakrabarti.

Languages: Fluent English, native Bengali speaker.

Personal Interests: Hindi and Bengali music, playing cricket, reading novels, puzzle solving.

References:

• Prof. Edmund M. Clarke, Carnegie Mellon University, USA, email: emc@cs.cmu.edu.
• Dr. Sriram Rajamani, Microsoft Research, USA, email: sriram@microsoft.com.
• Dr. Thomas Ball, Microsoft Research, USA, email: tball@microsoft.com.
• Prof. Randal E. Bryant, Carnegie Mellon University, USA, email: bryant@cs.cmu.edu.

Others available upon request.