Skip to content
Snippets Groups Projects
Commit ee5d0eb4 authored by Julien Signoles's avatar Julien Signoles Committed by Allan Blanchard
Browse files

[publis] Frama-C general, Eva WP, E-ACSL

parent 18e3988d
No related branches found
No related tags found
1 merge request!11publis
Hide whitespace changes
Inline Side-by-side
dokuwiki/publications.md
+ 241
− 326
View file @ ee5d0eb4
---
layout: clean_page
---
This page is dedicated to publications related to Frama-C. They are
categorized by plug-ins. Manuals appear first, then founding thesis and
articles and finally an inexhaustive lists of other relevant articles.
Each category is sorted by inverse order of date of publication.
Please feel free to update this page with your own knowledge. Add links
when possible and only if they do respect copyright.
This page is dedicated to publications related to Frama-C. It is not exhaustive,
but focuses on foundational papers for Frama-C and some of its plug-ins.
# Frama-C General
#### Frama-C Manuals
### Manuals
- Loïc Correnson, Pascal Cuoq, Florent Kirchner, Virgile Prevosto,
Armand Puccetti, Julien Signoles and Boris Yakobowski.
**Frama-C User Manual.**
<http://frama-c.com/download/frama-c-user-manual.pdf>.
- Loïc Correnson, Pascal Cuoq, Florent Kirchner, André Maroneze,
Virgile Prevosto, Armand Puccetti, Julien Signoles, and Boris Yakobowski.
**Frama-C User Manual.**
<http://frama-c.com/download/frama-c-user-manual.pdf>.
*The manual introducing common features to all analyzers.*
<!-- end list -->
- Julien Signoles, Loïc Correnson and Virgile Prevosto.
- Julien Signoles, Thibaud Antignac, Loïc Correnson, Matthieu Lemerre,
and Virgile Prevosto.
**Frama-C Plug-in Development Guide**.
<http://frama-c.com/download/frama-c-plugin-development-guide.pdf>.
*The manual for developing a Frama-C plug-in.*
#### ACSL manuals
- Patrick Baudin, Jean-Christophe Filliâtre, Claude Marché, Benjamin
Monate, Yannick Moy and Virgile Prevosto.
**ACSL: ANSI/ISO C Specification Language. Version 1.7**.
<!-- end list -->
- Patrick Baudin, Jean-Christophe Filliâtre, Claude Marché, Benjamin
Monate, Yannick Moy, and Virgile Prevosto.
**ACSL: ANSI/ISO C Specification Language.**.
<http://frama-c.com/download/acsl.pdf>.
*The reference manual of ACSL, the specification language used by
Frama-C.*
<!-- end list -->
- Virgile Prevosto.
**ACSL Tutorial.**
<http://frama-c.com/download/acsl-tutorial.pdf>.
*The official tutorial of ACSL.*
<!-- end list -->
- Jochen Burghardt and Jens Gerlach.
**ACSL by Example**. *A fairly complete tour of ACSL and WP features
through various functions inspired from C++ STL.*
- <https://github.com/fraunhoferfokus/acsl-by-example> (Major
version of the document corresponds to the Frama-C version that
has been used to make the proofs).
<!-- end list -->
- Patrick Baudin, Pascal Cuoq, Jean-Christophe Filliâtre, Claude
Marché, Benjamin Monate, Yannick Moy and Virgile Prevosto.
**ACSL version 1.7. Implementation in Fluorine-20130601**.
<http://frama-c.com/download/acsl-implementation-Fluorine-20130601.pdf>.
*The sub-part of ACSL implemented in the latest Frama-C release.*
### Founding Articles
#### Founding Articles
- Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien
Signoles and Boris Yakobowski.
- Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles,
and Boris Yakobowski.
**Frama-C, A Software Analysis Perspective.**
In Formal Aspects of Computing, vol. 27 issue 3, March 2015.
<http://dx.doi.org/10.1007/s00165-014-0326-7>.
Extended version of the following paper.
<!-- end list -->
- Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto,
Julien Signoles and Boris Yakobowski.
Julien Signoles, and Boris Yakobowski.
**Frama-C, A Software Analysis Perspective.**
In proceedings of International Conference on Software Engineering
and Formal Methods 2012 (SEFM'12), October 2012.
and Formal Methods 2012 (SEFM), October 2012.
*This paper presents a synthetic view of Frama-C, its main and
composite analyses, and some of its industrial achievements.*
<!-- end list -->
- Loïc Correnson and Julien Signoles.
#### Articles about the Frama-C Kernel
- Julien Signoles.
**Software Architecture of Code Analysis Frameworks Matters:
The Frama-C Example.**
In Formal Integrated Development Environment (F-IDE), June 2015.
<http://julien.signoles.free.fr/publis/2015_fide.pdf>
*This papers presents the Frama-C architecture and discusses its design
choices.*
<!-- end list -->
- Loïc Correnson, and Julien Signoles.
**Combining Analyses for C Program Verification.**
In proceedings of International Workshop on Formal Methods for
Industrial Critical Systems 2012 (FMICS'12), August 2012.
Industrial Critical Systems 2012 (FMICS), August 2012.
<http://julien.signoles.free.fr/publis/2012_fmics.pdf>
*This paper explains how Frama-C combines several partial results
coming from its plug-ins into a fully consolidated validity status
for each program property.*
<!-- end list -->
- Pascal Cuoq, Damien Doligez, Julien Signoles.
**Lightweight Typed Customizable Unmarshaling.** ML workshop 2011
<http://blog.frama-c.com/public/unmarshal.pdf>.
<!-- end list -->
- Julien Signoles.
**Une bibliothèque de typage dynamique en OCaml.**
In Hermann, editor, JFLA 11, Actes des Journées Francophones des
Langages Applicatifs 2011, January 2011. In French.
*Cet article présente une bibliothèque OCaml fournissant une
représentation dynamique des types monomorphes, y compris pour les
instances des types polymorphes et les types de données abstraits.
Elle permet ainsi de voir les types OCaml comme des citoyens de
première classe. Elle comble aussi le fossé séparant OCaml des
langages dynamiques en mêlant vérifications statiques et dynamiques
des types. Nous nous concentrons ici sur le coeur de son
implantation, ses propriétés théoriques et l'usage qui en est fait
dans Frama-C, plateforme logicielle libre d'analyse statique de
programmes C au sein de laquelle cette bibliothèque est distribuée.*
<!-- end list -->
- Pascal Cuoq, Damien Doligez, and Julien Signoles.
**Lightweight Typed Customizable Unmarshaling.**
In Workshop on ML, September 2011.
<http://blog.frama-c.com/public/unmarshal.pdf>.
*This short paper presents how Frama-C unmarshal its data.*
<!-- end list -->
- Pascal Cuoq and Julien Signoles.
- Pascal Cuoq, Julien Signoles, Patrick Baudin, Richard Bonichon,
Géraud Canet, Loïc Correnson, Benjamin Monate, Virgile Prevosto, and
Armand Puccetti.
**Experience Report: OCaml for an Industrial-Strength Static
Analysis Framework.**
In Proceedings of International Conference of Functional Programming
(ICFP'09), pages 281--286, September 2009.
In International Conference of Functional Programming (ICFP),
September 2009.
<http://julien.signoles.free.fr/publis/2009_icfp.pdf>
*This experience report describes the choice of OCaml as the
implementation language for Frama-C, a framework for the static
analysis of C programs. OCaml became the implementation language for
Frama-C because it is expressive. Most of the reasons listed in the
remaining of this article are secondary reasons, features which are
not specific to OCaml (modularity, availability of a C parser,
control over the use of resources...) but could have prevented the
use of OCaml for this project if they had been missing.*
implementation language for Frama-C.*
<!-- end list -->
- Julien Signoles.
**Comment un chameau peut-il écrire un journal?**
In Journées Francophones des Langages Applicatifs (JFLA), January 2014.
In French.
*Presentation of the journalization mechanism of Frama-C.*
<!-- end list -->
- Julien Signoles.
**Une bibliothèque de typage dynamique en OCaml.**
In Journées Francophones des Langages Applicatifs (JFLA), January 2011.
In French.
*Presentation of the Frama-C library for dynamic typing and its usage.*
<!-- end list -->
- Julien Signoles.
**Foncteurs impératifs et composés: la notion de projets dans
Frama-C.**
In Hermann, editor, JFLA 09, Actes des vingtièmes Journées
Francophones des Langages Applicatifs 2009, volume 7.2 of Studia
Informatica Universalis, pages 245--280, June 2009. In French.
*Cet article présente la bibliothèque de projets de Frama-C, une
plateforme facilitant le développement d'analyseurs statiques de
programmes C. Grâce à sa description, nous présentons une
utilisation originale des foncteurs du système de modules de ML qui
exploite aussi bien leur caractère impératif que compositionnel.
Ceci est le seul véritable recours pour réaliser la fonctionalité
souhaitée de manière bien typée. En outre, nous montrons un exemple
peu fréquent d'un même foncteur appliqué plusieurs centaines de
fois. Cet article introduit aussi la plateforme Frama-C elle-même, à
travers un de ses aspects essentiels, la notion de projet.*
#### Other Articles
- Dillon Pariente and Emmanuel Ledinot.
**Formal Verification of Industrial C Code using Frama-C: a Case
Study.**
In Proceedings of First International Conference on Formal
Verification of Object-Oriented Software (FoVeOOS'10), June 2010.
*This paper gives some results and lessons learnt with Frama-C, a
static analysis toolbox, used to prove behavioral and safety
properties on an industrial code. After a short presentation of the
methods and tools background, the related industrial use case is
briefly exposed, with an overview of the process that was followed.
Then the positive results obtained so far are presented, with a few
practices and additional tools developed in-house. To conclude, this
paper presents some needs and future work directions that should be
addressed, to ensure a technology readiness level compliant with
operational use of formal verification into an industrial
development environment.*
**See also the [associated video](http://frama-c.com/video.html)**.
<!-- end list -->
- Matti Mantere, Ilkka Uusitalo, Juha Röning.
**Comparison of Static Code Analysis Tools.**
securware, Third International Conference on Emerging Security
Information, Systems and Technologies, pages 15--22, June 2009.
*In this paper we compare three static code analysis tools. The
tools represent three different approaches in the field of static
analysis: Fortify SCA is a non-annotation based heuristic analyzer,
Splint represents an annotation based heuristic analyzer, and
Frama-C an annotation based correct analyzer. The tools are compared
by analysing their performance when checking a demonstration code
with intentionally implemented errors.*
# Eva / Value Analysis
#### Manual
- Pascal Cuoq and Virgile Prevosto.
**Frama-C’s value analysis plug-in.**
<http://frama-c.com/download/frama-c-value-analysis.pdf>.
*The official manual for the value analysis of Frama-C.*
#### Founding Articles
Frama-C.**
In Journées Francophones des Langages Applicatifs (JFLA), January 2009.
In French.
*Presentation of the Frama-C library providing its notion of
projects.*
<!-- end list -->
### Tutorials
- Allan Blanchard, Nikolai Kosmatov, and Frédéric Loulergue.
**A Lesson on Verification of IoT Software with Frama-C.**
In International Conference on High Performance Computing & Simulation
(HPCS), July 2018.
<https://hal.inria.fr/hal-02317078>
<!-- end list -->
- Nikolai Kosmatov and Julien Signoles.
**Frama-C, a Collaborative Framework for C Code Verification.
Tutorial Synopsis.**
In International Conference on Runtime Verification (RV 2016),
September 2016.
<http://julien.signoles.free.fr/publis/2016_rv.pdf>
<!-- end list -->
# Eva
### Manual
- David Bühler, Pascal Cuoq, Boris Yakobowski, Matthieu Lemerre,
André Maroneze, Valentin Perelle, and Virgile Prevosto.
**Eva - The Evolved Value Analysis plug-in.**
<http://frama-c.com/download/frama-c-eva-manual.pdf>.
<!-- end list -->
### Thesis
- David Bühler.
**EVA, an Evolved Value Analysis for Frama-C: structuring an abstract
interpreter through value and state abstractions.**
PhD Thesis, University of Rennes 1, March 2017.
<http://http://www.theses.fr/2017REN1S016>
### Founding Articles
- Sandrine Blazy, David Bühler, and Boris Yakobowski.
**Structuring Abstract Interpreters through State and Value
Abstractions**
To be published in the proceedings of VMCAI 2017. [local
version](/assets/dokuwiki/articles/eva-vmcai2017.pdf)
*The formalization of the communication mechanism between
Abstractions**
In International Conference on Verification, Model Checking, and Abstract
Interpretation (VMCAI), January 2017.
<https://hal-cea.archives-ouvertes.fr/cea-01808886>
*Formalization of the communication mechanism between
abstractions in EVA.*
<!-- end list -->
- Richard Bonichon and Pascal Cuoq.
**A Mergeable Interval Map.**
In Studia Informatica Universalis, vol. 9, nb. 1. pp. 5--37. 2011
<http://studia.complexica.net/index.php?option=com_content&view=article&id=185%3Aa-mergeable-interval-map%20pp-5-37&catid=56%3Anumber-1&Itemid=100&lang=en>
Extended version of the paper below.
<!-- end list -->
- Richard Bonichon and Pascal Cuoq.
**Une table d'association d'intervalles fusionnable.**
In Proceedings of vingt-et-unième Journées Francophones des Langages
Applicatifs (JFLA'10). February 2010. The body of the article is in
English.
<!-- end list -->
<!-- end list -->
- Richard Bonichon and Pascal Cuoq.
**A Mergeable Interval Map.**
In Journées Francophones des Langages Applicatifs (JFLA), January 2011.
<http://studia.complexica.net/index.php?option=com_content&view=article&id=185%3Aa-mergeable-interval-map%20pp-5-37&catid=56%3Anumber-1&Itemid=100&lang=en>
*Presentation of one of the most important internal datastructure of Eva.*
<!-- end list -->
### Other Articles
- Géraud Canet, Pascal Cuoq and Benjamin Monate.
**A Value Analysis for C Programs.**
In Proceedings of the Ninth IEEE International Working Conference on
Source Code Analysis and Manipulation (SCAM'09). September 2009.
*We demonstrate the value analysis of Frama-C. Frama-C is an Open
Source static analysis framework for the C language. In Frama-C,
each static analysis technique, approach or idea can be implemented
as a new plug-in, with the opportunity to obtain information from
other plug-ins, and to leave the verification of difficult
properties to yet other plug-ins. The new analysis may in turn
provide access to the data it has computed. The value analysis of
Frama-C is a plug-in based on abstract interpretation. It computes
and stores supersets of possible values for all the variables at
each statement of the analyzed program. It handles pointers, arrays,
structs, and heterogeneous pointer casts. Besides producing
supersets of possible values for the variables at each point of the
execution, the value analysis produces run-time-error alarms. An
alarm is emitted for each operation in the analyzed program where
the value analysis cannot guarantee that there will not be a
run-time error.*
<!-- end list -->
Source Code Analysis and Manipulation (SCAM). September 2009.
*Presentation of a former version of Eva.*
<!-- end list -->
- Pascal Cuoq and Damien Doligez.
**Hashconsing in an incrementally garbage-collected system: a story
of weak pointers and hashconsing in OCaml 3.10.2.**
In Proceedings of the 2008 ACM SIGPLAN Workshop on ML (ML'08), pages
13--22, September 2008.
*This article describes the implementations of weak pointers, weak
hashtables and hashconsing in version 3.10.2 of the Objective Caml
system, with focus on several performance pitfalls and their
solutions.*
#### Other Articles
- Pascal Cuoq, Benjamin Monate, Anne Pacalet, Virgile Prevosto, John
Regehr, Boris Yakobowski and Xuejun Yang.
**Testing Static Analyzers with Randomly Generated Programs.**
In Proceedings of the 4th NASA Formal Methods Symposium (NFM 2012),
LNCS 7226, April 2012.
<!-- end list -->
In Workshop on ML, September 2008.
*This article describes weak pointers, weak hashtables and hashconsing as
implemented in OCaml and used in a former version of Eva.*
<!-- end list -->
# WP
- Pascal Cuoq, Philippe Hilsenkopf, Florent Kirchner, Sébastien Labbé,
Nguyen Thuy and Boris Yakobowski.
**Formal verification of software important to safety using the
Frama-C tool suite.**
NPIC\&HMIT 2012.
### Manual
- Patrick Baudin, François Bobot, Loïc Correnson, and Zaynah Dargaye.
**WP Plug-in Manual.**
<http://frama-c.com/download/frama-c-wp-manual.pdf>.
*The official manual for the WP plug-in.*
<!-- end list -->
- Chatzieleftheriou, G. and Katsaros, P.
**Test driving static analysis tools in search of C code
vulnerabilities.**
In Proceedings of the 6th IEEE International Workshop on Security,
Trust, and Privacy for Software Applications (STPSA'11), Munich,
Germany, IEEE Computer Society, 2011.
### Founding Articles
- Loïc Correnson.
**Qed. Computing What Remains to Be Proved.**
In NASA Formal Methods (NFM), April 2012.
*Presentation of Qed, a core library of WP that simplifies proof obligations
before sending them to provers.*
<!-- end list -->
### Tutorials
- Allan Blanchard.
** Introduction to C Program Proof with Frama-C and its WP plug-in.**
<https://allan-blanchard.fr/publis/frama-c-wp-tutorial-en>
<!-- end list -->
- Armand Puccetti.
**Static Analysis of the XEN Kernel using Frama-C.**
Journal of Universal Computer Science, volume 16, issue 4, 2010.
*In this paper, we describe the static analysis of the XEN 3.0.3
hypervisor using the Frama-C static analysis tool.*
- Jochen Burghardt and Jens Gerlach.
**ACSL by Example**.
<https://github.com/fraunhoferfokus/acsl-by-example>
*A fairly complete tour of ACSL and WP features through various functions
inspired from C++ STL.*
<!-- end list -->
- Pascal Berthomé, Karinne Heydemann, Xavier Kauffmann-Tourkestansky
and Jean-François Lalande.
**Attack model for verification of interval security properties for
smart card C codes.**
Proceedings of the 5th Workshop on Programming Languages and
Analysis for Security (PLAS'10). 2010.
*Smart card programs are subject to physical attacks that disturb
the execution of the embedded code. These attacks enable attackers
to steal valuable information or to force a malicious behavior upon
the attacked code. This paper proposes a methodology to check
interval security properties on smart card source codes. The goal is
to identify critical attacks that violate these security properties.
The verification takes place at source-level and considers all
possible attacks thanks to a proposed source-level model of physical
attacks. The paper defines an equivalence relation between attacks
and shows that a code can be divided into areas where attacks are
equivalent. Thus, verifying an interval security property
considering all the possible attacks requires to verify as many
codes as the number of equivalence classes. This paper provides a
reduction algorithm to define the classes i.e. the minimal number of
attacked codes that covers all possible attacks. The paper also
proposes a solution to make the property verification possible for
large codes or codes having unknown source parts.*
# WP
#### Manual
- Loïc Correnson and Zaynah Dargaye and Anne Pacalet.
**WP (Draft) Manual.**
<http://frama-c.com/download/frama-c-wp-manual.pdf>.
*A draft manual for the WP plug-in.*
#### Other articles
- Pascal Cuoq, Benjamin Monate, Anne Pacalet and Virgile Prevosto.
**Functional Dependencies of C Functions via Weakest
Pre-Conditions**
International Journal on Software Tools for Technology Transfer
(STTT), edition VSTTE 2009-2010,
**Functional Dependencies of C Functions via Weakest Pre-Conditions**
In International Journal on Software Tools for Technology Transfer
(STTT), 2010,
[SpringerLink](http://www.springerlink.com/content/yj344380377p4011/)
[More information](functional_dependencies)
<!-- end list -->
# E-ACSL
### Manual
- Julien Signoles and Kostyantyn Vorobyov.
**E-ACSL User Manual.**
<http://frama-c.com/download/e-acsl/e-acsl-manual.pdf>.
*The official manual of the Frama-C plug-in E-ACSL.*
<!-- end list -->
- Arnaud Dieumegard and Marc Pantel.
**Vérification d’un générateur de code par génération
d’annotations.**
Conférence en IngénieriE du Logiciel (CIEL), Juin 2012.
<http://gpl2012.irisa.fr/sites/default/files/CIEL2012-Dieumegard-paper34.pdf>
- Allan Blanchard.
**Introduction to C Program Proof using Frama-C and its WP Plugin.**
WP tutorial, available at <http://allan-blanchard.fr/teaching.html>.
- Julien Signoles.
**E-ACSL: Executable ANSI/ISO C Specification Language.**
<http://frama-c.com/download/e-acsl/e-acsl.pdf>.
*The reference manual of the E-ACSL specification language.*
<!-- end list -->
### Thesis
- Julien Signoles.
**From Static Analysis to Runtime Verification with Frama-C and E-ACSL.**
Habilitation Thesis, University of Paris Sud, July 2018.
<http://julien.signoles.free.fr/publis/hdr.pdf>
<!-- end list -->
#### Founding Articles
- Julien Signoles, Nikolai Kosmatov, and Kostyantyn Vorobyov.
**E-ACSL, a Runtime Verification Tool for Safety and Security of C Programs.
Tool Paper.**
In International Workshop on Competitions, Usability, Benchmarks, Evaluation,
and Standardisation for Runtime Verification Tools (RV-CuBES), September 2017.
<http://julien.signoles.free.fr/publis/2017_rvcubes_tool.pdf>
*An overview of the E-ACSL plug-in.*
<!-- end list -->
- Kostyantyn Vorobyov, Julien Signoles, and Nikolai Kosmatov.
Shadow state encoding for efficient monitoring of block-level properties.
In International Symposium on Memory Management (ISMM), June 2017.
<http://julien.signoles.free.fr/publis/2017_ismm.pdf>
*Presentation of the shadow memory technique used by E-ACSL to monitor
memory properties.*
<!-- end list -->
- Mickaël Delahaye, Nikolaï Kosmatov and Julien Signoles.
**Common Specification Language for Static and Dynamic Analysis of C
Programs.**
In Proceedings of Symposium on Applied Computing 2013 (SAC), March 2013.
<http://kosmatov.perso.sfr.fr/nikolai/publications/delahaye_ks_sac_2013.pdf>
*An overview of the specification language.*
<!-- end list -->
#### Other Articles
- Kostyantyn Vorobyov, Nikolai Kosmatov, and Julien Signoles.
**Detection of Security Vulnerabilities in C Code using Runtime
Verification.**
In International Conference on Tests and Proofs (TAP), June 2018.
<http://julien.signoles.free.fr/publis/2018_tap_vorobyov.pdf>
*Explore how some runtime verification tools (including E-ACSL) may detect
security vulnerabilities.*
<!-- end list -->
- Kostyantyn Vorobyov, Nikolai Kosmatov, Julien Signoles, and Arvid Jakobsson.
**Runtime detection of temporal memory errors.**
In International Conference on Runtime Verification (RV), September 2017.
<http://julien.signoles.free.fr/publis/2017_rv.pdf>
<!-- end list -->
- Nikolaï Kosmatov, Guillaume Petiot and Julien Signoles.
**An Optimized Memory Monitoring for Runtime Assertion Checking of C
Programs.**
In Proceedings of Runtime Verification 2013 (RV), September 2013.
*Presentation of the runtime memory model used by a former version of
E-ACSL.*
<!-- end list -->
# Jessie
#### Manual
......@@ -616,54 +579,6 @@ detecting loss of separation among aircraft.*
showing the use of Aoraï in generating a threat scenario in a
driver.
# E-ACSL
#### Manual
- Julien Signoles.
**E-ACSL User Manual.**
<http://frama-c.com/download/e-acsl/e-acsl-manual.pdf>.
*The official manual of the Frama-C plug-in E-ACSL.*
<!-- end list -->
- Julien Signoles.
**E-ACSL: Executable ANSI/ISO C Specification Language. Version
1.7.**
<http://frama-c.com/download/e-acsl/e-acsl.pdf>.
*The reference manual of the E-ACSL specification language.*
<!-- end list -->
- Julien Signoles.
**E-ACSL Version 1.7. Implementation in Frama-C Plug-in E-ACSL
version 0.3.**
<http://frama-c.com/download/e-acsl/e-acsl-implementation.pdf>.
*What part of the E-ACSL specification language is currently
implemented in the E-ACSL plug-in.*
#### Founding Articles
- Mickaël Delahaye, Nikolaï Kosmatov and Julien Signoles.
**Common Specification Language for Static and Dynamic Analysis of C
Programs.**
In Proceedings of Symposium on Applied Computing 2013 (SAC'13),
March 2013.
<http://kosmatov.perso.sfr.fr/nikolai/publications/delahaye_ks_sac_2013.pdf>.
<!-- end list -->
- Nikolaï Kosmatov, Guillaume Petiot and Julien Signoles.
**An Optimized Memory Monitoring for Runtime Assertion Checking of C
Programs.**
In Proceedings of Runtime Verification 2013 (RV'13), September 2013.
#### Other Article
- Nikolaï Kosmatov and Julien Signoles.
**A Lesson on Runtime Assertion Checking with Frama-C. RV 2013
Tutorial.**
In Proceedings of Runtime Verification 2013 (RV'13), September 2013.
# Security Slicing
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment