SEARCH · Engineering Papers

Results for “symbolic execution”

Search indexed NASA NTRS and DOE OSTI research on propulsion, heat transfer, battery materials and energy systems. Follow report and document links to the original sources.

SourceResearch connectionFrom yearThrough year

Quote a phrase for an exact phrase match. Source license links do not imply unrestricted reuse.

At least 37 records · Page 2

All sources NASA NTRS DOE OSTI

NASA NTRS2007

Model Checker for Java Programs

Java Pathfinder (JPF) is a verification and testing environment for Java that integrates model checking, program analysis, and testing. JPF consists of a custom-made Java Virtual Machine (JVM) that interprets bytecode, combined with a search interface to allow the complete behavior of a Java program to be analyzed, including interleavings of concurrent programs. JPF is implemented in Java, and its architecture is highly modular to support rapid prototyping of new features. JPF is an explicit-state model checker, because it enumerates all visited states and, therefore, suffers from the state-explosion problem inherent in analyzing large programs. It is suited to analyzing programs less than 10kLOC, but has been successfully applied to finding errors in concurrent programs up to 100kLOC. When an error is found, a trace from the initial state to the error is produced to guide the debugging. JPF works at the bytecode level, meaning that all of Java can be model-checked. By default, the software checks for all runtime errors (uncaught exceptions), assertions violations (supports Java s assert), and deadlocks. JPF uses garbage collection and symmetry reductions of the heap during model checking to reduce state-explosion, as well as dynamic partial order reductions to lower the number of interleavings analyzed. JPF is capable of symbolic execution of Java programs, including symbolic execution of complex data such as linked lists and trees. JPF is extensible as it allows for the creation of listeners that can subscribe to events during searches. The creation of dedicated code to be executed in place of regular classes is supported and allows users to easily handle native calls and to improve the efficiency of the analysis.

Visser, Willem↗

NASA NTRS2011

Automated Test Case Generation for an Autopilot Requirement Prototype

Designing safety-critical automation with robust human interaction is a difficult task that is susceptible to a number of known Human-Automation Interaction (HAI) vulnerabilities. It is therefore essential to develop automated tools that provide support both in the design and rapid evaluation of such automation. The Automation Design and Evaluation Prototyping Toolset (ADEPT) enables the rapid development of an executable specification for automation behavior and user interaction. ADEPT supports a number of analysis capabilities, thus enabling the detection of HAI vulnerabilities early in the design process, when modifications are less costly. In this paper, we advocate the introduction of a new capability to model-based prototyping tools such as ADEPT. The new capability is based on symbolic execution that allows us to automatically generate quality test suites based on the system design. Symbolic execution is used to generate both user input and test oracles user input drives the testing of the system implementation, and test oracles ensure that the system behaves as designed. We present early results in the context of a component in the Autopilot system modeled in ADEPT, and discuss the challenges of test case generation in the HAI domain.

Giannakopoulou, Dimitra↗

NASA NTRS2012

A Change Impact Analysis to Characterize Evolving Program Behaviors

Change impact analysis techniques estimate the potential effects of changes made to software. Directed Incremental Symbolic Execution (DiSE) is an intraprocedural technique for characterizing the impact of software changes on program behaviors. DiSE first estimates the impact of the changes on the source code using program slicing techniques, and then uses the impact sets to guide symbolic execution to generate path conditions that characterize impacted program behaviors. DiSE, however, cannot reason about the flow of impact between methods and will fail to generate path conditions for certain impacted program behaviors. In this work, we present iDiSE, an extension to DiSE that performs an interprocedural analysis. iDiSE combines static and dynamic calling context information to efficiently generate impacted program behaviors across calling contexts. Information about impacted program behaviors is useful for testing, verification, and debugging of evolving programs. We present a case-study of our implementation of the iDiSE algorithm to demonstrate its efficiency at computing impacted program behaviors. Traditional notions of coverage are insufficient for characterizing the testing efforts used to validate evolving program behaviors because they do not take into account the impact of changes to the code. In this work we present novel definitions of impacted coverage metrics that are useful for evaluating the testing effort required to test evolving programs. We then describe how the notions of impacted coverage can be used to configure techniques such as DiSE and iDiSE in order to support regression testing related tasks. We also discuss how DiSE and iDiSE can be configured for debugging finding the root cause of errors introduced by changes made to the code. In our empirical evaluation we demonstrate that the configurations of DiSE and iDiSE can be used to support various software maintenance tasks

