Software Engineering Institute | Carnegie Mellon University
Software Engineering Institute | Carnegie Mellon University

Digital Library

Sagar Chaki
March 2017 - Podcast Verifying Distributed Adaptive Real-Time Systems

In this podcast, James Edmondson and Sagar Chaki describe an architecture and approach to engineering high-assurance software for Distributed Adaptive Real-Time (DART) systems.

February 2017 - Video Assuring Autonomous Software

Authors: Sagar Chaki

Watch Sagar Chaki in this SEI Cyber Minute as he discusses "Assuring Autonomous Software".

January 2017 - Conference Paper Certifiable Runtime Assurance of Distributed Real-Time Systems

Topics: Software Assurance

This paper presents two challenge problems guiding research on developing a provably correct approach for runtime assurance of distributed real-time embedded systems.

December 2016 - White Paper Cyber-Physical Systems

Topics: Cyber-Physical Systems

Cyber-physical systems (CPS) integrate computational algorithms and physical components. SEI promotes efficient development of high-confidence, distributed CPS.

December 2016 - White Paper Predictability by Construction

Topics: Process Improvement

Predictability by construction (PBC) makes the behavior of a component-based system predictable before implementation, based on known properties of components.

November 2016 - Presentation Verifying DART Systems

This work is producing validated assurance techniques for distributed adaptive real-time (DART) systems

November 2016 - Presentation Auto-Active Verification of Software with Timers and Clocks

Software that accesses the system clock is the key to real-time and cyber-physical systems

October 2016 - Poster Auto-Active Verification of Software with Timers and Clocks

Authors: Sagar Chaki

Formally verify STACs at the source code level using deductive (aka auto-active) verification

October 2016 - Poster Verifying Distributed Adaptive Real (DART) Systems

Authors: Sagar Chaki

DART Vision

October 2016 - Conference Paper Contract-Based Verification of Timing Enforcers

In this paper, the authors focus on proving the correctness of the budget enforcement that guarantees that no task τi executes beyond its W1 i. They present their approach and some preliminary results.

October 2016 - Conference Paper Modeling, Verifying, and Generating Software for Distributed Cyber-Physical Systems using DMPL and AADL.

Topics: Cyber-Physical Systems

This paper provides an end-to-end framework where DART systems can be designed, analyzed, and implemented within the same toolchain. In this talk, the authors present this toolchain and demonstrate it on a few representative examples.

October 2016 - Conference Paper Verifying Cyber-Physical Systems by Combining Software Model Checking with Hybrid Systems Reachability

This work proposes a bridge between two important verification methods, software model checking and hybrid systems reachability.

September 2016 - Conference Paper Input Attribution for Statistical Model Checking using Logistic Regression

In this conference paper, the authors describe an approach to Statistical Model Checking (SMC). This paper is part of the Lecture Notes in Computer Science book series.

June 2016 - Technical Report DMPL: Programming and Verifying Distributed Mixed-Synchrony and Mixed-Critical Software

Topics: Cyber-Physical Systems

DMPL is a language for programming distributed real-time, mixed-criticality software. It supports distributed systems in which each node executes a set of periodic real-time threads that are scheduled by priority and criticality.

December 2015 - Conference Paper Model Checking with Multi-threaded IC3 Portfolios

This paper presents three variants of multi-threaded IC3s for model checking hardware, differing by degree of synchronization and aggressiveness of proof checking.

November 2015 - Presentation Engineering High-Assurance Software for Distributed Adaptive Real-Time Systems

This presentation describes an evidence-based approach for producing high-assurance DART software involving multiple layers of the CPS stack.

October 2015 - Poster Verifying Distributed Adaptive Real-Time (DART) Systems Poster (SEI 2015 Research Review)

This poster describes the authors' research efforts in verifying distributed adaptive real-time systems.

October 2015 - Presentation Verifying Distributed Adaptive Real-Time (DART) Systems

This 2015 Research Review presentation describes the authors' research efforts in verifying distributed adaptive real-time systems.

October 2015 - Presentation Parallel Software Model Checking

Authors: Sagar Chaki

In this 2015 Research Review presentation, the author describes his research efforts into scaling up software model checking—a fundamental challenge in the field.

September 2015 - Conference Paper High Assurance for Distributed Cyber Physical Systems

This short paper introduces our architecture and approach to engineering a DART system so that we achieve high assurance in its runtime behavior against a set of formally specified requirements.

October 2014 - Article Supervised Learning for Provenance-Similarity of Binaries

Topics: Malware Analysis

In this article, the authors present a notion of similarity based on provenance; two binaries are similar if they are compiled from the same source code with the same compilers.

October 2014 - Article Binary Function Clustering using Semantic Hashes

Topics: Malware Analysis

