Roberta Gori

Roberto Bruni, Lorenzo Gazzella, Roberta Gori

Thanks to the locality principle, separation logics support modular, scalable analysis of large codebases by relying on local axioms and frame rules to focus only on the heap fragments required for verification. However, depending on the direction (forward vs. backward) and sense of approximation (over vs. under) of the analysis, designing the corresponding proof systems can require some ingenuity. In his work on the calculational design of program logics, Patrick Cousot outlines a methodology for deriving proof systems directly from program semantics using abstract interpretation, covering both correctness and incorrectness analyses. Unfortunately, when applied to heap-manipulating programs, Cousot's calculational approach cannot handle the locality principle, because it does not provide a calculational way to derive frame rules and produces axioms that refer to the global heap. In this paper, we propose a general methodology for systematically deriving local axioms in which the locality principle is embedded by construction. For heap-manipulating primitives, we can derive the minimal required heap and the corresponding pre- and postconditions, complemented by universal frame rules without additional syntactic side conditions. Our method is parametric w.r.t. a set of semantic closure properties that are exploited to design local axioms; it can deal with different memory models; it favors the reuse of many inference rules across over- and under-approximation; and it produces logical systems capable of deriving a broader range of triples w.r.t. existing, cleverly designed, program logics for (in)correctness, ranging from Separation Logic and Incorrectness Separation Logic to Separation Sufficient Incorrectness Logic. Furthermore, we demonstrate the flexibility of our methodology by applying it to design a novel proof system for inferring necessary preconditions with separation logic.

Roberto Bagnara, Michele Chiari, Roberta Gori et al.

Verification of 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, that enable verification via symbolic execution based model checking, abstract interpretation, and test data generation. 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.

Roberto Bagnara, Matthieu Carlier, Roberta Gori et al.

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 is a hot research topic. 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, as 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.