Rungta, Neha Shyam↗

NASA NTRS2009

jFuzz: A Concolic Whitebox Fuzzer for Java

We present jFuzz, a automatic testing tool for Java programs. jFuzz is a concolic whitebox fuzzer, built on the NASA Java PathFinder, an explicit-state Java model checker, and a framework for developing reliability and analysis tools for Java. Starting from a seed input, jFuzz automatically and systematically generates inputs that exercise new program paths. jFuzz uses a combination of concrete and symbolic execution, and constraint solving. Time spent on solving constraints can be significant. We implemented several well-known optimizations and name-independent caching, which aggressively normalizes the constraints to reduce the number of calls to the constraint solver. We present preliminary results due to the optimizations, and demonstrate the effectiveness of jFuzz in creating good test inputs. The source code of jFuzz is available as part of the NASA Java PathFinder. jFuzz is intended to be a research testbed for investigating new testing and analysis techniques based on concrete and symbolic execution. The source code of jFuzz is available as part of the NASA Java PathFinder.

Jayaraman, Karthick↗

NASA NTRS2014

Compositional Solution Space Quantification for Probabilistic Software Analysis

Probabilistic software analysis aims at quantifying how likely a target event is to occur during program execution. Current approaches rely on symbolic execution to identify the conditions to reach the target event and try to quantify the fraction of the input domain satisfying these conditions. Precise quantification is usually limited to linear constraints, while only approximate solutions can be provided in general through statistical approaches. However, statistical approaches may fail to converge to an acceptable accuracy within a reasonable time. We present a compositional statistical approach for the efficient quantification of solution spaces for arbitrarily complex constraints over bounded floating-point domains. The approach leverages interval constraint propagation to improve the accuracy of the estimation by focusing the sampling on the regions of the input domain containing the sought solutions. Preliminary experiments show significant improvement on previous approaches both in results accuracy and analysis time.

Monte Carlo Methods↗

NASA NTRS2001

Automatic Overset Grid Generation with Heuristic Feedback Control

An advancing front grid generation system for structured Overset grids is presented which automatically modifies Overset structured surface grids and control lines until user-specified grid qualities are achieved. The system is demonstrated on two examples: the first refines a space shuttle fuselage control line until global truncation error is achieved; the second advances, from control lines, the space shuttle orbiter fuselage top and fuselage side surface grids until proper overlap is achieved. Surface grids are generated in minutes for complex geometries. The system is implemented as a heuristic feedback control (HFC) expert system which iteratively modifies the input specifications for Overset control line and surface grids. It is developed as an extension of modern control theory, production rules systems and subsumption architectures. The methodology provides benefits over the full knowledge lifecycle of an expert system for knowledge acquisition, knowledge representation, and knowledge execution. The vector/matrix framework of modern control theory systematically acquires and represents expert system knowledge. Missing matrix elements imply missing expert knowledge. The execution of the expert system knowledge is performed through symbolic execution of the matrix algebra equations of modern control theory. The dot product operation of matrix algebra is generalized for heuristic symbolic terms. Constant time execution is guaranteed.

Robinson, Peter I.↗

NASA NTRSDate not supplied

NEUROSPF: A Tool For the Symbolic Analysis of Neural Networks

