TAP 2023
Tue 18 - Wed 19 July 2023 Leicester, United Kingdom
co-located with STAF 2023
Wed 19 Jul 2023 15:45 - 16:15 at Willow - TAP Session 6: Abstraction and Refinement Chair(s): Matteo Cimini

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 Jul

Displayed 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
30m
Talk
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
30m
Talk
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
P: Megan Strauss Carnegie Mellon University, Stefan Mitsch Carnegie Mellon University, USA
DOI