Abstract Dynamic Symbolic Execution (DSE) is an important method for the testing of programs. The major advantage of DSE is its path-by-path exploration of the program execution space. However, this often leads to the path explosion problem. To address this issue, a method of abstraction learning has been used. The key step here is the computation of an interpolant to represent the learned abstraction. In Test-Comp 2024, we use two different approaches of interpolant generation viz., Deletion Interpolation and Weakest Precondition Interpolation. The former is our more stable and mature system and briefly discussed in [8]. In this paper, we present the latter approach which is the heart of TracerX. In general, the Weakest Precondition (WP) is the ideal (most general) interpolant. However, WP is intractable to compute and is exponentially disjunctive. A major challenge is to obtain a conjunctive approximation of the WP. Therefore, we generate an approximation of the WP.

MC/DC coverage prescribes a set of MC/DC sequences. Such a sequence is defined by a specification of the truth values of certain atomic boolean expressions which appear in predicates (i.e. boolean combinations of atomic boolean expressions) in the program. An execution trace satisfies the sequence if it realizes the atomic boolean conditions in accordance with the truth value specification of the sequence. An MC/DC sequence is feasible if there is one such execution trace. The overall goal for an MC/DC test generator is, for each sequence: if feasible, to generate a test input realizing the sequence; otherwise, to prove that the sequence is infeasible.

Dynamic Symbolic Execution (DSE) is an important method for testing of programs. An important system on DSE is KLEE [ 1 ] which inputs a C/C++ program annotated with symbolic variables, compiles it into LLVM, and then emulates the execution paths of LLVM using a specified backtracking strategy. The major challenge in symbolic execution is path explosion . The method of abstraction learning [ 7 ] has been used to address this. The key step here is the computation of an interpolant to represent the learned abstraction. TracerX, our tool, is built on top of KLEE and it implements and utilizes abstraction learning . The core feature in abstraction learning is subsumption of paths whose traversals are deemed to no longer be necessary due to similarity with already-traversed paths. Despite the overhead of computing interpolants, the pruning of the symbolic execution tree that interpolants provide often brings significant overall benefits. In particular, TracerX can fully explore many programs that would be impossible for any non-pruning system like KLEE to do so.

With the advances in both hardware and software of embedded systems in the past few years, dynamic memory allocation can now be safely used in embedded software. As a result, the need to develop methods to avoid heap overflow errors in safety-critical embedded systems has increased. Resource analysis of imperative programs with non-regular loop patterns and signed integers, to support both memory allocation and deallocation, has long been an open problem. Existing methods can generate symbolic bounds that are parametric w.r.t. the program inputs; such bounds, however, are imprecise in the presence of non-regular loop patterns. In this paper, we present a worst-case memory consumption analysis, based upon the framework of symbolic execution. Our assumption is that loops (and recursions) of to-be-analyzed programs are indeed bounded. We then can exhaustively unroll loops and the memory consumption of each iteration can be precisely computed and summarized for aggregation. Because of path-sensitivity, our algorithm generates more precise bounds. Importantly, we demonstrate that by introducing a new concept of reuse, symbolic execution scales to a set of realistic benchmark programs.

We present a framework for WCET analysis of programs with emphasis on cache micro-architecture. Such an analysis is challenging primarily because of the timing model of a dynamic nature, that is, the timing of a basic block is heavily dependent on the context in which it is executed. At its core, our algorithm is based on symbolic execution, and an analysis is obtained by locating the "longest" symbolic execution path. Clearly a challenge is the intractable number of paths in the symbolic execution tree. Traditionally this challenge is met by performing some form of abstraction in the path generation process but this leads to a loss of path-sensitivity and thus precision in the analysis. The key feature of our algorithm is the ability for reuse. This is critical for maintaining a high-level of path-sensitivity, which in turn produces significantly increased accuracy. In other words, reuse allows scalability in path-sensitive exploration. Finally, we present an experimental evaluation on well known benchmarks in order to show two things: that systematic path-sensitivity in fact brings significant accuracy gains, and that the algorithm still scales well.