Formalizing an Efficient Runtime Assertion Checker for an Arithmetic Language with Functions and Predicates

Runtime Assertion Checking (RAC) is a lightweight formal method that verifies formal code annotations, typically assertions, at runtime. The main RAC challenge consists in generating code that is both sound and efficient for checking expressive properties. In particular, checking formal arithmetic properties usually requires to use machine integer arithmetic to be efficient, but needs to rely on an exact yet slower arithmetic library to be sound. This paper formalizes an efficient RAC tool for arithmetic properties, which may include user-defined functions and predicates. Efficient code generation for these routines is based on specialization, allowing to generate efficient functions using machine arithmetic when possible, or slower functions relying on exact arithmetic, according to the calling context. This formalization is implemented in E-ACSL, a runtime assertion checker for C programs.