diff --git a/dokuwiki/publications.md b/dokuwiki/publications.md
deleted file mode 100644
index 2bacbb4680edf15292879b6df4f2be0240b50d8f..0000000000000000000000000000000000000000
--- a/dokuwiki/publications.md
+++ /dev/null
@@ -1,798 +0,0 @@
----
-layout: clean_page
-title: Publications
----
-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
-
-#### Manuals
-
- - 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.*
- - 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.*
- - 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.*
-
-#### Founding Articles
-
- - 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.
- - Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto,
- Julien Signoles, and Boris Yakobowski.\
- **Frama-C, A Software Analysis Perspective.**\
- In proceedings of International Conference on Software Engineering
- 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.*
-
-#### 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.*
- - 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), 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.*
- - 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.*
- - 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 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.*
- - 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.*
- - 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.*
- - Julien Signoles.\
- **Foncteurs impératifs et composés: la notion de projets dans
- 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.*
-
-#### 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>
- - 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>
-
-# 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>.
-
-#### 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**\
- 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.*
- - 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.*
-
-#### 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). September 2009.\
- *Presentation of a former version of Eva.*
- - 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 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.*
-
-# WP
-
-#### 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.*
-
-#### 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.*
-
-#### 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.pdf>\
- *A comprehensive tutorial on how to prove C programs with Frama-C and WP.*
- - 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.*
-
-#### Other articles
-
- - Pascal Cuoq, Benjamin Monate, Anne Pacalet and Virgile Prevosto.\
- **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)
-
-# 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.*
- - 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.*
-
-#### 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>
-
-#### 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.*
- - 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.*
- - 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.*
-
-#### 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.*
- - 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>
- - 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.*
- - Dara Ly, Nikolai Kosmatov, Julien Signoles and Frédéric Loulergue.\
- **Soundness of a Dataflow Analysis for Memory Monitoring.**\
- In Workshop on Languages and Tools for Ensuring Cyber-Resilience in
- Critical Software-Intensive Systems (HILT) , November 2018.\
- <https://hal.archives-ouvertes.fr/cea-02283406/>
- - Dara Ly, Nikolai Kosmatov, Frédéric Loulergue and Julien Signoles.\
- **Verified Runtime Assertion Checking for Memory Properties.**\
- In International Conference on Tests and Proofs (TAP), June 2020.\
- <https://hal-cea.archives-ouvertes.fr/cea-02879211>
-
-# Aoraï
-
-##### Manual
-
- - Nicolas Stouls.\
- **Aoraï Plug-in Tutorial.**\
- <http://frama-c.com/download/aorai/aorai-manual.pdf>.\
- *The official manual of the Frama-C plug-in Aoraï.*
-
-##### Founding Article
-
- - Julien Groslambert and Nicolas Stouls.\
- **Vérification de propriétés LTL sur des programmes C par génération
- d'annotations.**\
- <http://hal.archives-ouvertes.fr/inria-00568947/>\
- In Proceedings of Approches Formelles dans l'Assistance au
- Développement de Logiciels 2009 (AFADL'09), January 2009. In
- French.
-
-# Security Slicing
-
-##### Founding Article
-
- - Benjamin Monate and Julien Signoles.\
- **Slicing for Security of Code.**\
- In Proceedings of the 1st international conference on Trusted
- Computing and Trust in Information Technologies (TRUST'08), pages
- 133--142, March 2008.\
- *Bugs in programs implementing security features can be catastrophic: for example they may be exploited by malign users to gain access to sensitive data. These exploits break the confidentiality of information. All security analyses assume that softwares implementing security features correctly implement the security policy,* i.e. *are security bug-free. This assumption is almost always wrong and IT security administrators consider that any software that has no security patches on a regular basis should be replaced as soon as possible. As programs implementing security features are usually large, manual auditing is very error prone and testing techniques are very expensive. This article proposes to reduce the code that has to be audited by applying a program reduction technique called* slicing *. Slicing transforms a source code into an equivalent one according to a set of criteria. We show that existing slicing criteria do* not *preserve the confidentiality of information. We introduce a new automatic and correct source-to-source method properly preserving the confidentiality of information* i.e. *confidentiality is guaranteed to be exactly the same in the original program and in the sliced program.*
-
-# Internal Plug-ins at CEA
-
-### Cfp
-
-#### Founding Articles
-
- - Michele Alberti and Julien Signoles.\
- **Context Generation from Formal Specifications for C Analysis Tools.**\
- In Logic-based Program Synthesis and Transformation (LOPSTR), October 2017.\
- <http://julien.signoles.free.fr/publis/2017_lopstr.pdf>\
- Best paper award.
-
-### MetACSL
-
-#### Founding Articles
-
- - Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, and
- Pascale Le Gall.\
- **MetAcsl: Specification and Verification of High-Level Properties.**\
- In International Conference on Tools and Algorithms for the Construction
- and Analysis of Systems (TACAS), April 2019.\
- <https://hal-cea.archives-ouvertes.fr/cea-02019790>
-
- - Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling and
- Pascale Le Gall.\
- **Tame Your Annotations with MetAcsl: Specifying, Testing and Proving
- High-Level Properties.**\
- In Tests and Proofs (TAP), 13th International Conference, October 2019.\
- <https://hal.archives-ouvertes.fr/cea-02301892/>
-
-### PathCrawler
-
-##### Manual
-
- - **PathCrawler Automatic Test Generation Tool For C Programs User Manual Version 3.1.**\
- <http://frama-c.com/download/frama-c-pathcrawler.pdf>.\
- *The user manual of the Frama-C plug-in PathCrawler.*
-
-##### Founding Articles
-
- - Nicky Williams, Bruno Marre and Patricia Mouy.\
- **On-the-fly generation of k-paths tests for C functions :
- towards the automation of grey-box testing.**\
- In International Conference on Automated Software Engineering (ASE),
- September 2004.\
- <http://pathcrawler-online.com/pubs/ase04copy.pdf>\
- The final publication is available from IEEE\
- <http://doi.ieeecomputersociety.org/10.1109/ASE.2004.10020>
- - Nicky Williams, Bruno Marre, Patricia Mouy and Muriel Roger.\
- **PathCrawler: automatic generation of path tests by combining
- static and dynamic analysis.**\
- In European Dependable Computing Conference (EDCC-5), April 2005.\
- <http://pathcrawler-online.com/pubs/edcc05.pdf>\
- The final publication is available at www.springerlink.com.\
- <http://dx.doi.org/10.1007/11408901_21>
-
-
-##### Tutorials
-
- - Nicky Williams and Nikolai Kosmatov.\
- **Structural Testing with PathCrawler. Tutorial Synopsis.**\
- In International Conference on Quality Software (QSIC), August 2012.\
- <http://pathcrawler-online.com/pubs/qsic12copy.pdf>\
- The final publication will be available from IEEE.\
- <http://www.ieee.org>
- - Nikolai Kosmatov, Nicky Williams, Bernard Botella, Muriel Roger,
- Omar Chebaro.\
- **A Lesson on Structural Testing with PathCrawler-online.com.**\
- In International Conference on Tests and Proofs (TAP), May 2012.\
- <http://pathcrawler-online.com/pubs/tap_2012_pconline_final.pdf>\
- The final publication is available at www.springerlink.com.\
- <http://dx.doi.org/10.1007/978-3-642-30473-6_15>
-
-##### Other Articles
-
- - Nicky Williams.\
- **WCET measurement using modified path testing.**\
- In International Workshop on Worst-Case Execution Time Analysis (WCET),
- July 2005.\
- <http://pathcrawler-online.com/pubs/wcet05.pdf>\
- The final publication is available at DROPS.
- <http://drops.dagstuhl.de/opus/volltexte/2007/809>
- - Patricia Mouy, Bruno Marre, Nicky Williams and Pascale Le Gall.\
- **Generation of all-paths unit test with function calls.**\
- In International Conference on Software Testing, Verification, and
- Validation (ICST), April 2008.\
- <http://pathcrawler-online.com/pubs/icst08copy.pdf>\
- The final publication is available from IEEE.\
- <http://doi.ieeecomputersociety.org/10.1109/ICST.2008.35>
- - Nikolai Kosmatov.\
- **All-paths test generation for programs with internal aliases.**\
- In International Symposium on Software Reliability Engineering
- (ISSRE), November 2008.\
- <http://pathcrawler-online.com/pubs/issre08copy.pdf>\
- The final publication is available from IEEE.\
- <http://dx.doi.org/10.1109/ISSRE.2008.25>
- - Bernard Botella, Mickaël Delahaye, Stéphane Hong-Tuan-Ha, Nikolai
- Kosmatov, Patricia Mouy, Muriel Roger and Nicky Williams.\
- **Automating Structural Testing of C Programs: Experience with
- PathCrawler.**\
- In International Workshop on Automation of Software Test (AST), May 2009.\
- <http://pathcrawler-online.com/pubs/ast09industrycopy.pdf>\
- The final publication is available from IEEE.\
- <http://dx.doi.org/10.1109/IWAST.2009.5069043>
- - Nicky Williams and Muriel Roger.\
- **Test Generation Strategies to Measure Worst-Case Execution
- Time.**\
- In International Workshop on Automation of Software Test (AST), May 2009.\
- <http://pathcrawler-online.com/pubs/ast09researchcopy.pdf>\
- The final publication is available from IEEE.\
- <http://dx.doi.org/10.1109/IWAST.2009.5069045>
- - Nikolai Kosmatov.\
- **On Complexity of All-Paths Test Generation. From Practice to
- Theory.**\
- In Testing: Academic and Industrial Conference - Practice and
- Research Techniques (TAIC PART 2009), September 2009.\
- <http://pathcrawler-online.com/pubs/taic09copy.pdf>\
- The final publication is available from IEEE.\
- <http://dx.doi.org/10.1109/TAICPART.2009.26>
- - Nicky Williams.\
- **Abstract path testing with PathCrawler.**\
- <http://doi.acm.org/10.1145/1808266.1808272>
- - Nikolai Kosmatov, Bernard Botella, Muriel Roger and Nicky
- Williams.\
- **Online Test Generation with PathCrawler. Tool demo.**\
- Best demo award.\
- In International Workshop on Constraints in Software Testing, Verification,
- and Analysis (CSTVA 2011), March 2011.\
- <http://pathcrawler-online.com/pubs/kosmatov_brw_cstva_2011copy.pdf>\
- The final publication is available from IEEE.\
- <http://dx.doi.org/10.1109/ICSTW.2011.85>
-
-
-### RPP
-
-##### Founding Articles
-
- - Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall and Virgile Prevosto.\
- **RPP: Automatic Proof of Relational Properties by Self-composition.**\
- In Tools and Algorithms for the Construction and Analysis of Systems
- 23rd International Conference, {TACAS} 2017.\
- <https://hal-cea.archives-ouvertes.fr/cea-01808885>
- - Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto and
- Guillaume Petiot.\
- **Static and Dynamic Verification of Relational Properties on
- Self-composed C Code.**\
- In Tests and Proofs - 12th International Conference, TAP@STAF 2018.\
- <https://hal-cea.archives-ouvertes.fr/cea-01835470>
-
-##### Thesis
-
- - Lionel Blatter.\
- **Relational properties for specification and verification of C programs in Frama-C.**\
- PhD Thesis, University of Paris Saclay, December 2019.\
- <http://http://www.theses.fr/2017REN1S016>
-
-### SecureFlow
-
-##### Thesis
-
- - Mounir Assaf.\
- **From qualitative to quantitative program analysis: permissive enforcement of secure information flow.**\
- PhD Thesis, University of Rennes 1, May 2015.\
- <http://http://www.theses.fr/2015REN1S003>
-
-##### Founding Articles
-
- - Gergö Barany and Julien Signoles.\
- **Hybrid Information Flow Analysis for Real-World C Code.**\
- In International Conference on Tests and Proofs (TAP), July 2017.\
- <http://julien.signoles.free.fr/publis/2017_tap.pdf>
- - Mounir Assaf, Julien Signoles, Éric Totel, and Frédéric Tronel.\
- **Program transformation for non-interference verification on programs
- with pointers.**\
- In International Information Security and Privacy Conference (SEC), July 2013.\
- <http://julien.signoles.free.fr/publis/2013_sec.pdf>\
- Best student paper award.
-
-# External Plug-ins
-
-These publications are related to Frama-C plug-ins which are not
-available from the official Frama-C website (<http://frama-c.com>).
-These plug-ins may be either closed or open source.
-
-
-### Jessie
-
-#### Manual
-
- - The main web page, including the manual and many other resources, is
- <http://krakatoa.lri.fr/>
-
-#### Thesis
-
- - Yannick Moy.\
- **Automatic Modular Static Safety Checking for C Programs.**\
- Phd Thesis. January 2009.\
- <http://www.lri.fr/~marche/moy09phd.pdf>.
- - François Bobot.\
- **Logique de séparation et vérification déductive.**\
- Thèse de doctorat, Université Paris-Sud, December 2011.\
- <http://proval.lri.fr/publications/bobot11these.pdf>
- - Romain Bardou.\
- **Verification of Pointer Programs Using Regions and
- Permissions.**\
- Thèse de doctorat, Université Paris-Sud, October 2011.
- <http://proval.lri.fr/publications/bardou11phd.pdf>.
-
-#### Founding Articles
-
- - Yannick Moy and Claude Marché.\
- **Modular inference of subprogram contracts for safety checking.**\
- In Journal of Symbolic Computation, 2010.\
- <http://hal.inria.fr/inria-00534331/en>
- - Sylvie Boldo and Thi Minh Tuyen Nguyen.\
- **Hardware-independent proofs of numerical programs.**\
- In Proceedings of the Second NASA Formal Methods Symposium, April 2010.\
- <http://shemesh.larc.nasa.gov/NFM2010/proceedings/NASA-CP-2010-216215.pdf>
- - Ali Ayad.\
- **On formal methods for certifying floating-point C programs.**\
- Research Report RR-6927, INRIA, 2009.\
- <http://hal.inria.fr/inria-00383793/en/>
- - Yannick Moy.\
- **Sufficient Preconditions for Modular Assertion Checking.**\
- In Proceedings of the 9th International Conference on Verification,
- Model Checking, and Abstract Interpretation (VMCAI'08). January 2008.\
- *Assertion checking is the restriction of program verification to
- validity of program assertions. It encompasses safety checking,
- which is program verification of safety properties, like memory
- safety or absence of overflows. In this paper, we consider assertion
- checking of program parts instead of whole programs, which we call
- modular assertion checking. Classically, modular assertion checking
- is possible only if the context in which a program part is executed
- is known. By default, the worst-case context must be assumed, which
- may impair the verification task. It usually takes user effort to
- detail enough the execution context for the verification task to
- succeed, by providing strong enough preconditions. We propose a
- method to automatically infer sufficient preconditions in the
- context of modular assertion checking of imperative pointer
- programs. It combines abstract interpretation, weakest precondition
- calculus and quantifier elimination. We instantiate this method to
- prove memory safety for C and Java programs, under some memory
- separation conditions.*
- - Yannick Moy.\
- **Checking C Pointer Programs for Memory Safety.**\
- INRIA Research Report n°6334, October 2007.\
- *We propose an original approach for checking memory safety of C
- pointer programs that do not include casts, structures, double
- indirection and memory deallocation. This involves first identifying
- aliasing and strings, which we do in a local setting rather than
- through a global analysis as it is done usually. Our separation
- analysis in particular is a totally new treatment of non-aliasing.
- We present for the first time two abstract lattices to deal with
- local pointer aliasing and local pointer non-aliasing in an abstract
- interpretation framework. The key feature of our work is to combine
- abstract interpretation techniques and deductive verification. The
- approach is modular and contextual, thanks to the use of Hoare-style
- annotations (pre- and postconditions), allowing to verify each C
- function independently. Abstract interpretation techniques are used
- to automatically generate such annotations, in an idiomatic way:
- standard practice of C programming is identified and incorporated as
- heuristics. Abstract interpretation and deductive verification are
- both used to check these annotations in a sound way. Our first
- contribution is the design of an abstract domain for implications,
- which makes it possible to build efficient contextual analyses. Our
- second contribution is an efficient back-and-forth propagation
- method to generate contextual annotations in a modular way, in the
- framework of abstract interpretation. It considers the safety
- conditions to prove as a starting point, which focuses the analysis
- on the paths of interest. Thanks to previously unknown loop
- refinement operators, this propagation method does not require
- iterating around loops. We implemented our method in Caduceus, a
- tool for the verification of C programs, and successfully verified
- automatically the C standard string library functions.*
- - Yannick Moy.\
- **Union and Cast in Deductive Verification.**\
- In Proceedings of the C/C++ Verification Workshop (CCV'07), July 2007.\
- *Deductive verification based on weakest-precondition calculus has
- proved effective at proving imperative programs, through a suitable
- encoding of memory as functional arrays (a.k.a. the Burstall-Bornat
- model). Unfortunately, this encoding of memory makes it impossible
- to support features like union and cast in C. We show that an
- interesting subset of those unions and casts can be encoded as
- structure subtyping, on which it is possible to extend the Burstall-
- Bornat encoding. We present an automatic translation from C to an
- intermediate language Jessie on which this extended interpretation
- is performed.*
- - Yannick Moy and Claude Marché.\
- **Inferring local (non-)aliasing and strings for memory safety.**\
- In Proceedings of Heap Analysis and Verification (HAV’07), Braga,
- Portugal, March 2007.\
- *We propose an original approach for checking memory safety of C
- pointer programs, by combining deductive verification and abstract
- interpretation techniques. The approach is modular and contextual,
- thanks to the use of Hoare-style annotations (pre- and
- postconditions), allowing us to verify each C function
- independently. Deductive verification is used to check these
- annotations in a sound way. Abstract interpretation techniques are
- used to automatically generate such annotations, in an idiomatic
- way: standard practice of C programming is identified and
- incorporated as heuristics. Our first contribution is a set of
- techniques for identifying aliasing and strings, which we do in a
- local setting rather than through a global analysis as it is done
- usually. Our separation analysis in particular is a totally new
- treatment of non-aliasing. We present for the first time two
- abstract lattices to deal with local pointer aliasing and local
- pointer non-aliasing in an abstract interpretation framework. Our
- second contribution is the design of an abstract domain for
- implications, which makes it possible to build efficient contextual
- analyses. Our last contribution is an efficient back-and-forth
- propagation method to generate contextual annotations in a modular
- way, in the framework of abstract interpretation. We implemented our
- method in Caduceus, a tool for the verification of C programs, and
- successfully generated appropriate annotations for the C standard
- string library functions.*
- - Thierry Hubert and Claude Marché.\
- **Separation analysis for deductive verification.**\
- In Heap Analysis and Verification (HAV'07), pages 81-93, Braga,
- Portugal, March 2007.\
- <http://www.lri.fr/~marche/hubert07hav.pdf>
-
-#### Other Articles
-
- - Jochen Burghardt, Jens Gerlach, Hans Pohl and Juan Soto.\
- **An Experience Report on the Verification of Algorithms in the C++ Standard Library using Frama-C.**\
- In First Proceedings of International Conference of Formal
- Verification of Object-Oriented Software (FoVeOOS'10), June 2010.\
- *Over the past few years, we have been conducting assessment studies
- to determine the utility of the Frama-C/Jessie platform of software
- analyzers (in conjunction with automatic theorem provers) for the
- formal verification of software. In this experience report, we
- discuss experiments in the verification of algorithms in the C++
- Standard Library based on tool-supported Hoare-style weakest
- precondition computations to formally prove ACSL (ANSI/ISO C
- Specification Language) properties. Often automated provers are
- unable to perform inductive proofs. Hence, we introduce an approach
- to guide automated provers to find an inductive proof using
- auxiliary C-code corresponding to the proof structure. We also
- present a method to verify that a function only permutes the
- contents of an array, and obtain the relation between the pre- and
- post-index for each array element for use in later specification
- properties. Furthermore, we describe an approach to prove the
- essential properties of a function independent of each other,
- supplying for each task only the assumptions actually needed, i.e.,
- related to the current goal. This approach reduces the proof search
- space and leads to higher verification rates for automatic provers.
- However, additional methods and tool support are desired to overcome
- drawbacks from a software engineering point of view. Finally, we
- sketch some ideas for an extension of ACSL for C++.*
- - Stéphane Duprat, Pierre Gaufillet, Victoria Moya Lamiel and Frédéric
- Passarello.\
- **Formal verification of SAM state machine implementation.**\
- In Proceedings of Embedded Real Time Software and Systems
- (ERTS²'10), May 2010.\
- <http://www.erts2010.org/Site/0ANDGY78/Fichier/PAPIERS%20ERTS%202010/ERTS2010_0053_final.pdf>\
- *This paper reports the results of an experiment about the formal
- verification of source code made according to an EMF model. Models
- define the semantics of a system whereas the source code defines its
- implementation. We applied this solution to a model of Automaton in
- SAM language and its C language implementation. The technical
- environment is close to an industrial operational context and all
- the tools are available. The experimentation has succeeded and has
- to be consolidated with bigger cases before an introduction in the
- operational development process. More generally, this solution must
- be extended to other model languages.*
- - Murat Torlakcik.\
- **Contracts in OpenBSD.**\
- Msc. Dissertation Report, April 2010.\
- <http://kindsoftware.com/documents/reports/Torlakcik10.pdf>.
- - Franck Butelle, Florent Hivert, Micaela Mayero and Frédéric
- Toumazet.\
- **Formal Proof of SCHUR Conjugate Function.**\
- In 17th Symposium on the Integration of Symbolic Computation and
- Mechanised Reasoning (CALCULEMUS 2010).\
- <http://www-lipn.univ-paris13.fr/~mayero/publis/Calculemus2010.pdf>
- - Nikolai Kosmatov, Virgile Prevosto and Julien Signoles.\
- **Specification and Proof of Programs with Frama-C. SAC 2013 Tutorial**\
- In 28th ACM Symposium on Applied Computing (SAC), March 2013.\
- <http://www.acm.org/conferences/sac/sac2013/T4.pdf>\
- [Slides](http://www.acm.org/conferences/sac/sac2013/T4-Handout.pdf)
- - Alwyn Goodloe, César A. Muñoz, Florent Kirchner, Loïc Correnson.\
- **Verification of Numerical Programs: From Real Numbers to Floating
- Point Numbers.**\
- In NASA Formal Methods 2013.\
- *Usually, proofs involving numerical computations are conducted in the infinitely precise realm of the field of real numbers. However, numerical computations in these algorithms are often implemented using floating point numbers. The use of a finite representation of real numbers introduces uncertainties as to whether the properties verified in the theoretical setting hold in practice. This short paper describes work in progress aimed at addressing these concerns. Given a formally proven algorithm, written in the Program Verification System(PVS), the Frama-C suite of tools is used to identify sufficient conditions and verify that under such conditions the rounding errors arising in a C implementation of the algorithm do not affect its correctness. The technique is illustrated using an algorithm for detecting loss of separation among aircraft.*
-
-### Cost
-
- - Nicolas Ayache, Roberto M. Amadio and Yann Régis-Gianas.\
- **Certifying and reasoning on cost annotations in C programs.**\
- In Proceedings of the 17th International Workshop on Formal Methods
- for Industrial Critical Systems (FMICS 2012), Paris, France, August 2012.\
- <http://hal.inria.fr/hal-00702665>\
- *We present a so-called labelling method to enrich a compiler in
- order to turn it into a “cost annotating compilerâ€, that is, a
- compiler which can lift pieces of information on the execution cost
- of the object code as cost annotations on the source code. These
- cost annotations characterize the execution costs of code fragments
- of constant complexity. ... we present a Frama-C plugin that uses
- our cost annotating compiler to automatically infer trustworthy
- logic assertions about the concrete worst case execution cost of
- programs written in a fragment of the C language. ... We report our
- experimentations on some C programs, especially programs generated
- by a compiler for the synchronous programming language Lustre used
- in critical embedded software.*
-
-### Fan-C
-
- - Pascal Cuoq, David Delmas, Stéphane Duprat and Victoria Moya
- Lamiel.\
- **Fan-C, a Frama-C plug-in for data flow verification.**\
- In Proceedings of Embedded Real Time Software and Systems
- (ERTS'12).\
- <http://www.erts2012.org/Site/0P2RUC89/5C-3.pdf>
-
-### SANTE
-
- - Omar Chebaro, Nikolaï Kosmatov, Alain Giorgetti and Jacques
- Julliand.\
- **The SANTE Tool: Value Analysis, Program Slicing and Test
- Generation for C Program Debugging.**\
- In Proceedings of the 5th International Conference on Tests & Proofs
- (TAP 2011), Zurich, Switzerland, June 2011.\
- *This short paper presents a prototype tool called SANTE (Static
- ANalysis and TEsting) implementing an original method combining
- value analysis, program slicing and structural test generation for
- verification of C programs. First, value analysis is called to
- generate alarms when it can not guarantee the absence of errors.
- Then the program is reduced by program slicing. Alarm-guided test
- generation is then used to analyze the simplified program(s) in
- order to confirm or reject alarms.*
- - Omar Chebaro, Nikolaï Kosmatov, Alain Giorgetti and Jacques
- Julliand.\
- **Combining static analysis and test generation for C program
- debugging.**\
- In Proceedings of the 4th International Conference on Tests & Proofs
- (TAP 2010), pages 94-100, Malaga, Spain, July 2010.\
- *This paper presents our ongoing work on a tool prototype called
- SANTE (StaticANalysis and TEsting), implementing a combination of
- static analysis and structural program testing for detection of
- run-time errors in C programs. First, a static analysis tool
- (Frama-C) is called to generate alarms when it cannot ensure the
- absence of run-time errors. Second, these alarms guide a structural
- test generation tool (PathCrawler) trying to confirm alarms by
- activating bugs on sometest cases.Our experiments on real-life
- software showthat this combination can outperform the use of each
- technique independently.*
- - Omar Chebaro.\
- **Outil SANTE : Détection d’erreurs par analyse statique et test
- structurel des programmes C.**\
- In Proceedings of 10iemes Journées Francophones Internationales sur
- les Approches Formelles dans l'Assistance au Développement de
- Logiciels (AFADL'10), pages 75-79. June 2010. In French.
- - Omar Chebaro, Nikolaï Kosmatov, Alain Giorgetti and Jacques
- Julliand.\
- **Program slicing enhances a verification technique combining static
- and dynamic analysis.**\
- In Proceedings of the 27th Symposium On Applied Computing (SAC
- 2012), pages 1284-1291, Trento, Italy, March 2012.\
- *Recent research proposed efficient methods for software
- verification combining static and dynamic analysis, where static
- analysis reports possible runtime errors (some of which may be false
- alarms) and test generation confirms or rejects them. However, test
- generation may time out on real-sized programs before confirming
- some alarms as real bugs or rejecting some others as unreachable. To
- overcome this problem, we propose to reduce the source code by
- program slicing before test generation. This paper presents new
- optimized and adaptive usages of program slicing, provides
- underlying theoretical results and the algorithm these usages rely
- on. The method is implemented in a tool prototype called sante
- (Static ANalysis and TEsting). Our experiments show that our method
- with program slicing outperforms previous combinations of static and
- dynamic analysis. Moreover, simplifying the program makes it easier
- to analyze detected errors and remaining alarms. To appear.*
-
-### SIDAN
-
- - Jonathan-Christopher Demay, Éric Totel and Frédéric Tronel.\
- **SIDAN: a tool dedicated to Software Instrumentation for Detecting
- Attacks on Non-control-data.**\
- 4th International Conference on Risks and Security of Internet and
- Systems (CRISIS'2009), October 2009.
-
-### STAC
-
- - Dumitru Ceara, Laurent Mounier and Marie-Laure Potet.\
- **Taint Dependency Sequences: a characterization of insecure
- execution paths based on input-sensitive cause sequences.**\
- Modeling and Detecting Vulnerabilities workshop (MDV'10), associated
- to ICST 2010, April 2010.
-
-### Taster
-
- - David Delmas, Stéphane Duprat, Victoria Moya Lamiel and Julien
- Signoles.\
- **Taster, a Frama-C plug-in to enforce Coding Standards.**\
- In Proceedings of Embedded Real Time Software and Systems (ERTS'10),
- May 2010.\
- <http://web.archive.org/web/20110726034209/http://www.erts2010.org/Site/0ANDGY78/Fichier/PAPIERS%20ERTS%202010/ERTS2010_0003_final.pdf>\
- *Enforcing Coding Standards is part of the traditional concerns of
- industrial software developments. In this paper, we present a
- framework based on the open source Frama-C platform for easily
- developing syntactic, typing (and even some semantic) analyses of C
- source code, among which conformance to Coding Standards. We report
- on our successful attempt to develop a Frama-C plug-in named Taster,
- in order to replace a commercial, off-the-shelf, legacy tool in the
- verification process of several Airbus avionics software products.
- We therefore present the types of coding rules to be verified, the
- Frama-C platform and the Taster plug-in. We also discuss ongoing
- industrial deployment and qualification activities.*
diff --git a/dokuwiki/start.md b/dokuwiki/start.md
index 7d9fc7b7abf9d01421222f4b7353f67568854e77..ceb57e6e57080613956a1c8001b230aa22ee1d9a 100644
--- a/dokuwiki/start.md
+++ b/dokuwiki/start.md
@@ -94,7 +94,7 @@ modalities are described in this [document](https://git.frama-c.com/pub/frama-c/
# Works about Frama-C
- - [List of publications](/dokuwiki/publications.html)
+ - [List of publications](/html/publications.html)
- [Exercises](/dokuwiki/exercises.html)
- [Teaching](/dokuwiki/teaching.html)
- [Tutorials](/dokuwiki/tutorial.html)
diff --git a/html/documentation.html b/html/documentation.html
index ce03825a097db19e2559eb722fa8c80017996d0a..bfa5274456643c0f70b53ea191cec9734f437255 100755
--- a/html/documentation.html
+++ b/html/documentation.html
@@ -57,7 +57,7 @@ title: Documentation - Frama-C
<div class="tile">
<h4 class="tileTitle"><span>About Frama-C</span></h4>
<ul>
- <li><a href="/dokuwiki/publications.html">List of publications</a></li>
+ <li><a href="/html/publications.html">List of publications</a></li>
<li><a href="/dokuwiki/exercises.html">Exercices</a></li>
<li><a href="/dokuwiki/teaching.html">Teaching</a></li>
<li><a href="/dokuwiki/tutorial.html">Tutorials</a></li>