Sagar Chaki's Homepage

Projects

• I am co-leading two Independent Research & Development (IRAD) projects at the SEI:
  • Learning a Portfolio-Based Checker for Provenance-Similarity of Binaries. Here's a blog post on our work. Here's another.
  • Regression Verification of Real-time Embedded Software. Here's a blog post on our work.
• I am also involved with work on Linear Decision Diagrams.

Publications

Journal

• Automated assume-guarantee reasoning for omega-regular systems and specifications (ISSE'11)
• Combining predicate and numeric abstraction for software model checking (STTT'10)
• Software model checking without source code (ISSE'10)
• Verification of Evolving Software via Component Substitutability Analysis (FMSD'08)
• Three Optimizations for Assume-Guarantee Reasoning with L* (FMSD'08)
• Concurrent Software Verification with States, Events, and Deadlocks (FACJ'05)
• An Iterative Framework for Simulation Conformance (JLC'05)
• Error Explanation with Distance Metrics (STTT'05)

Conference, Symposium

• Parametric Verification of Address Space Separation (POST'12)
• Regression Verification for Multi-Threaded Programs (VMCAI'12)
• Time-Bounded Analysis of Real-Time Systems (FMCAD'11)
• Supervised Learning for Provenance-Similarity of Binaries (KDD'11)
• Efficient Predicate Abstraction of Program Summaries (NFM'11)
• BOXES: A Symbolic Abstract Domain of Boxes (SAS'10)
• Automated Assume-Guarantee Reasoning for Omega-Regular Systems and Specifications (NFM'10)
• Scalable Parametric Verification of Secure Systems: How to Verify Reference Monitors without Worrying about Data Structure Size (Oakland'10)
• Using Architecturally Significant Requirements for Guiding System Evolution (CSMR'10)
• Decision Diagrams for Linear Arithmetic (FMCAD'09)
• Verifying Information Flow Control Over Unbounded Processes (FM'09)
• ASPIER: An Automated Framework for Verifying Security Protocol Implementations (CSF'09)
• Software Model Checking without Source Code (NFM'09)
• Combining Predicate and Numeric Abstraction for Software Model Checking (FMCAD'08)
• Model-Driven Construction of Certified Binaries (MODELS'07)
• Verification Across Intellectual Property Boundaries (CAV'07)
• Optimized L*-based Assume-Guarantee Reasoning (TACAS'07)
• Assume-Guarantee Reasoning for Deadlock (FMCAD'06)
• SAT-Based Software Certification (TACAS'06)
• Verifying Concurrent Message-Passing C Programs with Recursive Calls (TACAS'06)
• State/Event Software Verification for Branching-Time Specifications (IFM'05)
• Dynamic Component Substitutability Analysis (FM'05)
• The ComFoRT Reasoning Framework (CAV'05)
• Automated Assume-Guarantee Reasoning for Simulation Conformance (CAV'05)

Workshop

• Presentation Only: Efficient Predicate Abstraction of Program Summaries (SMT'11)
• Non-Preemptive Fixed-Priority Uniprocessor Scheduling where the Execution Time of a Job Depends on the Scheduling of Jobs that Executed Before it (RTSOPS'11)
• Formal Verification of Real-Time Embedded Software for Multicore Platforms (AVICPS'10)
• Assurance Cases for Proofs as Evidence (PCC'09)
• Towards Engineered Architecture Evolution (MISE'09)
• Combining Predicate and Numeric Abstraction for Software Model Checking (LFM'08)
• Parallel Assignments in Software Model Checking (SVV'05)

Report, Note, Whitepaper

• COVERT: A Framework for Finding Buffer Overflows in C Programs via Software Verification (2010)
• ASPIER: An Automated Framework for Verifying Security Protocol Implementations (2008)
• Automated Verification of Security Protocol Implementations (2008)
• Certified Binaries for Software Components (2007)
• Results of SEI Independent Research and Development Projects (2007)
• Assume-Guarantee Reasoning for Deadlock (2006)
• Certifying the Absence of Buffer Overflows (2006)
• SAT-Based Software Certification (2006)
• Results of SEI Independent Research and Development Projects and Report on Emerging Technologies and Technology Trends (2005)
• Verification of Evolving Software via Component Substitutability Analysis (2005)
• Precise Buffer Overflow Detection via Model Checking (2005)
• Learning Doubly Labeled Automata using Queries and Counterexamples (2005)

Previous Publications     Ph.D. thesis