This paper presents NEUROSPF, a tool for the symbolic analysis of neural networks. Given a trained neural network model, the tool extracts the architecture and model parameters and translates them into a Java representation that is amenable for analysis using the Symbolic PathFinder symbolic execution tool. Notably, NEUROSPF encodes specialized peer classes for parsing the model’s parameters, thereby enabling efficient analysis. With NEUROSPF the user has the flexibility to specify either the inputs or the network internal parameters as symbolic, promoting the application of program analysis and testing approaches from software engineering to the field of machine learning. For instance, NEUROSPF can be used for coverage-based testing and test generation, finding adversarial examples and also constraint-based repair of neural networks, thus improving the reliability of neural networks and of the applications that use them.

neural networks↗

NASA NTRS2015

A Flexible and Non-instrusive Approach for Computing Complex Structural Coverage Metrics

Software analysis tools and techniques often leverage structural code coverage information to reason about the dynamic behavior of software. Existing techniques instrument the code with the required structural obligations and then monitor the execution of the compiled code to report coverage. Instrumentation based approaches often incur considerable runtime overhead for complex structural coverage metrics such as Modified Condition/Decision (MC/DC). Code instrumentation, in general, has to be approached with great care to ensure it does not modify the behavior of the original code. Furthermore, instrumented code cannot be used in conjunction with other analyses that reason about the structure and semantics of the code under test. In this work, we introduce a non-intrusive preprocessing approach for computing structural coverage information. It uses a static partial evaluation of the decisions in the source code and a source-to-bytecode mapping to generate the information necessary to efficiently track structural coverage metrics during execution. Our technique is flexible; the results of the preprocessing can be used by a variety of coverage-driven software analysis tasks, including automated analyses that are not possible for instrumented code. Experimental results in the context of symbolic execution show the efficiency and flexibility of our nonintrusive approach for computing code coverage information

DO-178C↗

NASA NTRS2015

Environment Modeling Using Runtime Values for JPF-Android

Software applications are developed to be executed in a specific environment. This environment includes external native libraries to add functionality to the application and drivers to fire the application execution. For testing and verification, the environment of an application is simplified abstracted using models or stubs. Empty stubs, returning default values, are simple to generate automatically, but they do not perform well when the application expects specific return values. Symbolic execution is used to find input parameters for drivers and return values for library stubs, but it struggles to detect the values of complex objects. In this work-in-progress paper, we explore an approach to generate drivers and stubs based on values collected during runtime instead of using default values. Entry-points and methods that need to be modeled are instrumented to log their parameters and return values. The instrumented applications are then executed using a driver and instrumented libraries. The values collected during runtime are used to generate driver and stub values on- the-fly that improve coverage during verification by enabling the execution of code that previously crashed or was missed. We are implementing this approach to improve the environment model of JPF-Android, our model checking and analysis tool for Android applications.

Verification↗

DOE OSTI2024

Toward Automated Detection of Portability Bugs in Kokkos Parallel Programs

Performance-portable programming frameworks provide abstractions for parallel execution to allow easily porting an application to multiple backend programming models, such as CUDA, HIP, and OpenMP. However, programs may still have portability bugs that manifest only on specific backends. Traditional testing is ineffective in discovering these bugs, as it would require concrete execution on all supported hardware configurations for a potentially infinite set of inputs. To mitigate this issue, we focused on a specific programming framework, Kokkos, and identified several categories of common portability bugs. We then developed Klokkos, a static analysis approach based on symbolic execution that can run on commodity hardware, before execution on supercomputers. As a proof-of-concept, we ran Klokkos on examples encoding the identified bugs. Our results show that Klokkos is effective, efficient, and precise: it detected all the considered bugs, quickly, and without any false positives. Although preliminary, our results motivate further research and development in this direction.

Kale, Vivek↗

NASA NTRS2013

Maintaining the Health of Software Monitors

