Newer
Older
---
plugin: "e-acsl"
authors: "Nikolai Kosmatov, Fonenantsoa Maurica and Julien Signoles"
title: "Efficient Runtime Assertion Checking for Properties over Mathematical Numbers"
book: "International Conference on Runtime Verification (RV)"
link: http://julien.signoles.free.fr/publis/2020_rv.pdf
year: 2020
category: founding
---
Runtime assertion checking is the discipline of detecting at
runtime violations of program properties written as formal code annotations.
These properties often include numerical properties, which may rely on either
(bounded) machine representations or (unbounded) mathematical numbers. The
verification of the former is easier to implement and more efficient at
runtime, while the latter are more expressive and often more adequate for
writing specifications. This short paper explains how the runtime assertion
checker E-ACSL reconciles both approaches by presenting a type system that
allows the tool to generate efficient machine-number based code when it is
safe to do so, while generating arbitrary-precision code when it is necessary.
This type system and the code generator not only handle integers but also
rational arithmetics. As far as we know, it is the first runtime verification
tool that supports the verification of properties over rational numbers.