Source author record

Roberto Bagnara

Roberto Bagnara appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Programming Languages Software Engineering Artificial Intelligence Logic in Computer Science

Catalog footprint

What is connected

8works

4topics

4close collaborators

Actions

Connect this record

Open graph Browse works

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

preprint2021arXiv

Correct Approximation of IEEE 754 Floating-Point Arithmetic for Program Verification

Verification of programs using floating-point arithmetic is challenging on several accounts. One of the difficulties of reasoning about such programs is due to the peculiarities of floating-point arithmetic: rounding errors, infinities, non-numeric objects (NaNs), signed zeroes, denormal numbers, different rounding modes, etc. One possibility to reason about floating-point arithmetic is to model a program computation path by means of a set of ternary constraints of the form z = x op y and use constraint propagation techniques to infer new information on the variables' possible values. In this setting, we define and prove the correctness of algorithms to precisely bound the value of one of the variables x, y or z, starting from the bounds known for the other two. We do this for each of the operations and for each rounding mode defined by the IEEE 754 binary floating-point standard, even in the case the rounding mode in effect is only partially known. This is the first time that such so-called filtering algorithms are defined and their correctness is formally proved. This is an important slab for paving the way to formal verification of programs that use floating-point arithmetics.

preprint2020arXiv

A Practical Approach to Interval Refinement for math.h/cmath Functions

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.

preprint2020arXiv

BARR-C:2018 and MISRA C:2012: Synergy Between the Two Most Widely Used C Coding Standards

The Barr Group's Embedded C Coding Standard (BARR-C:2018, which originates from the 2009 Netrino's Embedded C Coding Standard) is, for coding standards used by the embedded system industry, second only in popularity to MISRA C. However, the choice between MISRA C:2012 and BARR-C:2018 needs not be a hard decision since they are complementary in two quite different ways. On the one hand, BARR-C:2018 has removed all the incompatibilities with respect to MISRA C:2012 that were present in the previous edition (BARR-C:2013). As a result, disregarding programming style, BARR-C:2018 defines a subset of C that, while preventing a significant number of programming errors, is larger than the one defined by MISRA C:2012. On the other hand, concerning programming style, whereas MISRA C leaves this to individual organizations, BARR-C:2018 defines a programming style aimed primarily at minimizing programming errors. As a result, BARR-C:2018 can be seen as a first, dramatically useful step to C language subsetting that is suitable for all kinds of projects; critical projects can then evolve toward MISRA C:2012 compliance smoothly while maintaining the BARR-C programming style. In this paper, we introduce BARR-C:2018, we describe its relationship with MISRA C:2012, and we discuss the parallel and serial adoption of the two coding standards.

preprint2015arXiv

Exploiting Binary Floating-Point Representations for Constraint Propagation: The Complete Unabridged Version

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.

preprint2013arXiv

Eventual Linear Ranking Functions

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.

preprint2013arXiv

Proceedings of the 12th International Colloquium on Implementation of Constraint and LOgic Programming Systems

This volume contains the papers presented at CICLOPS'12: 12th International Colloquium on Implementation of Constraint and LOgic Programming Systems held on Tueseday September 4th, 2012 in Budapest. The program included 1 invited talk, 9 technical presentations and a panel discussion on Prolog open standards (open.pl). Each programme paper was reviewed by 3 reviewers. CICLOPS'12 continues a tradition of successful workshops on Implementations of Logic Programming Systems, previously held in Budapest (1993) and Ithaca (1994), the Compulog Net workshops on Parallelism and Implementation Technologies held in Madrid (1993 and 1994), Utrecht (1995) and Bonn (1996), the Workshop on Parallelism and Implementation Technology for (Constraint) Logic Programming Languages held in Port Jefferson (1997), Manchester (1998), Las Cruces (1999), and London (2000), and more recently the Colloquium on Implementation of Constraint and LOgic Programming Systems in Paphos (2001), Copenhagen (2002), Mumbai (2003), Saint Malo (2004), Sitges (2005), Seattle (2006), Porto (2007), Udine (2008), Pasadena (2009), Edinburgh (2010) - together with WLPE, Lexington (2011). We would like to thank all the authors, Tom Schrijvers for his invited talk, the programme committee members, and the ICLP 2012 organisers. We would like to also thank arXiv.org for providing permanent hosting.

preprint2012arXiv

The Automatic Synthesis of Linear Ranking Functions: The Complete Unabridged Version

The classical technique for proving termination of a generic sequential computer program involves the synthesis of a ranking function for each loop of the program. Linear ranking functions are particularly interesting because many terminating loops admit one and algorithms exist to automatically synthesize it. In this paper we present two such algorithms: one based on work dated 1991 by Sohn and Van Gelder; the other, due to Podelski and Rybalchenko, dated 2004. Remarkably, while the two algorithms will synthesize a linear ranking function under exactly the same set of conditions, the former is mostly unknown to the community of termination analysis and its general applicability has never been put forward before the present paper. In this paper we thoroughly justify both algorithms, we prove their correctness, we compare their worst-case complexity and experimentally evaluate their efficiency, and we present an open-source implementation of them that will make it very easy to include termination-analysis capabilities in automatic program verifiers.

preprint2011arXiv

Coding Guidelines for Prolog

Coding standards and good practices are fundamental to a disciplined approach to software projects, whatever programming languages they employ. Prolog programming can benefit from such an approach, perhaps more than programming in other languages. Despite this, no widely accepted standards and practices seem to have emerged up to now. The present paper is a first step towards 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 programming 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 fully-fledged coding standard for the project.