Adds 3 E-ACSL publications

_fc-publications/e-acsl/founding/2020-rv-kms.md

+---
+plugin: "e-acsl"
+authors: "Nikolai Kosmatov, Fonenantsoa Maurica and Julien Signoles"
+title: "Efficient Runtime Assertion Checking for Properties over Mathematical Numbers"
+book: "International Conference on Runtime Verification (RV)"
+link: http://julien.signoles.free.fr/publis/2020_rv.pdf
+year: 2020
+category: founding
+---
+
+Runtime assertion checking is the discipline of detecting at
+runtime violations of program properties written as formal code annotations.
+These properties often include numerical properties, which may rely on either
+(bounded) machine representations or (unbounded) mathematical numbers. The
+verification of the former is easier to implement and more efficient at
+runtime, while the latter are more expressive and often more adequate for
+writing specifications. This short paper explains how the runtime assertion
+checker E-ACSL reconciles both approaches by presenting a type system that
+allows the tool to generate efficient machine-number based code when it is
+safe to do so, while generating arbitrary-precision code when it is necessary.
+This type system and the code generator not only handle integers but also
+rational arithmetics. As far as we know, it is the first runtime verification
+tool that supports the verification of properties over rational numbers.
\ No newline at end of file

_fc-publications/e-acsl/other/2015-jfla-jks.md

+---
+plugin: "e-acsl"
+authors: "Arvid Jakobsson, Nikolai Kosmatov and Julien Signoles"
+title: "Rester statique pour devenir plus rapide, plus précis et plus mince"
+book: "Journées Francophones des Langages Applicatifs (JFLA)"
+link: http://julien.signoles.free.fr/publis/2015_jfla.pdf
+year: 2015
+category: other
+short: "In French"
+---
+
+E-ACSL est un greffon de Frama-C, une plateforme d'analyse de codes C qui est
+développée en OCaml. Son but est de transformer un programme C formellement
+annoté dans le langage de spécification éponyme E-ACSL en un autre programme C
+dont le comportement à l'exécution est équivalent si toutes les spécifications
+sont dynamiquement vérifiées et qui échoue sur la première spécification
+fausse sinon. Pour cela, une instrumentation du programme source est notamment
+effectuée afin, d'une part, de conserver les informations nécessaires à
+l'évaluation des prédicats E-ACSL et, d'autre part, de traduire correctement
+ces derniers.
+
+Cet article présente deux analyses statiques qui améliorent grandement la
+précision de cette transformation de programmes en réduisant l'instrumentation
+effectuée. Ainsi, le code généré est plus rapide et consomme moins de mémoire
+lors de son exécution. La première analyse est un système de types fondé sur
+une inférence d'intervalles et permettant de distinguer les entiers
+(mathématiques) pouvant être convertis en des expressions C de type "entier
+machine" de ceux devant être traduits vers des entiers en précision
+arbitraire. La seconde analyse est une analyse flot de données arrière
+sur-approximante paramétrée par une analyse d'alias. Elle permet de limiter
+l'instrumentation des opérations sur la mémoire à celles ayant un impact
+potentiel sur la validité d'une annotation formelle. 

_fc-publications/e-acsl/tutorials/2013-rv-ks.md

+---
+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.
\ No newline at end of file