skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.


Search for: All records

Award ID contains: 2043104

Note: When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external site maintained by the publisher. Some full text articles may not yet be available without a charge during the embargo (administrative interval).
What is a DOI Number?

Some links on this page may take you to non-federal websites. Their policies may differ from this site.

  1. Abstract Invariant relations are used to analyze while loops; while their primary application is to derive the function of a loop, they can also be used to derive loop invariants, weakest preconditions, strongest postconditions, sufficient conditions of correctness, necessary conditions of correctness, and termination conditions of loops. In this paper we present two generic invariant relations that capture the semantics of loops whose loop body applies affine transformations on numeric variables. 
    more » « less
  2. Free, publicly-accessible full text available February 24, 2026
  3. Context. Several Research areas emerged and have been proceeding independently when in fact they have much in common. These include: mutant subsumption and mutant set minimization; relative correctness and the semantic definition of faults; differentiator sets and their application to test diversity; generate-and--validate methods of program repair; test suite coverage metrics. Objective. Highlight their analogies, commonalities and overlaps; explore their potential for synergy and shared research goals; unify several disparate concepts around a minimal set of artifacts. Method. Introduce and analyze a minimal set of concepts that enable us to model these disparate research efforts, and explore how these models may enable us to share insights between different research directions, and advance their respective goals. Results. Capturing absolute (total and partial) correctness and relative (total and partial) correctness with a single concept: Detector sets. Using the same concept to quantify the effectiveness of test suites, and prove that the proposed measure satisfies appealing monotonicity properties. Using the measure of test suite effectiveness to model mutant set minimization as an optimization problem, characterized by an objective function and a constraint. Generalizing the concept of mutant subsumption using the concept of differentiator sets. Identifying analogies between detector sets and differentiator sets, and inferring relationships between subsumption and relative correctness. Conclusion. This paper does not aim to answer any pressing research question as much as it aims to raise research questions that use the insights gained from one research venue to gain a fresh perspective on a related research issue. mutant subsumption; mutant set minimization; relative correctness; absolute correctness; total correctness; partial correctness; program fault; program repair; differentiator set; detector set. 
    more » « less
    Free, publicly-accessible full text available January 1, 2026
  4. Free, publicly-accessible full text available January 1, 2026
  5. Rhode, Matilda; Simmons, Kent (Ed.)
    Function Extraction (FX) is a new and evolving paradigm for the production of secure computer codes. It is, in effect, the inverse of formal verification as it analyzes code to produce a mathematical specification of its behavior. This has the potential for identifying unwanted or unexpected behaviors and has the potential for analyzing unknown or “found” code artifacts such as malware. The effort is enabled by recent developments in loop analysis that allow invariant relations to be developed for loop bodies enabling the loop function to be discovered. The paper defines program behavior as a mathematical description of the effects of program execution on the environment in which the program runs and continues with a discussion of its current status. As FX is an evolving paradigm, areas in which work remains to be done are discussed and examples of the results of two prototype analyzers are given. The paper concludes with a discussion of the path forward and the work that remains to be done. 
    more » « less
  6. Ghosh, Sudipto; Troubitsyna, Elena; Chen, Zhenyu (Ed.)
    When we quantify the effectiveness of a test suite by its mutation coverage, we are in fact equating test suite effectiveness with fault detection: to the extent that mutations are faithful proxies of actual faults, it is sensible to consider that the effectiveness of a test suite to kill mutants reflects its ability to detect faults. But there is another way to measure the effectiveness of a test suite: by its ability to expose the failures of an incorrect program. The relationship between failures and faults is tenuous at best: a fault is the adjudged or hypothesized cause of a failure. The same failure may be attributed to more than one fault. This raises the question: what is the relationship between detecting faults and exposing failures. In this paper, we discuss an empirical experiment in which we explore this relationship. 
    more » « less
  7. Several metrics have been proposed in the past to quantify the effectiveness of a test suite; they are usually based on some measure of coverage because it is sensible to quantify the effectiveness of a test suite by the extent to which it exercises (covers) various syntactic features of the program under test. Though no coverage metric has emerged as the gold standard of test suite effectiveness, mutation coverage is widely perceived as a reliable measure of test suite effectiveness because the ability of a test suite to detect program mutations can be used as an indication of its ability to detect actual faults. In this paper we aim to challenge the superiority of mutation coverage, by showing that the same test suite may have vastly different values of mutation coverage depending on the mutation operators that are used in the estimation. 
    more » « less
  8. Since the dawn of programming, several developments in programming language design and programming methodology have been hailed as the end of the profession of programmer; they have all proven to be exaggerated rumors, to echo the words of Mark Twain. In this paper we ponder the question of whether the emergence of large language models finally realizes these prophecies. 
    more » « less