In this article, the authors present an alternative to pair wise comparisons based on "hashing” that captures the semantics of functions as semantic hashes.

October 2014 - Article Recovering C++ Objects From Binaries Using Inter-Procedural Data-Flow Analysis

Topics: Malware Analysis

In this article, the authors present a static approach that uses symbolic execution and inter-procedural data flow analysis to discover object instances, data members, and methods of a common class.

July 2013 - Conference Paper Probabilistic Verification of Coordinated Multi-Robot Missions

Topics: Cyber-Physical Systems

In this paper, the authors advocate, formalize, and empirically justify an approach to compute quantitative utility of robotic missions using probabilistic model checking.

May 2013 - Conference Paper Towards a Quantitative Method for Assuring Coordinated Autonomy

This article introduces a reliability engineering assurance approach based on probabilistic model checking.

August 2012 - Technical Report Results of SEI Line-Funded Exploratory New Starts Projects

This report describes the line-funded exploratory new starts (LENS) projects that were undertaken during fiscal year 2011. For each project, the report presents a brief description and a recounting of the research that was done, as well as a synopsis of the results of the project.

December 2011 - Special Report Standards-Based Automated Remediation: A Remediation Manager Reference Implementation, 2011 Update

Topics: Acquisition Support

In this report, the authors describe work to develop standards for automated remediation of vulnerabilities and compliance issues on DoD networked systems.

October 2011 - Presentation Time-Bounded Analysis of Real-Time Systems

Topics: Cyber-Physical Systems

This presentation considers the problem of verifying functional correctness of periodic Real-Time Embedded Software (RTES), a popular variant of RTES that execute periodic tasks in an order determined by Rate Monotonic Scheduling (RMS).

July 2011 - Special Report Standards-Based Automated Remediation: A Remediation Manager Reference Implementation

Topics: Acquisition Support

In this report, the authors describe work to develop standards for vulnerability and compliance remediation on DoD networked systems.

August 2010 - Technical Report COVERT: A Framework for Finding Buffer Overflows in C Programs via Software Verification

Topics: Software Architecture

In this report, the authors present COVERT, an automated framework for finding buffer overflows in C programs using software verification tools and techniques.

October 2007 - Presentation Model-Driven Construction of Certified Binaries

Sagar Chaki and others describe in this presentation an implementation of the approach that targets the Pin component technology, and presents experimental results on a collection of benchmarks.

September 2007 - Technical Report Certified Binaries for Software Components

Topics: Software Assurance

In this report, the authors present an approach to certify binary code against expressive policies to achieve the benefits of PCC and CMC.

April 2007 - White Paper Copper Manual, Tutorial, and Specification Grammar

Authors: Sagar Chaki

Copper is a software model checker for concurrent message-passing C programs.

March 2007 - Conference Paper Optimized L*-Based Assume-Guarantee Reasoning

Paper from the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2007.

September 2006 - Technical Note Assume-Guarantee Reasoning for Deadlock

This report shows how L^F can be used for compositional regular failure language containment and deadlock detection, using non-circular and circular assume-guarantee rules.

September 2006 - Technical Note Certifying the Absence of Buffer Overflows

Topics: Software Assurance

In this report, the authors present a technique for certifying the safety of buffer manipulations in C programs.

February 2006 - Technical Note SAT-Based Software Certification

Authors: Sagar Chaki

This 2006 report presents a technique that uses proofs to certify software.

December 2005 - White Paper Precise Buffer Overflow Detection via Model Checking

In this paper, the authors present an automated overflow detection technique based on model checking and iterative refinement.

December 2005 - Technical Report Verification of Evolving Software via Component Substitutability Analysis

Topics: Software Architecture

This 2005 report describes the application of the SEI Architecture Tradeoff Analysis Method (ATAM) to the U.S. Army's Warfighter Information Network-Tactical (WIN-T) system.

December 2005 - Technical Report Results of SEI Independent Research and Development Projects and Report on Emerging Technologies and Technology Trends (FY2005)

This report describes the IR&D projects that were conducted during fiscal year 2005 (October 2004 through September 2005). In addition, this report provides information on what the SEI has learned in its role as a technology scout for developments over the past year in the field of software engineering.

August 2005 - Presentation The ComFoRT Reasoning Framework

Presented: August 2005

July 2005 - White Paper The ComFoRT Reasoning Framework

Model checking is a promising technology for verifying critical behavior of software. However, software model checking is hamstrung by scalability issues and is difficult for software engineers to use directly. ComFoRT addresses both of these challenges.

October 2004 - White Paper Predicate Abstraction with Minimum Predicates

Predicate abstraction is a popular abstraction technique employed in formal software verification. Experiments show that predicate minimization can result in a significant reduction of both verification time and memory usage compared to earlier methods.