Back to Top
- 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
- I am also interested in Publish-Subscribe
Systems and Parallel and
Distributed Computing .
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.
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.
aims at verifying software components
written in C.
is a set of software libraries for developing robust and efficient
- 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
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 ).
- 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 ).
- An Expressive Verification
Framework for State/Event Systems, Technical report # CMU-CS-04-145,
Computer Science Department, School of Computer Science, Carnegie
University, Sagar Chaki, Edmund Clarke, Orna Grumberg, Joel
Ouaknine, Natasha Sharygina, Tayssir Touili, Helmut Veith, ( ps
Summer '00 and '01 at MSR