Abstract Interpretation of Recursive Logic Definitions for Efficient Runtime Assertion CheckingTAP Best Paper
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 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.
Wed 19 JulDisplayed time zone: London change
15:45 - 16:45 | TAP Session 6: Abstraction and RefinementResearch Papers at Willow Chair(s): Matteo Cimini University of Massachusetts Lowell Remote Participants: Zoom Link | ||
15:45 30mTalk | Abstract Interpretation of Recursive Logic Definitions for Efficient Runtime Assertion CheckingTAP Best Paper Research Papers P: Thibaut Benjamin Université Paris-Saclay, CEA, List, Julien Signoles Université Paris-Saclay, CEA, List DOI | ||
16:15 30mTalk | Slow Down, Move Over: A Case Study in Formal Verification, Refinement, and Testing of the Responsibility-Sensitive Safety Model for Self-Driving Cars Research Papers DOI |