Software health management (SWHM) techniques complement the rigorous verification and validation processes that are applied to safety-critical systems prior to their deployment. These techniques are used to monitor deployed software in its execution environment, serving as the last line of defense against the effects of a critical fault. SWHM monitors use information from the specification and implementation of the monitored software to detect violations, predict possible failures, and help the system recover from faults. Changes to the monitored software, such as adding new functionality or fixing defects, therefore, have the potential to impact the correctness of both the monitored software and the SWHM monitor. In this work, we describe how the results of a software change impact analysis technique, Directed Incremental Symbolic Execution (DiSE), can be applied to monitored software to identify the potential impact of the changes on the SWHM monitor software. The results of DiSE can then be used by other analysis techniques, e.g., testing, debugging, to help preserve and improve the integrity of the SWHM monitor as the monitored software evolves.

Runtime Monitor↗

DOE OSTI2025

Speeding-up fuzzing through directional seeds

Abstract Fuzzing is an automated process for discovering inputs in a program that may trigger unexpected behavior. Today, fuzzing has become a standard practice for the discovery of bugs and security vulnerabilities. However, the main issue with such practices is that the exploration of the input space of programs can often be prohibitively expensive. Therefore, several alternative fuzzing strategies have been introduced during the last few years. Some fuzzing techniques rely on human expertise to provide a plausible set of initial input examples, namely, seeds. However, the process of handcrafting seeds for fuzzing purposes often becomes strenuous for humans as it requires a deeper understanding of the Program-Under-Test (PUT). Also, the use of known inputs to programs often does not trigger vulnerable program behavior or may not reach potentially vulnerable code locations. To address those issues, we propose a seed generation framework that enables Human-In-The-Loop (HITL) directed fuzzing where the human assumes a more active role in the creation of seeds that can penetrate and assess desired locations of the PUT. Our proposed framework uses Symbolic Execution (SE) to generate seeds that exercise paths to target program locations. Moreover, our framework enables the visualization of the explored execution paths in the binary of the PUT for the generated seeds. We evaluated our approach on a set of 12 carefully designed C programs with diverse characteristics that mimic real-world programs. The experimental results show the effectiveness of the proposed approach in improving the performance of standard fuzzing tools such as the American Fuzzy Lop ("Image missing" <#comment/> ). Specifically, our solution can generate seeds that substantially enhance the performance of the fuzzer, achieving speedups ranging from $$1.46\times $$ 1.46 × to $$68.53\times $$ 68.53 × for branch conditions, $$1.39\times $$ 1.39 × to $$254.62\times $$ 254.62 × for branch depths, $$14,879.59\times $$ 14 , 879.59 × to $$30,295.88\times $$ 30 , 295.88 × for branch widths over traditional seeds. Additionally, the speedup increases with the number of target function ranging from $$12,260\times $$ 12 , 260 × to $$22,856.07\times $$ 22 , 856.07 × over traditional seeds while only requiring less than 15 seconds on average for the seed generation step.

97 MATHEMATICS AND COMPUTING↗

DOE OSTI2025

Towards Automated Reasoning Chains for Verification of LLM-Generated Scientific Code

With the rise of Large Language Model (LLM) generated code, including in domains like scientific computing, ensuring not only syntactical, but also mathematical correctness, has become a critical task. Traditional formal methods approaches often struggle with the ambiguity of floating-point code, and full symbolic execution is extremely costly and limited. We propose a chain-of-reasoning approach that iteratively lifts basic semantics from code into the SPIRAL system and then establishes numerical equivalency to the desired mathematical operation. Here, we leverage the ample mathematical knowledge already formalized in SPIRAL to enable the system to recognize not just different implementations of the same algorithm but fully separate approaches to solving the given problem. The chain establishes tight error bounds on the output of given code with respect to the true continuous solution it approximates, quantifying all sources of error. We demonstrate this approach by establishing the correctness of a pseudospectral solver for a simple 1-dimensional Poisson problem.

Oschatz, Quentin [Carnegie Mellon University,Pitts↗

DOE OSTI2024

Shorter function summaries for finite state machine-based high consequence systems using logic synthesis and tautologies (Final Report LDRD 24-1302)

Computer programs are often viewed as collections of functions – each function has parameters (inputs) and computes a return value, and each has potential side effects that modify program state (outputs). In this research, a Sandia symbolic execution tool designed to support “human-in-the-loop” analysis was modified to automatically create “function summaries,” and a new tool, “diaboolical,” was created to support enhancing readability of the summary using a novel approach to bit-vector simplification that leverages logic synthesis and tautologies. For this effort, students at Auburn University created several finite state machines (FSMs) to serve as exemplars for high-consequence systems. Function summaries for each of the machines were obtained, and then portions of the summaries were simplified using both diaboolical and the simplification procedure of a popular SMT solver. A comparison of the results shows that diaboolical can often produce smaller function summaries, with expression length improvements over the unsimplified function summaries ranging from 0% to 90% for diaboolical and 0% to 65% for the SMT solver, though diaboolical had a significantly greater cost in time. Diaboolical was evaluated against a collection of “arbitrary” C-code as well as FSM exemplars, and for both datasets it achieved an approximately 10% improvement in expression length compared to simplifications that could be obtained using existing techniques. Function summaries can assist assurance efforts that evaluate existing systems and their executable code. A smaller function summary is likely easier for humans to understand and could thus increase the ability and efficacy of assurance practices centered around the analysis of executable artifacts.

97 MATHEMATICS AND COMPUTING↗

NASA NTRS1978

Using tools for verification, documentation and testing

Methodologies are discussed on four of the major approaches to program upgrading -- namely dynamic testing, symbolic execution, formal verification and static analysis. The different patterns of strengths, weaknesses and applications of these approaches are shown. It is demonstrated that these patterns are in many ways complementary, offering the hope that they can be coordinated and unified into a single comprehensive program testing and verification system capable of performing a diverse and useful variety of error detection, verification and documentation functions.

Osterweil, L. J.↗

NASA NTRS1982

Automated verification of flight software. User's manual

(Automated Verification of Flight Software), a collection of tools for analyzing source programs written in FORTRAN and AED is documented. The quality and the reliability of flight software are improved by: (1) indented listings of source programs, (2) static analysis to detect inconsistencies in the use of variables and parameters, (3) automated documentation, (4) instrumentation of source code, (5) retesting guidance, (6) analysis of assertions, (7) symbolic execution, (8) generation of verification conditions, and (9) simplification of verification conditions. Use of AVFS in the verification of flight software is described.

Saib, S. H.↗

NASA NTRS1983

Integrated verification and testing system (IVTS) for HAL/S programs

The IVTS is a large software system designed to support user-controlled verification analysis and testing activities for programs written in the HAL/S language. The system is composed of a user interface and user command language, analysis tools and an organized data base of host system files. The analysis tools are of four major types: (1) static analysis, (2) symbolic execution, (3) dynamic analysis (testing), and (4) documentation enhancement. The IVTS requires a split HAL/S compiler, divided at the natural separation point between the parser/lexical analyzer phase and the target machine code generator phase. The IVTS uses the internal program form (HALMAT) between these two phases as primary input for the analysis tools. The dynamic analysis component requires some way to 'execute' the object HAL/S program. The execution medium may be an interpretive simulation or an actual host or target machine.

Senn, E. H.↗

NASA NTRS1984

Research in computer science

Several short summaries of the work performed during this reporting period are presented. Topics discussed in this document include: (1) resilient seeded errors via simple techniques; (2) knowledge representation for engineering design; (3) analysis of faults in a multiversion software experiment; (4) implementation of parallel programming environment; (5) symbolic execution of concurrent programs; (6) two computer graphics systems for visualization of pressure distribution and convective density particles; (7) design of a source code management system; (8) vectorizing incomplete conjugate gradient on the Cyber 203/205; (9) extensions of domain testing theory and; (10) performance analyzer for the pisces system.

Ortega, J. M.↗