Monday, October 21, 2013 - 1:00pm to 1:50pm
KEC 3057

Speaker Information

Sagar Chaki
Senior Member, Technical Staff
Software Engineering Institute
Carnegie Mellon University


Abstract: In this talk, I will present recent developments in our ongoing research on verifying periodic programs -- a commonly used form of real-time software that consists of a set of asynchronous tasks running periodically and being scheduled preemptively based on their priorities. We focus on an approach based on sequentialization -- reducing the verification of a time-bounded periodic program to that of an equivalent sequential program. We present a new compositional form of sequentialization that improves on earlier work in terms of both scalability and completeness (i.e., false warnings) by leveraging temporal separation between jobs in the same hyper-period and across multiple hyper-periods. We also show how the new sequentialization can be further improved in the case of harmonic systems to generate sequential programs of asymptotically smaller size. Experiments indicate that our new sequentialization improves verification time by orders of magnitude compared to competing schemes. This is joint work with Arie Gurfinkel, Soonho Kong, and Ofer Strichman. Further details of our project are available at:

Speaker Bio

Sagar Chaki is a senior Member of Technical Staff at the Software Engineering Institute at Carnegie Mellon University. He received a B.Tech in Computer Science & Engineering from the Indian Institute of Technology, Kharagpur in 1999, and a Ph.D. in Computer Science from Carnegie Mellon University in 2005. These days, he works mainly on model checking software for real-time and cyber-physical systems, but he is generally interested in rigorous and automated approaches for improving software quality. He has developed several automated software verification tools, including two model checkers for C programs, MAGIC and Copper. He has co-authored over 50 peer reviewed publications. More details about Sagar and his current work can be found at