Academics

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

Back to Top

Back to Top

• MAGIC aims at verifying software components written in C.
  

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

Back to Top

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 of Transactions 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 ).
  

Back to Top

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.

Back to Top

Current Activities

• Focusing on research.
• Theorem Proving and Model Checking in PVS

Back to Top