21 citations · 78 across the 23 of their papers we have counts for
16 papers · 1 filter
C-rusted: The Advantages of Rust, in C, without the Disadvantages
Roberto Bagnara, Abramo Bagnara, Federico Serafini
C-rusted is an innovative technology whereby C programs can be (partly) annotated so as to express: ownership, exclusivity and shareability of language, system and user-defined res…
Coding Guidelines and Undecidability
Roberto Bagnara, Abramo Bagnara, Patricia M. Hill
The C and C++ programming languages are widely used for the implementation of software in critical systems. They are complex languages with subtle features and peculiarities that m…
A Rationale-Based Classification of MISRA C Guidelines
Roberto Bagnara, Abramo Bagnara, Patricia M. Hill
MISRA C is the most authoritative language subset for the C programming language that is a de facto standard in several industry sectors where safety and security are of paramount…
BARR-C:2018 and MISRA C:2012: Synergy Between the Two Most Widely Used C Coding Standards
Roberto Bagnara, Michael Barr, Patricia M. Hill
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…
That's C, baby. C!
Roberto Bagnara
Hardly a week goes by at BUGSENG without having to explain to someone that almost any piece of C text, considered in isolation, means absolutely nothing. The belief that C text has…
Correct Approximation of IEEE 754 Floating-Point Arithmetic for Program Verification
Roberto Bagnara, Abramo Bagnara, Fabio Biselli +2
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…
The MISRA C Coding Standard and its Role in the Development and Analysis of Safety- and Security-Critical Embedded Software
Roberto Bagnara, Abramo Bagnara, Patricia M. Hill
The MISRA project started in 1990 with the mission of providing world-leading best practice guidelines for the safe and secure application of both embedded control systems and stan…
A Practical Approach to Interval Refinement for math.h/cmath Functions
Roberto Bagnara, Michele Chiari, Roberta Gori +1
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 librarie…
Eventual Linear Ranking Functions
Roberto Bagnara, Fred Mesnard
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…
Proceedings of the 12th International Colloquium on Implementation of Constraint and LOgic Programming Systems
Nicos Angelopoulos, Roberto Bagnara
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,…
The Automatic Synthesis of Linear Ranking Functions: The Complete Unabridged Version
Roberto Bagnara, Fred Mesnard, Andrea Pescetti +1
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 f…
A Prolog-based Environment for Reasoning about Programming Languages (Extended abstract)
Roberto Bagnara, Patricia Hill, Enea Zaffanella
ECLAIR is a Prolog-based prototype system aiming to provide a functionally complete environment for the study, development and evaluation of programming language analysis and imple…
On the Design of Generic Static Analyzers for Modern Imperative Languages
Roberto Bagnara, Patricia M. Hill, Andrea Pescetti +1
The design and implementation of precise static analyzers for significant fragments of modern imperative languages like C, C++, Java and Python is a challenging problem. In this pa…
Widening Operators for Weakly-Relational Numeric Abstractions (Extended Abstract)
Roberto Bagnara, Patricia M. Hill, Elena Mazzi +1
We discuss the divergence problems recently identified in some extrapolation operators for weakly-relational numeric domains. We identify the cause of the divergences and point out…
Finite-Tree Analysis for Constraint Logic-Based Languages: The Complete Unabridged Version
Roberto Bagnara, Roberta Gori, Patricia M. Hill +1
Logic languages based on the theory of rational, possibly infinite, trees have much appeal in that rational trees allow for faster unification (due to the safe omission of the occu…
Soundness, Idempotence and Commutativity of Set-Sharing
Patricia M. Hill, Roberto Bagnara, Enea Zaffanella
It is important that practical data-flow analyzers are backed by reliably proven theoretical results. Abstract interpretation provides a sound mathematical framework and necessary…