Sagar Jyoti Chaki

By Renee James,2014-03-26 16:13
7 views 0
Pittsburgh, USA refinement framework for verifying concurrent C programs Edmund M Clarke, Carnegie Mellon University, USA, email: emc@cscmuedu


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: Phone: +1 (412) 268-5942

    URL: Fax: +1 (412) 268-5576

Citizenship: Indian Visa: F1 (Student)

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


    Carnegie Mellon Ph.D., Computer Science 1999 - present University (CMU) Dissertation topic: A counterexample guided abstraction

    Pittsburgh, USA refinement framework for verifying concurrent C programs.

     Adviser: Prof. Edmund M. Clarke

     Microsoft Graduate Student Fellow

Indian Institute B.Tech. (Hons.), Computer 1995-1999

    of Technology (IIT) Science & Engineering

    Kharagpur, India Dissertation: Symbolic and automata-theoretic model

     checking for timed abstraction of Verilog descriptions.

     Advisers: Prof. P. P. Chakraborti & Prof. P. Dasgupta

     GPA: 9.82/10, President of India Gold Medal

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 and implemented algorithms for efficient

    matching in publish-subscribe systems using Binary Decision Diagrams (BDDs). Details and download at:

     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

     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

    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, Joel 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, Joel 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, Joel 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, Joel 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.


Prof. Edmund M. Clarke, Carnegie Mellon University, USA, email:

     Dr. Sriram Rajamani, Microsoft Research, USA, email:

     Dr. Thomas Ball, Microsoft Research, USA, email:

     Prof. Randal E. Bryant, Carnegie Mellon University, USA, email:

    Others available upon request.

Report this document

For any questions or suggestions please email