NPATH is a metric introduced by Brian A. Nejmeh (Communications of the ACM, 31(2):188-200, 1988) that is aimed at overcoming some important limitations of McCabe’s cyclomatic complexity metric. Despite the fact that the declared NPATH objective is to count the number of acyclic execution paths through a function, the definition given for the C language in Nejmeh’s paper fails to do so even for very simple programs. We show that counting the number of acyclic paths in CFG is unfeasible in general. Then we define a new metric for C -like languages, called $A C P A T H$, that allows to quickly compute a very good estimation of the number of acyclic execution paths through the given function. We show that, if the function body does not contain backward gotos and does not contain jumps into a loop from outside the loop (which is the case for all MISRA-compliant programs), then such estimation is actually exact.

Verification of C/C++ programs has seen considerable progress in several areas, but not for programs that use these languages’ mathematical libraries. The reason is that all libraries in widespread use come with no guarantees about the computed results. This would seem to prevent any attempt at formal verification of programs that use them: without a specification for the functions, no conclusion can be drawn statically about the behavior of the program. We propose an alternative to surrender. We introduce a pragmatic approach that leverages the fact that most math.h/cmath functions are almost piecewise monotonic: as we discovered through exhaustive testing, they may have glitches , often of very small size and in small numbers. We develop interval refinement techniques for such functions based on a modified dichotomic search, which enable verification via symbolic execution based model checking, abstract interpretation, and test data generation. To the best of our knowledge, our refinement algorithms are the first in the literature to be able to handle non-correctly rounded function implementations, enabling verification in the presence of the most common implementations. We experimentally evaluate our approach on real-world code, showing its ability to detect or rule out anomalous behaviors.

Floating-point computations are quickly finding their way in the design of safety- and mission-critical systems, despite the fact that designing floating-point algorithms is significantly more difficult than designing integer algorithms. For this reason, verification and validation of floating-point computations are hot research topics. An important verification technique, especially in some industrial sectors, is testing. However, generating test data for floating-point intensive programs proved to be a challenging problem. Existing approaches usually resort to random or search-based test data generation, but without symbolic reasoning it is almost impossible to generate test inputs that execute complex paths controlled by floating-point computations. Moreover, because constraint solvers over the reals or the rationals do not natively support the handling of rounding errors, the need arises for efficient constraint solvers over floating-point domains. In this paper, we present and fully justify improved algorithms for the propagation of arithmetic IEEE 754 binary floating-point constraints. The key point of these algorithms is a generalization of an idea by B. Marre and C. Michel that exploits a property of the representation of floating-point numbers.

Verifying critical numerical software involves the generation of test data for floating-point intensive programs. As the symbolic execution of floating-point computations presents significant difficulties, existing approaches usually resort to random or search-based test data generation. However, without symbolic reasoning, it is almost impossible to generate test inputs that execute many paths with floating-point computations. Moreover, constraint solvers over the reals or the rationals do not handle the rounding errors. In this paper, we present a new version of FPSE, a symbolic evaluator for C program paths, that specifically addresses this problem. The tool solves path conditions containing floating-point computations by using correct and precise projection functions. This version of the tool exploits an essential filtering property based on the representation of floating-point numbers that makes it suitable to generate path-oriented test inputs for complex paths characterized by floating-point intensive computations. The paper reviews the key implementation choices in FPSE and the labeling search heuristics we selected to maximize the benefits of enhanced filtering. Our experimental results show that FPSE can generate correct test inputs for selected paths containing several hundreds of iterations and thousands of executable floating-point statements on a standard machine: this is currently outside the scope of any other symbolic-execution test data generator tool.

Program termination is a hot research topic in program analysis. The last few years have witnessed the development of termination analyzers for programming languages such as C and Java with remarkable precision and performance. These systems are largely based on techniques and tools coming from the field of declarative constraint programming. In this paper, we first recall an algorithm based on Farkas' Lemma for discovering linear ranking functions proving termination of a certain class of loops. Then we propose an extension of this method for showing the existence of eventual linear ranking functions, i.e., linear functions that become ranking functions after a finite unrolling of the loop. We show correctness and completeness of this algorithm.

Abstract Coding standards and good practices are fundamental to a disciplined approach to software projects irrespective of programing languages being employed. Prolog programing can benefit from such an approach, perhaps more than programing in other languages. Despite this, no widely accepted standards and practices seem to have emerged till now. The present paper is a first step toward filling this void: It provides immediate guidelines for code layout, naming conventions, documentation, proper use of Prolog features, program development, debugging, and testing. Presented with each guideline is its rationale and, where sensible options exist, illustrations of the relative pros and cons for each alternative. A coding standard should always be selected on a per-project basis, based on a host of issues pertinent to any given programing project; for this reason the paper goes beyond the mere provision of normative guidelines by discussing key factors and important criteria that should be taken into account when deciding on a full-fledged coding standard for the project.

Abstract Since the seminal work of Cousot and Halbwachs, the domain of convex polyhedra has been employed in several systems for the analysis and verification of hardware and software components. Although most implementations of the polyhedral operations assume that the polyhedra are topologically closed (i.e., all the constraints defining them are non-strict), several analyzers and verifiers need to compute on a domain of convex polyhedra that are not necessarily closed (NNC). The usual approach to implementing NNC polyhedra is to embed them into closed polyhedra in a higher dimensional vector space and reuse the tools and techniques already available for closed polyhedra. In this work we highlight and discuss the issues underlying such an embedding for those implementations that are based on the double description method, where a polyhedron may be described by a system of linear constraints or by a system of generating rays and points. Two major achievements are the definition of a theoretically clean, high-level user interface and the specification of an efficient procedure for removing redundancies from the descriptions of NNC polyhedra.

