Sagar Chaki

These are organized by the type of venue: Keynote Journal Conference Workshop Other. Within each category, publications are chronological. A more up-to-date list may be available at DBLP. Only papers written while I have been at the SEI are listed here. Available elsewhere are my earlier publications as a student, and my Ph.D. thesis.

• Engineering High-Assurance Software for Distributed Adaptive Real-Time Systems (MVD'16)
• Verification Across Intellectual Property Boundaries (HCSS'16)

• SMT-based model checking for recursive programs (FMSD)
• Regression Verification for Multi-Threaded Programs (With extensions to locks and dynamic thread creation) (FMSD)
• Verification across Intellectual Property Boundaries (TOSEM'13)
• 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)

• High Coverage Concolic Equivalence Checking (DATE'19)
• BDD-Based Symbolic Model Checking (HBMC)
• Have your PI and Eat it Too: Practical Security on a Low-cost Ubiquitous Computing Platform (EUROS&P'18)
• Combining Symbolic Runtime Enforcers for Cyber-Physical Systems (RV'17)
• Formal Verification of a Timing Enforcer Implementation (EMSOFT'17)
• Decision-Making with Cross-Entropy for Self-Adaptation (SEAMS'17)
• Certifiable Runtime Assurance of Distributed Real-Time Systems (Invited) (AIAA SCITECH'17)
• Software Solutions for Distributed Autonomous Multi-Functional Robotics in Space (AIAA SPACE'16)
• Input Attribution for Statistical Model Checking using Logistic Regression (RV'16)
• Verifying Cyber-Physical Systems by Combining Software Model Checking with Hybrid Systems Reachability (EMSOFT'16)
• UberSpark: Enforcing Secure Object Abstractions for Automated Compositional Security Analysis of a Hypervisor (USENIX Security'16)
• BUZZ: Testing Context-Dependent Policies in Stateful Networks (NSDI'16)
• Model Checking with Multi-Threaded IC3 Portfolios (VMCAI'16)
• Statistical Model Checking of Distributed Adaptive Real-Time Software (RV'15)
• Semantic Importance Sampling for Statistical Model Checking (TACAS'15)
• Verification of Real-Time Systems using Statistical Model Checking (AIAA SCITECH'15)
• Efficient Verification of Periodic Programs using Sequential Consistency and Snapshots (FMCAD'14)
• Optimizing Robotic Team Performance with Probabilistic Model Checking (SIMPAR'14)
• Contract-Based Integration of Cyber-Physical Analyses (EMSOFT'14)
• Model-Driven Verifying Compilation of Synchronous Distributed Applications (MODELS'14)
• Toward Parameterized Verification of Synchronous Distributed Applications (SPIN'14)
• SMT-based Model Checking for Recursive Programs (CAV'14)
• Finding errors in Python programs using dynamic symbolic execution (ICTSS'13)
• Verifying Periodic Programs with Priority Inheritance Locks (FMCAD'13)
• Probabilistic Verification of Coordinated Multi-Robot Missions (SPIN'13)
• Automatic Abstraction in SMT-Based Unbounded Software Model Checking (CAV'13)
• Design, Implementation and Verification of an eXtensible and Modular Hypervisor Framework (Oakland'13)
• Compositional Sequentialization of Periodic Programs (VMCAI'13)
• Binary Function Clustering using Semantic Hashes (ICMLA'12)
• Non-Preemptive Scheduling with History-Dependent Execution Time (ECRTS'12)
• Parametric Verification of Address Space Separation (POST'12) [Best paper award nominee]
• 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)

• Contract-Based Verification of Timing Enforcers (HILT'16)
• Modeling, Verifying, and Generating Software for Distributed Cyber-Physical Systems using DMPL and AADL (Abstract Only) (HILT'16)
• Eliminating Inter-Domain Vulnerabilities in Cyber-Physical Systems: An Analysis Contracts Approach (CPS-SPC'15)
• High Assurance for Distributed Cyber Physical Systems (ASDS'15)
• Recovering C++ Objects From Binaries Using Inter-Procedural Data-Flow Analysis (PPREW'14) [Best Paper Award Winner]
• Toward A Quantitative Method for Assuring Coordinated Autonomy (ARMS'13)
• UFO: Verification with Interpolants and Abstract Interpretation (Competition Contribution) (TACAS'13) (Invited Paper)
• 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)

• DMPL: Programming and Verifying Distributed Mixed-Synchrony and Mixed-Critical Software (2016)
• Results of SEI Line-Funded Exploratory New Starts Projects: FY 2012 (2013)
• Results of SEI Line-Funded Exploratory New Starts Projects (2012)
• Parametric Verification of Address Space Separation (2012)
• Standards-Based Automated Remediation: A Remediation Manager Reference Implementation, 2011 Update (2011)
• 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)