Abstract Applying deductive verification to formally prove that a program respects its formal specification is a very complex and time-consuming task due in particular to the lack of feedback in case of proof failures. Along with a non-compliance between the code and its specification (due to an error in at least one of them), possible reasons of a proof failure include a missing or too weak specification for a called function or a loop, and lack of time or simply incapacity of the prover to finish a particular proof. This work proposes a methodology where test generation helps to identify the reason of a proof failure and to exhibit a counterexample clearly illustrating the issue. We define the categories of proof failures, introduce two subcategories of contract weaknesses (single and global ones), and examine their properties. We describe how to transform a C program formally specified in an executable specification language into C code suitable for testing, and illustrate the benefits of the method on comprehensive examples. The method has been implemented in StaDy , a plugin of the software analysis platform Frama -C. Initial experiments show that detecting non-compliances and contract weaknesses allows to precisely diagnose most proof failures.

Software verification and validation often rely on formal specifications that encode desired program properties. Recent research proposed a combined verification approach in which a program can be incrementally verified using alternatively deductive verification and testing. Both techniques should use the same specification expressed in a unique specification language. This paper addresses this problem within the Frama-C framework for analysis of C programs, that offers ACSL as a common specification language. We provide a formal description of an automatic translation of ACSL annotations into C code that can be used by a test generation tool either to trigger and detect specification failures, or to gain confidence, or, under some assumptions, even to confirm that the code is in conformity with respect to the annotations. We implement the proposed specification translation in a combined verification tool Study. Our initial experiments suggest that the proposed support for a common specification language can be very helpful for combined static-dynamic analyses.

Recent code-based test input generators based on dynamic symbolic execution increase path coverage by solving path condition with a constraint or an SMT solver. When the solver considers path condition produced from an infeasible path, it tries to show unsatisfiability, which is a useless time-consuming process. In this paper, we propose a new method that takes opportunity of the detection of a single infeasible path to generalize to a (possibly infinite) family of infeasible paths, which will not have to be considered in further path conditions solving. The method exploits non-intrusive constraint-based explanations, a technique developed in Constraint Programming to explain unsatisfiability. Experimental results obtained with our prototype tool IPEG show that, whatever is the underlying constraint solving procedure (IC, Colibri and the SMT solver Z3), this approach can save considerable computational time.

Abstract Symbolic execution is a classical program testing technique which evaluates a selected control flow path with symbolic input data. A constraint solver can be used to enforce the satisfiability of the extracted path conditions as well as to derive test data. Whenever path conditions contain floating‐point computations, a common strategy consists of using a constraint solver over the rationals or the reals. Unfortunately, even in a fully IEEE‐754‐compliant environment, this leads not only to approximations but also can compromise correctness: a path can be labelled as infeasible although there exists floating‐point input data that satisfy it. In this paper, the peculiarities of symbolic execution of programs with floating‐point numbers are addressed. Issues in the symbolic execution of this kind of program are carefully examined and a constraint solver is described that supports constraints over floating‐point numbers. Preliminary experimental results demonstrate the value of the approach proposed. Copyright © 2005 John Wiley & Sons, Ltd.

Automatic test data generation leads to the identification of input values on which a selected path or a selected branch is executed within a program (path-oriented vs. goal-oriented methods). In both cases, several approaches based on constraint solving exist, but in the presence of pointer variables only path-oriented methods have been proposed. This paper proposes to extend an existing goal-oriented test data generation technique to deal with multi-level pointer variables. The approach exploits the results of an intraprocedural flow-sensitive points-to analysis to automatically generate goal-oriented test data at the unit testing level. Implementation is in progress and a few examples are presented.

Constraint-Based Test data generation (CBT) exploits constraint satisfaction techniques to generate test data able to kill a given mutant or to reach a selected branch in a program. When pointer variables are present in the program, aliasing problems may arise and may lead to the failure of current CBT approaches. In our work, we propose an overall CBT method that exploits the results of an intraprocedural points-to analysis and provides two specific constraint combinators for automatically generating test data able to reach a selected branch. Our approach correctly handles multi-levels stack-directed pointers that are mainly used in real-time control systems. The method has been fully implemented in the test data generation tool INKA and first experiences in applying it to a variety of existing programs tend to show the interest of the approach.

Usual techniques for automatic test data generation are based on the assumption that a complete oracle will be available during the testing process. However, there are programs for which this assumption is unreasonable. Recently, Chen et al. (1998, 2001) proposed to overcome this obstacle by using known relations over the input data and their unknown expected outputs to seek a subclass of faults inside the program. In this paper, we introduce an automatic testing framework able to check these so-called metamorphic relations. The framework makes use of constraint logic programming techniques to find test data that violate a given metamorphic-relation. Circumstances where it can also prove that the program satisfies this relation are presented. The first experimental results we got with a prototype tool build on the top of the test data generator INKA, show that this methodology can be completely automated.

Automatic test data generation leads to identify input values on which a selected point in a procedure is executed. This paper introduces a new method for this problem based on constraint solving techniques. First, we statically transform a procedure into a constraint system by using well-known "Static Single Assignment" form and control-dependencies. Second, we solve this system to check whether at least one feasible control flow path going through the selected point exists and to generate test data that correspond to one of these paths.The key point of our approach is to take advantage of current advances in constraint techniques when solving the generated constraint system. Global constraints are used in a preliminary step to detect some of the non feasible paths. Partial consistency techniques are employed to reduce the domains of possible values of the test data. A prototype implementation has been developped on a restricted subset of the C language. Advantages of our approach are illustrated on a non-trivial example.