$\textup{\textsf{Sharing}}$ , an abstract domain developed by D. Jacobs and A. Langen for the analysis of logic programs, derives useful aliasing information. It is well-known that a commonly used core of techniques, such as the integration of $\textup{\textsf{Sharing}}$ with freeness and linearity information, can significantly improve the precision of the analysis. However, a number of other proposals for refined domain combinations have been circulating for years. One feature that is common to these proposals is that they do not seem to have undergone a thorough experimental evaluation even with respect to the expected precision gains. In this paper we experimentally evaluate: helping $\textup{\textsf{Sharing}}$ with the definitely ground variables found using $\textit{Pos}$ , the domain of positive Boolean formulas; the incorporation of explicit structural information; a full implementation of the reduced product of $\textup{\textsf{Sharing}}$ and $\textit{Pos}$ ; the issue of reordering the bindings in the computation of the abstract $\mgu$ ; an original proposal for the addition of a new mode recording the set of variables that are deemed to be ground or free; a refined way of using linearity to improve the analysis; the recovery of hidden information in the combination of $\textup{\textsf{Sharing}}$ with freeness information. Finally, we discuss the issue of whether tracking compoundness allows the computation of more sharing information.

We present cTI, the first system for universal left-termination inference of logic programs. Termination inference generalizes termination analysis and checking. Traditionally, a termination analyzer tries to prove that a given class of queries terminates. This class must be provided to the system, for instance by means of user annotations. Moreover, the analysis must be redone every time the class of queries of interest is updated. Termination inference, in contrast, requires neither user annotations nor recomputation. In this approach, terminating classes for all predicates are inferred at once. We describe the architecture of cTI and report an extensive experimental evaluation of the system covering many classical examples from the logic programming termination literature and several Prolog programs of respectable size and complexity.

It is well known that freeness and linearity information positively interact with aliasing information, allowing both the precision and the efficiency of the sharing analysis of logic programs to be improved. In this paper, we present a novel combination of set-sharing with freeness and linearity information, which is characterized by an improved abstract unification operator. We provide a new abstraction function and prove the correctness of the analysis for both the finite tree and the rational tree cases. Moreover, we show that the same notion of redundant information as identified in Bagnara et al. (2000) and Zaffanella et al. (2002) also applies to this abstract domain combination: this allows for the implementation of an abstract unification operator running in polynomial time and achieving the same precision on all the considered observable properties.

It is important that practical data-flow analyzers are backed by reliably proven theoretical results. Abstract interpretation provides a sound mathematical framework and necessary generic properties for an abstract domain to be well-defined and sound with respect to the concrete semantics. In logic programming, the abstract domain Sharing is a standard choice for sharing analysis for both practical work and further theoretical study. In spite of this, we found that there were no satisfactory proofs for the key properties of commutativity and idempotence that are essential for Sharing to be well-defined and that published statements of the soundness of Sharing assume the occurs-check. This paper provides a generalization of the abstraction function for Sharing that can be applied to any language, with or without the occurs-check. Results for soundness, idempotence and commutativity for abstract unification using this abstraction function are proven.

Complementation, the inverse of the reduced product operation, is a technique for systematically finding minimal decompositions of abstract domains. Filé and Ranzato advanced the state of the art by introducing a simple method for computing a complement. As an application, they considered the extraction by complementation of the pair-sharing domain PS from the Jacobs and Langen's set-sharing domain SH. However, since the result of this operation was still SH, they concluded that PS was too abstract for this. Here, we show that the source of this result lies not with PS but with SH and, more precisely, with the redundant information contained in SH with respect to ground-dependencies and pair-sharing. In fact, a proper decomposition is obtained if the non-redundant version of SH, PSD, is substituted for SH. To establish the results for PSD, we define a general schema for subdomains of SH that includes PSD and Def as special cases. This sheds new light on the structure of PSD and exposes a natural though unexpected connection between Def and PSD. Moreover, we substantiate the claim that complementation alone is not sufficient to obtain truly minimal decompositions of domains. The right solution to this problem is to first remove redundancies by computing the quotient of the domain with respect to the observable behavior, and only then decompose it by complementation.

Sharing, a domain due to D. Jacobs and A. Langen for the analysis of logic programs, derives useful aliasing information.It is well-known that a commonly used core of techniques, such as the standard integration of Sharing with freeness and linearity information, can signi cantly improve the precision of Sharing.However, a numb e rof other proposals for re ned domain combinations have been circulating for years.One feature that is common to these proposals is that they do not seem to have undergone a thorough experimental evaluation even with respect to the expected precision gains.In this paper, we discuss and/or experimentally evaluate: helping Sharing with de nitely ground variables computed with Pos; the incorporation of explicit structural information into the domain of analysis; more sophisticated ways of integrating Sharing and Pos; the issue of reordering the bindings in the computation of the abstract mgu; an original proposal concerning the addition of a domain recording the set of variables that are deemed to b eground or free; a more re ned way of using linearity to improve the analysis; the issue of whether tracking compoundness allows to compute more precise sharing information; and, nally, the recovery of hidden information in the combination of Sharing with the usual domain for freeness.