Skip to content
Snippets Groups Projects
Normal view Permalink
2013-rv-ks.md 1.13 KiB
Newer Older
Allan Blanchard's avatar
Adds 3 E-ACSL publications
Allan Blanchard committed
1 2 3 4 5 6 7 8 9 10 11 12 
---
plugin: "e-acsl"
authors: "Nikolai Kosmatov and Julien Signoles"
title: "A Lesson on Runtime Assertion Checking with Frama-C"
book: "International Conference on Runtime Verification (RV)"
link: "http://julien.signoles.free.fr/publis/2013_rv.pdf"
year: 2013
category: tutorials
short: "A tutorial about the Frama-C plug-in E-ACSL."
---

Runtime assertion checking provides a powerful, highly automatizable technique to detect violations of specified program properties. This paper provides a lesson on runtime assertion checking with Frama-C, a publicly available toolset for analysis of C programs. We illustrate how a C program can be specified in executable specification language E-ACSL and how this specification can be automatically translated into instrumented C code suitable for monitoring and runtime verification of specified properties. We show how various errors can be automatically detected on the instrumented code, including C runtime errors, failures in postconditions, assertions, preconditions of called functions, and memory leaks. Benefits of combining runtime assertion checking with other Frama-C analyzers are illustrated as well.