Abstract Interpretation of Recursive Logic Definitions for Efficient Runtime Assertion Checking

Runtime Assertion Checking (RAC) is a lightweight formal method for verifying at runtime code properties written in a formal specification language. One of the main challenge of RAC is to check the properties efficiently, while emitting sound verdicts. In particular, arithmetic properties are only efficiently verified using machine integers, yet soundness can only be achieved by using an exact but slower exact arithmetic library. This paper presents how E-ACSL, a RAC tool for C programs, applies abstract interpretation for efficiently and soundly supporting arithmetic properties. Abstract interpretation provides sound static information regarding the size of terms involved in runtime assertions in order to choose at compile time whether machine integers or exact arithmetic will be used at runtime on a case by case basis. Our specification language includes recursive user-defined logic functions and predicates, for which we rely on fast fixpoint operators based on widening of abstract values.