Sagar Chaki
Software Engineering Institute
Publications by Sagar Chaki
-
Verifying Distributed Adaptive Real-Time Systems
March 27, 2017 • Podcast
Sagar ChakiJames Edmondson
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.
learn more -
Assuring Autonomous Software
February 23, 2017 • Video
Sagar Chaki
Watch Sagar Chaki in this SEI Cyber Minute as he discusses "Assuring Autonomous Software".
watch -
Certifiable Runtime Assurance of Distributed Real-Time Systems
January 13, 2017 • Conference Paper
Sagar ChakiDionisio de Niz
This paper presents two challenge problems guiding research on developing a provably correct approach for runtime assurance of distributed real-time embedded systems.
read -
Cyber-Physical Systems
December 01, 2016 • White Paper
Björn AndersonSagar ChakiDionisio de Niz
Cyber-physical systems (CPS) integrate computational algorithms and physical components. SEI promotes efficient development of high-confidence, distributed CPS.
read -
Predictability by Construction
December 01, 2016 • White Paper
Sagar ChakiScott HissamGabriel Moreno
Predictability by construction (PBC) makes the behavior of a component-based system predictable before implementation, based on known properties of components.
read -
Verifying DART Systems
November 01, 2016 • Presentation
Sagar ChakiDionisio de Niz
This work is producing validated assurance techniques for distributed adaptive real-time (DART) systems
read -
Auto-Active Verification of Software with Timers and Clocks
November 01, 2016 • Presentation
Sagar ChakiDionisio de Niz
Software that accesses the system clock is the key to real-time and cyber-physical systems
read -
Auto-Active Verification of Software with Timers and Clocks
October 18, 2016 • Poster
Sagar Chaki
Formally verify STACs at the source code level using deductive (aka auto-active) verification
read -
Verifying Distributed Adaptive Real (DART) Systems
October 18, 2016 • Poster
Sagar Chaki
DART Vision
read -
Contract-Based Verification of Timing Enforcers
October 07, 2016 • Conference Paper
Sagar ChakiDionisio de Niz
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.
read -
Modeling, Verifying, and Generating Software for Distributed Cyber-Physical Systems using DMPL and AADL.
October 06, 2016 • Conference Paper
Sagar ChakiDionisio de NizJoe Seibel
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.
read -
Verifying Cyber-Physical Systems by Combining Software Model Checking with Hybrid Systems Reachability
October 01, 2016 • Conference Paper
Stanley Bak (Air Force Resarch Laboratory)Sagar Chaki
This work proposes a bridge between two important verification methods, software model checking and hybrid systems reachability.
read -
Input Attribution for Statistical Model Checking using Logistic Regression
September 20, 2016 • Conference Paper
Jeffrey HansenSagar ChakiScott Hissam
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.
read -
DMPL: Programming and Verifying Distributed Mixed-Synchrony and Mixed-Critical Software
June 21, 2016 • Technical Report
Sagar ChakiDavid Kyle
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.
read -
Model Checking with Multi-threaded IC3 Portfolios
December 25, 2015 • Conference Paper
Sagar ChakiDerrick Karimi
This paper presents three variants of multi-threaded IC3s for model checking hardware, differing by degree of synchronization and aggressiveness of proof checking.
read -
Engineering High-Assurance Software for Distributed Adaptive Real-Time Systems
November 18, 2015 • Presentation
Mark H. KleinSagar ChakiDionisio de Niz
This presentation describes an evidence-based approach for producing high-assurance DART software involving multiple layers of the CPS stack.
read -
Verifying Distributed Adaptive Real-Time (DART) Systems Poster (SEI 2015 Research Review)
October 22, 2015 • Poster
Sagar ChakiDionisio de Niz
This poster describes the authors' research efforts in verifying distributed adaptive real-time systems.
read -
Verifying Distributed Adaptive Real-Time (DART) Systems
October 16, 2015 • Presentation
Sagar ChakiDionisio de Niz
This 2015 Research Review presentation describes the authors' research efforts in verifying distributed adaptive real-time systems.
read -
Parallel Software Model Checking
October 16, 2015 • Presentation
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.
read -
High Assurance for Distributed Cyber Physical Systems
September 07, 2015 • Conference Paper
Scott HissamSagar ChakiGabriel Moreno
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.
read -
Supervised Learning for Provenance-Similarity of Binaries
October 28, 2014 • Article
Sagar ChakiCory CohenArie Gurfinkel
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.
read -
Binary Function Clustering using Semantic Hashes
October 28, 2014 • Article
Wesley JinSagar ChakiCory Cohen
In this article, the authors present an alternative to pair wise comparisons based on "hashing” that captures the semantics of functions as semantic hashes.
read -
Recovering C++ Objects From Binaries Using Inter-Procedural Data-Flow Analysis
October 28, 2014 • Article
Wesley JinCory CohenJeff Gennari
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.
read -
Probabilistic Verification of Coordinated Multi-Robot Missions
July 08, 2013 • Conference Paper
Sagar ChakiJohn M. DolanJoseph Giampapa
In this paper, the authors advocate, formalize, and empirically justify an approach to compute quantitative utility of robotic missions using probabilistic model checking.
read -
Results of SEI Line-Funded Exploratory New Starts Projects: FY 2012
July 01, 2013 • Technical Report
Bjorn AnderssonLori FlynnDavid P. Gluch
This report describes line-funded exploratory new starts (LENS) projects that were conducted during fiscal year 2012 (October 2011 through September 2012).
read -
Towards a Quantitative Method for Assuring Coordinated Autonomy
May 06, 2013 • Conference Paper
Sagar ChakiJoseph Giampapa
This article introduces a reliability engineering assurance approach based on probabilistic model checking.
read -
Results of SEI Line-Funded Exploratory New Starts Projects
August 01, 2012 • Technical Report
Len BassRick KazmanEdwin J. Morris
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.
read -
Standards-Based Automated Remediation: A Remediation Manager Reference Implementation, 2011 Update
December 01, 2011 • Special Report
Sagar ChakiRita C. CreelJeff Davenport
In this report, the authors describe work to develop standards for automated remediation of vulnerabilities and compliance issues on DoD networked systems.
read -
Time-Bounded Analysis of Real-Time Systems
October 31, 2011 • Presentation
Sagar ChakiArie GurfinkelSoonho Kong
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).
read -
Standards-Based Automated Remediation: A Remediation Manager Reference Implementation
July 01, 2011 • Special Report
Sagar ChakiRita C. CreelJeff Davenport
In this report, the authors describe work to develop standards for vulnerability and compliance remediation on DoD networked systems.
read -
COVERT: A Framework for Finding Buffer Overflows in C Programs via Software Verification
August 01, 2010 • Technical Report
Sagar ChakiArie Gurfinkel
In this report, the authors present COVERT, an automated framework for finding buffer overflows in C programs using software verification tools and techniques.
read -
Model-Driven Construction of Certified Binaries
October 05, 2007 • Presentation
Sagar ChakiJames IversPeter Lee
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.
read -
Certified Binaries for Software Components
September 01, 2007 • Technical Report
Sagar ChakiJames IversPeter Lee
In this report, the authors present an approach to certify binary code against expressive policies to achieve the benefits of PCC and CMC.
read -
Results of SEI Independent Research and Development Projects (FY 2006)
July 01, 2007 • Technical Report
Christopher J. AlbertsEileen C. ForresterSuzanne Garcia-Miller
This report describes the IRAD projects that were conducted during fiscal year 2006 (October 2005 through September 2006).
read -
Copper Manual, Tutorial, and Specification Grammar
April 01, 2007 • White Paper
Sagar Chaki
Copper is a software model checker for concurrent message-passing C programs.
read -
Optimized L*-Based Assume-Guarantee Reasoning
March 01, 2007 • Conference Paper
Sagar ChakiOfer Strichman
Paper from the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2007.
read -
Assume-Guarantee Reasoning for Deadlock
September 01, 2006 • Technical Note
Sagar ChakiNishant Sinha
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.
read -
Certifying the Absence of Buffer Overflows
September 01, 2006 • Technical Note
Sagar ChakiScott Hissam
In this report, the authors present a technique for certifying the safety of buffer manipulations in C programs.
read -
SAT-Based Software Certification
February 01, 2006 • Technical Note
Sagar Chaki
This 2006 report presents a technique that uses proofs to certify software.
read -
Precise Buffer Overflow Detection via Model Checking
December 01, 2005 • White Paper
Sagar ChakiScott Hissam
In this paper, the authors present an automated overflow detection technique based on model checking and iterative refinement.
read -
Verification of Evolving Software via Component Substitutability Analysis
December 01, 2005 • Technical Report
Sagar ChakiEdmund ClarkeNatasha Sharygina
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.
read -
Results of SEI Independent Research and Development Projects and Report on Emerging Technologies and Technology Trends (FY2005)
December 01, 2005 • Technical Report
Rosann W. CollinsRick KazmanRichard C. Linger (Oak Ridge National Laboratory)
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.
read -
The ComFoRT Reasoning Framework
August 10, 2005 • Presentation
Sagar ChakiJames IversNatasha Sharygina
Presented: August 2005
read -
The ComFoRT Reasoning Framework
July 01, 2005 • White Paper
Sagar ChakiJames IversNatasha Sharygina
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.
read -
Predicate Abstraction with Minimum Predicates
October 01, 2004 • White Paper
Sagar ChakiEdmund Clarke
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.
read