6 citations · 13 across the 6 of their papers we have counts for
7 papers
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…
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…
The ACPATH Metric: Precise Estimation of the Number of Acyclic Paths in C-like Languages
Roberto Bagnara, Abramo Bagnara, Alessandro Benedetti +1
NPATH is a metric introduced by Brian A. Nejmeh in [13] that is aimed at overcoming some important limitations of McCabe's cyclomatic complexity. Despite the fact that the declared…
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…