TY - GEN
T1 - Efficient Runtime Assertion Checking for Properties over Mathematical Numbers
AU - Kosmatov, Nikolai
AU - Maurica, Fonenantsoa
AU - Signoles, Julien
N1 - Publisher Copyright:
© 2020, Springer Nature Switzerland AG.
PY - 2020/1/1
Y1 - 2020/1/1
N2 - 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.
AB - 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.
KW - Numerical properties
KW - Optimized code generation
KW - Rational numbers
KW - Runtime assertion checking
KW - Typing
U2 - 10.1007/978-3-030-60508-7_17
DO - 10.1007/978-3-030-60508-7_17
M3 - Conference contribution
AN - SCOPUS:85093101797
SN - 9783030605070
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 310
EP - 322
BT - Runtime Verification - 20th International Conference, RV 2020, Proceedings
A2 - Deshmukh, Jyotirmoy
A2 - Nickovic, Dejan
PB - Springer Science and Business Media Deutschland GmbH
T2 - 20th International Conference on Runtime Verification, RV 2020
Y2 - 6 October 2020 through 9 October 2020
ER -