Academics

HOME

Research Interests

My primary research interest is in Formal Methods.In particular I am interested in combining techniques like Static Analysis , Type Checking , Theorem Proving and Model Checking for reasoning about correctness of systems. I am especially interested in verifying systems that involve interaction between a number of concurrent components.
I am also interested in Publish-Subscribe Systems and Parallel and Distributed Computing .

Thesis

Defense

I defended my thesis on Wednesday, January 26, 2005 at 9:30 AM (EST) in Newell Simon Hall 1507. Here is an abstract, a short summary, the defense presentation and the final version of my thesis.

Proposal

I gave my thesis proposal talk on Monday, December 9, 2002 at 2:00 PM (EST) in Wean Hall 4615A. Here is the proposal abstract in HTML and text formats. The formal writeup is also available in postscript and pdf formats.

Projects

MAGIC aims at verifying software components written in C.

SPEAR is a set of software libraries for developing robust and efficient Publish-Subscribe systems.

Publications

Journal

Modular Verification of Software Components in C, Transactions on Software Engineering (TSE), Volume 30, Number 6, pages 388-402, June 2004, Sagar Chaki, Edmund Clarke, Alex Groce, Somesh Jha, Helmut Veith. © IEEE, 2004. This is the author's version of the work. It is posted here by permission of IEEE for your personal use. Not for redistribution ( ps ps.gz pdf ).

Efficient Verification of Sequential and Concurrent C Programs, Formal Methods in System Design (FMSD),Volume 25, Issue 2-3, pages 129-166, September-November 2004, Sagar Chaki, Edmund Clarke, Alex Groce, Joel Ouaknine, Ofer Strichman, Karen Yorav. © Springer, 2004. This is the author's version of the work. It is posted here by permission of Springer for your personal use. Not for redistribution ( ps ps.gz pdf ).

Conference

Explaining Abstract Counterexamples, 12th International Symposium on Foundations of Software Engineering (FSE) 2004, Sagar Chaki, Alex Groce, Ofer Strichman, ( ps ps.gz pdf ). This paper describes a technique for explaining the cause behind counterexamples obtained by model checking predicate abstractions of C programs.

Automated, compositional and iterative deadlock detection, Second ACM-IEEE International Conference on Formal Methods and models for Codesign (MEMOCODE) 2004, Sagar Chaki, Edmund Clarke, Joel Ouaknine, Natasha Sharygina, ( ps ps.gz pdf ).

State/Event-based Software Model Checking, Fourth International Conference on Integrated Formal Methods (IFM) 2004, LNCS 2999, pages 128-147, Sagar Chaki, Edmund Clarke, Joel Ouaknine, Natasha Sharygina, Nishant Sinha, ( ps ps.gz pdf ). This is revised and extended version of our workshop publication with the same title.

Predicate Abstraction with Minimum Predicates, 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME) 2003, LNCS 2860, pages 19-34, Sagar Chaki, Edmund Clarke, Alex Groce, Ofer Strichman, ( ps ps.gz pdf ).

Integrating Publish/Subscribe into a Mobile Teamwork Support Platform, 15th International Conference on Software Engineering and Knowledge Engineering (SEKE) 2003, Sagar Chaki, Pascal Fenkam, Harald Gall, Somesh Jha, Engin Kirda, Helmut Veith, ( ps ps.gz pdf ).

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, ( ps ps.gz pdf ). Revised and extended version appeared as invited article in a special issue ofTransactions on Software Engineering (TSE) (see above).

Types as Models: Model Checking Message Passing Programs, 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) 2002 , pages 45-57, Sagar Chaki, Sriram K. Rajamani, Jakob Rehof, ( ps ps.gz pdf MSR-TR ).

Parameterized Verification of Multithreaded Software Libraries, 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2001 , LNCS 2031, pages 158-173, Thomas Ball, Sagar Chaki, Sriram K. Rajamani, ( ps ps.gz pdf MSR-TR ).

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

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

Workshop

State/Event-based Software Model Checking, Workshop on State-oriented vs. Event-oriented thinking in Requirements Analysis, Formal Specification and Software Engineering (ST.EVE) 2003 , Sagar Chaki, Joel Ouaknine, Natasha Sharygina, Nishant Sinha, ( ps ps.gz pdf ).

Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach, 2nd Workshop on Software Model Checking (SoftMC) 2003, ENTCS 89(3), Boulder, Colorado, July 2003, Sagar Chaki, Joel Ouaknine, Karen Yorav, Edmund Clarke, ( ps ps.gz pdf ).

Technical Report

An Expressive Verification Framework for State/Event Systems, Technical report # CMU-CS-04-145, Computer Science Department, School of Computer Science, Carnegie Mellon University, Sagar Chaki, Edmund Clarke, Orna Grumberg, Joel Ouaknine, Natasha Sharygina, Tayssir Touili, Helmut Veith, ( ps pdf ).

Summer '00 and '01 at MSR

I had two great summer internship experiences at Microsoft Research, Redmond in 2000 and 2001. I was involved with the SLAM and Behave! projects, both of which are being led by members of the Software Productivity Tools group.