Sagar Chaki's Andrew Homepage

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

• Decision Diagrams for Linear Arithmetic
• Verifying Information Flow Control Over Unbounded Processes
• 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