E-ACSL, a Runtime Verification Tool for Safety and Security of C Programs (tool paper) Article Swipe

PDF

Related Concepts

Computer science Runtime verification Programming language Formal verification Formal methods Formal specification Specification language Software engineering Refinement

Julien Signoles , Nikolaï Kosmatov , Kostyantyn Vorobyov ·

YOU? · · 2018 · Open Access · · DOI: https://doi.org/10.29007/fpdh · OA: W2786344151

This tool paper presents E-ACSL, a runtime verification tool for C programs capable of checking a broad range of safety and security properties expressed using a formal specification language. E-ACSL consumes a C program annotated with formal specifications and generates a new C program that behaves similarly to the original if the formal properties are satisfied, or aborts its execution whenever a property does not hold. This paper presents an overview of E-ACSL and its specification language.