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

Thibaut Benjamin; Julien Signoles

doi:10.1145/3555776.3577617

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

Thibaut Benjamin, Julien Signoles

Université Paris-Saclay

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

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.

Original language	English
Title of host publication	Proceedings of the 38th ACM/SIGAPP Symposium on Applied Computing, SAC 2023
Publisher	Association for Computing Machinery
Pages	1673-1680
Number of pages	8
ISBN (Electronic)	9781450395175
DOIs	https://doi.org/10.1145/3555776.3577617
Publication status	Published - 27 Mar 2023
Externally published	Yes
Event	38th Annual ACM Symposium on Applied Computing, SAC 2023 - Tallinn, Estonia Duration: 27 Mar 2023 → 31 Mar 2023

Publication series

Name	Proceedings of the ACM Symposium on Applied Computing

Conference

Conference	38th Annual ACM Symposium on Applied Computing, SAC 2023
Country/Territory	Estonia
City	Tallinn
Period	27/03/23 → 31/03/23

Access to Document

10.1145/3555776.3577617

Cite this

Benjamin, T., & Signoles, J. (2023). Formalizing an Efficient Runtime Assertion Checker for an Arithmetic Language with Functions and Predicates. In Proceedings of the 38th ACM/SIGAPP Symposium on Applied Computing, SAC 2023 (pp. 1673-1680). (Proceedings of the ACM Symposium on Applied Computing). Association for Computing Machinery. https://doi.org/10.1145/3555776.3577617

@inproceedings{444797d05bac4ece8765d72a512e30ef,

title = "Formalizing an Efficient Runtime Assertion Checker for an Arithmetic Language with Functions and Predicates",

abstract = "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.",

author = "Thibaut Benjamin and Julien Signoles",

note = "Publisher Copyright: {\textcopyright} 2023 ACM.; 38th Annual ACM Symposium on Applied Computing, SAC 2023 ; Conference date: 27-03-2023 Through 31-03-2023",

year = "2023",

month = mar,

day = "27",

doi = "10.1145/3555776.3577617",

language = "English",

series = "Proceedings of the ACM Symposium on Applied Computing",

publisher = "Association for Computing Machinery",

pages = "1673--1680",

booktitle = "Proceedings of the 38th ACM/SIGAPP Symposium on Applied Computing, SAC 2023",

}

Benjamin, T & Signoles, J 2023, Formalizing an Efficient Runtime Assertion Checker for an Arithmetic Language with Functions and Predicates. in Proceedings of the 38th ACM/SIGAPP Symposium on Applied Computing, SAC 2023. Proceedings of the ACM Symposium on Applied Computing, Association for Computing Machinery, pp. 1673-1680, 38th Annual ACM Symposium on Applied Computing, SAC 2023, Tallinn, Estonia, 27/03/23. https://doi.org/10.1145/3555776.3577617

Formalizing an Efficient Runtime Assertion Checker for an Arithmetic Language with Functions and Predicates. / Benjamin, Thibaut; Signoles, Julien.
Proceedings of the 38th ACM/SIGAPP Symposium on Applied Computing, SAC 2023. Association for Computing Machinery, 2023. p. 1673-1680 (Proceedings of the ACM Symposium on Applied Computing).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

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

AU - Benjamin, Thibaut

AU - Signoles, Julien

PY - 2023/3/27

Y1 - 2023/3/27

N2 - 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.

AB - 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.

U2 - 10.1145/3555776.3577617

DO - 10.1145/3555776.3577617

M3 - Conference contribution

AN - SCOPUS:85162926732

T3 - Proceedings of the ACM Symposium on Applied Computing

SP - 1673

EP - 1680

BT - Proceedings of the 38th ACM/SIGAPP Symposium on Applied Computing, SAC 2023

PB - Association for Computing Machinery

T2 - 38th Annual ACM Symposium on Applied Computing, SAC 2023

Y2 - 27 March 2023 through 31 March 2023

ER -

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

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this