Staff Page for Sagar Chaki
Contents: Background Education Announcements Activities Publications Contact
Job title: Senior Member of the Technical StaffAdministrative home: Research, Technology, and System Solutions (RTSS) Program
Key responsibilities: Development of tools and techniques that enable the verification and certification of the safety, security and reliability of component-based software systems.
Teams: Architecture Centric Engineering (ACE) initiative
Projects: ComFoRT, Copper, Covert.
Professional Background
Previously, I was a doctoral student at Carnegie Mellon University Computer Science Department where I was involved with the MAGIC and the SPEAR projects. Here is a summary of my academic activities as a graduate student, a list of publications and my Ph.D thesis.
Education
- Ph.D. Carnegie Mellon University, Computer Science
- B.Tech. (Hons.) IIT Kharagpur, Computer Science and Engineering
Announcements
- May '08: PACC Starter Kit version 2.0
released. Information and Download.
- July '07: ComFoRT version 2.0 released. Information and Download as part of the PACC Starter Kit.
- June '07: Copper version 2.0 released. Information and Download.
Professional Activities
- PC: Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), 2008.
- PC: Workshop on Software Verification and Validation (SVV), 2006.
Publications
Journal
- Verification of Evolving Software via Component Substitutability Analysis
- Three Optimizations for Assume-Guarantee Reasoning with L*
- Concurrent Software Verification with States, Events, and Deadlocks
- An Iterative Framework for Simulation Conformance
- Error Explanation with Distance Metrics
Conference
- ASPIER: An Automated Framework for Verifying Security Protocol Implementations
- Software Model Checking without Source Code
- Combining Predicate and Numeric Abstraction for Software Model Checking
- Model-Driven Construction of Certified Binaries
- Verification Across Intellectual Property Boundaries
- Optimized L*-based Assume-Guarantee Reasoning
- Assume-Guarantee Reasoning for Deadlock
- SAT-Based Software Certification
- Verifying Concurrent Message-Passing C Programs with Recursive Calls
- State/Event Software Verification for Branching-Time Specifications
- Dynamic Component Substitutability Analysis
- The ComFoRT Reasoning Framework
- Automated Assume-Guarantee Reasoning for Simulation Conformance
Workshop
- Assurance Cases for Proofs as Evidence
- Towards Engineered Architecture Evolution
- Combining Predicate and Numeric Abstraction for Software Model Checking
- Parallel Assignments in Software Model Checking
Report, Note, Whitepaper
- ASPIER: An Automated Framework for Verifying Security Protocol Implementations
- Automated Verification of Security Protocol Implementations
- Certified Binaries for Software Components
- Results of SEI Independent Research and Development Projects
- Assume-Guarantee Reasoning for Deadlock
- Certifying the Absence of Buffer Overflows
- SAT-Based Software Certification
- Results of SEI Independent Research and Development Projects and Report on Emerging Technologies and Technology Trends
- Verification of Evolving Software via Component Substitutability Analysis
- Precise Buffer Overflow Detection via Model Checking
- Learning Doubly Labeled Automata using Queries and Counterexamples
Previous Publications Ph.D. thesis
Contact Information
Electronic mail address: 
Phone: (412) 268-1436
Fax: (412) 268-5758
Room: 5121