From c124e368a44ba2aa59bab28d65fb15b70608c6fd Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 27 Aug 2020 08:12:52 +0200
Subject: [PATCH] Changes publications subsections titles
---
.../aorai/{founding => foundational}/2009-afadl-gs.md | 2 +-
.../c2s/{founding => foundational}/2016-scam-bkll.md | 2 +-
.../c2s/{founding => foundational}/2017-vpt-blk.md | 2 +-
.../cfp/{founding => foundational}/2017-lopstr-as.md | 2 +-
.../cost/{founding => foundational}/2012-fmics-amarg.md | 2 +-
.../e-acsl/{founding => foundational}/2013-sac-dks.md | 2 +-
.../e-acsl/{founding => foundational}/2017-ismm-vsk.md | 2 +-
.../e-acsl/{founding => foundational}/2017-rvcubes-skv.md | 2 +-
.../e-acsl/{founding => foundational}/2020-rv-kms.md | 2 +-
.../eva/{founding => foundational}/2011-jfla-bc.md | 2 +-
.../eva/{founding => foundational}/2019-vmcai-bby.md | 2 +-
.../fanc/{founding => foundational}/2012-erts-cddml.md | 2 +-
.../general/{founding => foundational}/2012-sefm-ckkpsy.md | 2 +-
.../general/{founding => foundational}/2015-fac-kkpsy.md | 2 +-
.../jessie/{founding => foundational}/2007-ccv-m.md | 2 +-
.../jessie/{founding => foundational}/2007-hav-hm.md | 2 +-
.../jessie/{founding => foundational}/2007-hav-mm.md | 2 +-
.../jessie/{founding => foundational}/2007-inria-m.md | 2 +-
.../jessie/{founding => foundational}/2008-vmcai-m.md | 2 +-
.../jessie/{founding => foundational}/2009-inria-a.md | 2 +-
.../jessie/{founding => foundational}/2010-jsc-mm.md | 2 +-
.../jessie/{founding => foundational}/2010-nfm-bn.md | 2 +-
.../metacsl/{founding => foundational}/2019-tacas-rkprlg.md | 2 +-
.../metacsl/{founding => foundational}/2019-tap-rkvrlg.md | 2 +-
.../pathcrawler/{founding => foundational}/2004-ase-wmm.md | 2 +-
.../{founding => foundational}/2005-edcc-wmmr.md | 2 +-
.../rpp/{founding => foundational}/2017-tacas-bklgp.md | 2 +-
.../rpp/{founding => foundational}/2018-tap-bklgpp.md | 2 +-
.../rpp/{founding => thesis}/2019-thesis-blatter.md | 0
.../sante/{founding => foundational}/2010-afadl-c.md | 2 +-
.../sante/{founding => foundational}/2010-tap-ckgj.md | 2 +-
.../sante/{founding => foundational}/2011-tap-ckgj.md | 2 +-
.../sante/{founding => foundational}/2012-sac-ckgj.md | 2 +-
.../secureflow/{founding => foundational}/2013-sec-astt.md | 2 +-
.../secureflow/{founding => foundational}/2017-tap-bs.md | 2 +-
.../sidan/{founding => foundational}/2009-crisis-dtt.md | 2 +-
.../slicing/{founding => foundational}/2008-trust-ms.md | 2 +-
.../stac/{founding => foundational}/2010-mdv-cmp.md | 2 +-
.../stady/{founding => foundational}/2014-scam-pkbgj.md | 2 +-
.../stady/{founding => foundational}/2014-tap-pkgj.md | 2 +-
.../stady/{founding => foundational}/2016-tap-pkbgj.md | 2 +-
.../stady/{founding => foundational}/2018-fac-pkbgj.md | 2 +-
.../taster/{founding => foundational}/2010-erts-ddmls.md | 2 +-
.../wp/{founding => foundational}/2012-nfm-c.md | 2 +-
html/publications.html | 6 +++---
45 files changed, 46 insertions(+), 46 deletions(-)
rename _fc-publications/aorai/{founding => foundational}/2009-afadl-gs.md (97%)
rename _fc-publications/c2s/{founding => foundational}/2016-scam-bkll.md (98%)
rename _fc-publications/c2s/{founding => foundational}/2017-vpt-blk.md (97%)
rename _fc-publications/cfp/{founding => foundational}/2017-lopstr-as.md (98%)
rename _fc-publications/cost/{founding => foundational}/2012-fmics-amarg.md (98%)
rename _fc-publications/e-acsl/{founding => foundational}/2013-sac-dks.md (97%)
rename _fc-publications/e-acsl/{founding => foundational}/2017-ismm-vsk.md (98%)
rename _fc-publications/e-acsl/{founding => foundational}/2017-rvcubes-skv.md (97%)
rename _fc-publications/e-acsl/{founding => foundational}/2020-rv-kms.md (98%)
rename _fc-publications/eva/{founding => foundational}/2011-jfla-bc.md (96%)
rename _fc-publications/eva/{founding => foundational}/2019-vmcai-bby.md (98%)
rename _fc-publications/fanc/{founding => foundational}/2012-erts-cddml.md (98%)
rename _fc-publications/general/{founding => foundational}/2012-sefm-ckkpsy.md (97%)
rename _fc-publications/general/{founding => foundational}/2015-fac-kkpsy.md (97%)
rename _fc-publications/jessie/{founding => foundational}/2007-ccv-m.md (97%)
rename _fc-publications/jessie/{founding => foundational}/2007-hav-hm.md (91%)
rename _fc-publications/jessie/{founding => foundational}/2007-hav-mm.md (98%)
rename _fc-publications/jessie/{founding => foundational}/2007-inria-m.md (98%)
rename _fc-publications/jessie/{founding => foundational}/2008-vmcai-m.md (98%)
rename _fc-publications/jessie/{founding => foundational}/2009-inria-a.md (98%)
rename _fc-publications/jessie/{founding => foundational}/2010-jsc-mm.md (97%)
rename _fc-publications/jessie/{founding => foundational}/2010-nfm-bn.md (97%)
rename _fc-publications/metacsl/{founding => foundational}/2019-tacas-rkprlg.md (98%)
rename _fc-publications/metacsl/{founding => foundational}/2019-tap-rkvrlg.md (98%)
rename _fc-publications/pathcrawler/{founding => foundational}/2004-ase-wmm.md (98%)
rename _fc-publications/pathcrawler/{founding => foundational}/2005-edcc-wmmr.md (98%)
rename _fc-publications/rpp/{founding => foundational}/2017-tacas-bklgp.md (98%)
rename _fc-publications/rpp/{founding => foundational}/2018-tap-bklgpp.md (98%)
rename _fc-publications/rpp/{founding => thesis}/2019-thesis-blatter.md (100%)
rename _fc-publications/sante/{founding => foundational}/2010-afadl-c.md (97%)
rename _fc-publications/sante/{founding => foundational}/2010-tap-ckgj.md (97%)
rename _fc-publications/sante/{founding => foundational}/2011-tap-ckgj.md (97%)
rename _fc-publications/sante/{founding => foundational}/2012-sac-ckgj.md (98%)
rename _fc-publications/secureflow/{founding => foundational}/2013-sec-astt.md (97%)
rename _fc-publications/secureflow/{founding => foundational}/2017-tap-bs.md (98%)
rename _fc-publications/sidan/{founding => foundational}/2009-crisis-dtt.md (98%)
rename _fc-publications/slicing/{founding => foundational}/2008-trust-ms.md (98%)
rename _fc-publications/stac/{founding => foundational}/2010-mdv-cmp.md (98%)
rename _fc-publications/stady/{founding => foundational}/2014-scam-pkbgj.md (98%)
rename _fc-publications/stady/{founding => foundational}/2014-tap-pkgj.md (97%)
rename _fc-publications/stady/{founding => foundational}/2016-tap-pkbgj.md (98%)
rename _fc-publications/stady/{founding => foundational}/2018-fac-pkbgj.md (98%)
rename _fc-publications/taster/{founding => foundational}/2010-erts-ddmls.md (97%)
rename _fc-publications/wp/{founding => foundational}/2012-nfm-c.md (97%)
diff --git a/_fc-publications/aorai/founding/2009-afadl-gs.md b/_fc-publications/aorai/foundational/2009-afadl-gs.md
similarity index 97%
rename from _fc-publications/aorai/founding/2009-afadl-gs.md
rename to _fc-publications/aorai/foundational/2009-afadl-gs.md
index 70c8e803..147c1077 100644
--- a/_fc-publications/aorai/founding/2009-afadl-gs.md
+++ b/_fc-publications/aorai/foundational/2009-afadl-gs.md
@@ -5,7 +5,7 @@ title: "Vérification de propriétés LTL sur des programmes C par génération
book: "Proceedings of Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL)"
link: http://hal.archives-ouvertes.fr/inria-00568947
year: 2009
-category: founding
+category: foundational
short: "In French."
---
diff --git a/_fc-publications/c2s/founding/2016-scam-bkll.md b/_fc-publications/c2s/foundational/2016-scam-bkll.md
similarity index 98%
rename from _fc-publications/c2s/founding/2016-scam-bkll.md
rename to _fc-publications/c2s/foundational/2016-scam-bkll.md
index 455c2bd6..de5a516e 100644
--- a/_fc-publications/c2s/founding/2016-scam-bkll.md
+++ b/_fc-publications/c2s/foundational/2016-scam-bkll.md
@@ -5,7 +5,7 @@ title: "Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of
book: "16th International Working Conference on Source Code Analysis and Manipulation (SCAM)"
link: https://hal.archives-ouvertes.fr/hal-01423641/en
year: 2016
-category: founding
+category: foundational
---
Frama-C is an extensible modular framework for analysis of C programs that offers different analyzers in the form of collaborating plugins. Currently, Frama-C does not support the proof of functional properties of concurrent code. We present Conc2Seq, a new code transformation based tool realized as a Frama-C plugin and dedicated to the verification of concurrent C programs. Assuming the program under verification respects an interleaving semantics, Conc2Seq transforms the original concurrent C program into a sequential one in which concurrency is simulated by interleavings. User specifications are automatically reintegrated into the new code without manual intervention. The goal of the proposed code transformation technique is to allow the user to reason about a concurrent program through the interleaving semantics using existing Frama-C analyzers.
\ No newline at end of file
diff --git a/_fc-publications/c2s/founding/2017-vpt-blk.md b/_fc-publications/c2s/foundational/2017-vpt-blk.md
similarity index 97%
rename from _fc-publications/c2s/founding/2017-vpt-blk.md
rename to _fc-publications/c2s/foundational/2017-vpt-blk.md
index e2b87e69..16ca150b 100644
--- a/_fc-publications/c2s/founding/2017-vpt-blk.md
+++ b/_fc-publications/c2s/foundational/2017-vpt-blk.md
@@ -5,7 +5,7 @@ title: "From Concurrent Programs to Simulating Sequential Programs: Correctness
book: "Fifth International Workshop on Verification and Program Transformation (VPT)"
link: https://hal.archives-ouvertes.fr/hal-01495454/en
year: 2017
-category: founding
+category: foundational
---
Frama-C is a software analysis framework that provides a common infrastructure and a common behavioral specification language to plugins that implement various static and dynamic analyses of C programs. Most plugins do not support concurrency. We have proposed conc2seq, a Frama-C plugin based on program transformation, capable to leverage the existing huge code base of plugins and to handle concurrent C programs. In this paper we formalize and sketch the proof of correctness of the program transformation principle behind conc2seq, and present an effort towards the full mechanization of both the for- malization and proofs with the proof assistant Coq.
\ No newline at end of file
diff --git a/_fc-publications/cfp/founding/2017-lopstr-as.md b/_fc-publications/cfp/foundational/2017-lopstr-as.md
similarity index 98%
rename from _fc-publications/cfp/founding/2017-lopstr-as.md
rename to _fc-publications/cfp/foundational/2017-lopstr-as.md
index bf4011c5..d2fcb4ef 100644
--- a/_fc-publications/cfp/founding/2017-lopstr-as.md
+++ b/_fc-publications/cfp/foundational/2017-lopstr-as.md
@@ -5,7 +5,7 @@ title: "Context Generation from Formal Specifications for C Analysis Tools"
book: "Logic-based Program Synthesis and Transformation (LOPSTR)"
link: http://julien.signoles.free.fr/publis/2017_lopstr.pdf
year: 2017
-category: founding
+category: foundational
short: "Best paper award."
---
diff --git a/_fc-publications/cost/founding/2012-fmics-amarg.md b/_fc-publications/cost/foundational/2012-fmics-amarg.md
similarity index 98%
rename from _fc-publications/cost/founding/2012-fmics-amarg.md
rename to _fc-publications/cost/foundational/2012-fmics-amarg.md
index 7c2bf431..ffe12df3 100644
--- a/_fc-publications/cost/founding/2012-fmics-amarg.md
+++ b/_fc-publications/cost/foundational/2012-fmics-amarg.md
@@ -5,7 +5,7 @@ title: "Certifying and reasoning on cost annotations in C programs"
book: "Proceedings of the 17th International Workshop on Formal Methods for Industrial Critical Systems (FMICS)"
link: http://hal.inria.fr/hal-00702665/en
year: 2012
-category: founding
+category: foundational
---
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. The first contribution of this paper is a proof methodology that extends standard simulation proofs of compiler correctness to ensure that the cost annotations on the source code are sound and precise with respect to an execution cost model of the object code. As a second contribution, we demonstrate that our label-based instrumentation is scalable because it consists in a modular extension of the compilation chain. To that end, we report our successful experience in implementing and testing the labelling approach on top of a prototype compiler written in OCaml for (a large fragment of) the C language. As a third and last contribution, we provide evidence for the usability of the generated cost annotations as a mean to reason on the concrete complexity of programs written in C. For this purpose, 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. These logic assertions are synthetic in the sense that they characterize the cost of executing the entire program, not only constant-time fragments. (These bounds may depend on the size of the input data.) 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.
\ No newline at end of file
diff --git a/_fc-publications/e-acsl/founding/2013-sac-dks.md b/_fc-publications/e-acsl/foundational/2013-sac-dks.md
similarity index 97%
rename from _fc-publications/e-acsl/founding/2013-sac-dks.md
rename to _fc-publications/e-acsl/foundational/2013-sac-dks.md
index 6ff37e28..2bf557a9 100644
--- a/_fc-publications/e-acsl/founding/2013-sac-dks.md
+++ b/_fc-publications/e-acsl/foundational/2013-sac-dks.md
@@ -5,7 +5,7 @@ title: "Common Specification Language for Static and Dynamic Analysis of C Progr
book: "Proceedings of Symposium on Applied Computing (SAC)"
link: https://hal.inria.fr/hal-00853721/en
year: 2013
-category: founding
+category: foundational
short: "An overview of the specification language."
---
diff --git a/_fc-publications/e-acsl/founding/2017-ismm-vsk.md b/_fc-publications/e-acsl/foundational/2017-ismm-vsk.md
similarity index 98%
rename from _fc-publications/e-acsl/founding/2017-ismm-vsk.md
rename to _fc-publications/e-acsl/foundational/2017-ismm-vsk.md
index 4bebe3d5..f32cc6ad 100644
--- a/_fc-publications/e-acsl/founding/2017-ismm-vsk.md
+++ b/_fc-publications/e-acsl/foundational/2017-ismm-vsk.md
@@ -5,7 +5,7 @@ title: "Shadow state encoding for efficient monitoring of block-level properties
book: "International Symposium on Memory Management (ISMM)"
link: http://julien.signoles.free.fr/publis/2017_ismm.pdf
year: 2017
-category: founding
+category: foundational
short: "Presentation of the shadow memory technique used by E-ACSL to monitor memory properties."
---
diff --git a/_fc-publications/e-acsl/founding/2017-rvcubes-skv.md b/_fc-publications/e-acsl/foundational/2017-rvcubes-skv.md
similarity index 97%
rename from _fc-publications/e-acsl/founding/2017-rvcubes-skv.md
rename to _fc-publications/e-acsl/foundational/2017-rvcubes-skv.md
index 368e2032..b8010568 100644
--- a/_fc-publications/e-acsl/founding/2017-rvcubes-skv.md
+++ b/_fc-publications/e-acsl/foundational/2017-rvcubes-skv.md
@@ -5,7 +5,7 @@ title: "E-ACSL, a Runtime Verification Tool for Safety and Security of C Program
book: "International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CuBES)"
link: http://julien.signoles.free.fr/publis/2017_rvcubes_tool.pdf
year: 2017
-category: founding
+category: foundational
short: "An overview of the E-ACSL plug-in."
---
diff --git a/_fc-publications/e-acsl/founding/2020-rv-kms.md b/_fc-publications/e-acsl/foundational/2020-rv-kms.md
similarity index 98%
rename from _fc-publications/e-acsl/founding/2020-rv-kms.md
rename to _fc-publications/e-acsl/foundational/2020-rv-kms.md
index 69fbae02..d2e73bb5 100644
--- a/_fc-publications/e-acsl/founding/2020-rv-kms.md
+++ b/_fc-publications/e-acsl/foundational/2020-rv-kms.md
@@ -5,7 +5,7 @@ title: "Efficient Runtime Assertion Checking for Properties over Mathematical Nu
book: "International Conference on Runtime Verification (RV)"
link: http://julien.signoles.free.fr/publis/2020_rv.pdf
year: 2020
-category: founding
+category: foundational
---
Runtime assertion checking is the discipline of detecting at
diff --git a/_fc-publications/eva/founding/2011-jfla-bc.md b/_fc-publications/eva/foundational/2011-jfla-bc.md
similarity index 96%
rename from _fc-publications/eva/founding/2011-jfla-bc.md
rename to _fc-publications/eva/foundational/2011-jfla-bc.md
index 97413415..4cf1dde8 100644
--- a/_fc-publications/eva/founding/2011-jfla-bc.md
+++ b/_fc-publications/eva/foundational/2011-jfla-bc.md
@@ -5,7 +5,7 @@ title: "A Mergeable Interval Map"
book: "Journées Francophones des Langages Applicatifs (JFLA)"
link: "https://pdfs.semanticscholar.org/5972/1d7cac5cf4fdc0cc3947432c6472f1da0f82.pdf"
year: 2011
-category: founding
+category: foundational
---
This article describes an efficient persistent mergeable data structure for mapping intervals to values. We call this data structure rangemap. We provide an example of application where the need for such a data structure arises (abstract interpretation of programs with pointer casts). We detail different solutions we have considered and dismissed before reaching the solution of rangemaps. We show how they solve the initial problem and eventually describe their implementation.
\ No newline at end of file
diff --git a/_fc-publications/eva/founding/2019-vmcai-bby.md b/_fc-publications/eva/foundational/2019-vmcai-bby.md
similarity index 98%
rename from _fc-publications/eva/founding/2019-vmcai-bby.md
rename to _fc-publications/eva/foundational/2019-vmcai-bby.md
index 3e3038fd..0a63ed6b 100644
--- a/_fc-publications/eva/founding/2019-vmcai-bby.md
+++ b/_fc-publications/eva/foundational/2019-vmcai-bby.md
@@ -5,7 +5,7 @@ title: "Structuring Abstract Interpreters Through State and Value Abstractions"
book: "Verification, Model Checking, and Abstract Interpretation (VMCAI)"
link: https://hal-cea.archives-ouvertes.fr/cea-01808886/en
year: 2019
-category: founding
+category: foundational
short: "Formalization of the communication mechanism between abstractions in EVA."
---
diff --git a/_fc-publications/fanc/founding/2012-erts-cddml.md b/_fc-publications/fanc/foundational/2012-erts-cddml.md
similarity index 98%
rename from _fc-publications/fanc/founding/2012-erts-cddml.md
rename to _fc-publications/fanc/foundational/2012-erts-cddml.md
index 9b606047..f2450f0b 100644
--- a/_fc-publications/fanc/founding/2012-erts-cddml.md
+++ b/_fc-publications/fanc/foundational/2012-erts-cddml.md
@@ -5,7 +5,7 @@ title: "Fan-C, a Frama-C plug-in for data flow verification"
book: "Proceedings of Embedded Real Time Software and Systems (ERTS²)"
link: https://hal.archives-ouvertes.fr/hal-02263407/en
year: 2012
-category: founding
+category: foundational
---
DO-178B compliant avionics development processes must both define the data and control flows of embedded software at design level, and verify flows are faithfully implemented in the source code. This verification is traditionally performed during dedicated code reviews, but such intellectual activities are costly and error-prone, especially for large and complex software. In this paper, we present the Fan-C plug-in, developed by Airbus on top of the abstract-interpretation-based value and dataflow analyses of the Frama-C platform, in order to automate this verification activity for C avionics software. We therefore describe the Airbus context, the Frama-C platform, its value analysis and related plug-ins, the Fan-C plug-in, and discuss analysis results and ongoing industrial deployment and qualification activities.
\ No newline at end of file
diff --git a/_fc-publications/general/founding/2012-sefm-ckkpsy.md b/_fc-publications/general/foundational/2012-sefm-ckkpsy.md
similarity index 97%
rename from _fc-publications/general/founding/2012-sefm-ckkpsy.md
rename to _fc-publications/general/foundational/2012-sefm-ckkpsy.md
index dc81d871..e07afed6 100644
--- a/_fc-publications/general/founding/2012-sefm-ckkpsy.md
+++ b/_fc-publications/general/foundational/2012-sefm-ckkpsy.md
@@ -4,7 +4,7 @@ authors: "Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Jul
title: "Frama-C, A Software Analysis Perspective"
book: "Proceedings of International Conference on Software Engineering and Formal Methods 2012 (SEFM)"
year: 2012
-category: founding
+category: foundational
short: "This paper presents a synthetic view of Frama-C, its main and composite analyses, and some of its industrial achievements."
---
diff --git a/_fc-publications/general/founding/2015-fac-kkpsy.md b/_fc-publications/general/foundational/2015-fac-kkpsy.md
similarity index 97%
rename from _fc-publications/general/founding/2015-fac-kkpsy.md
rename to _fc-publications/general/foundational/2015-fac-kkpsy.md
index 5855e986..1fd1f627 100644
--- a/_fc-publications/general/founding/2015-fac-kkpsy.md
+++ b/_fc-publications/general/foundational/2015-fac-kkpsy.md
@@ -5,7 +5,7 @@ title: "Frama-C, A Software Analysis Perspective"
book: "Formal Aspects of Computing, vol. 27 issue 3"
link: "http://dx.doi.org/10.1007/s00165-014-0326-7"
year: 2015
-category: founding
+category: foundational
---
Frama-C is a source code analysis platform that aims at conducting verification of industrial-size C programs. It provides its users with a collection of plug-ins that perform static analysis, deductive verification, and testing, for safety- and security-critical software. Collaborative verification across cooperating plug-ins is enabled by their integration on top of a shared kernel and datastructures, and their compliance to a common specification language. This foundational article presents a consolidated view of the platform, its main and composite analyses, and some of its industrial achievements.
\ No newline at end of file
diff --git a/_fc-publications/jessie/founding/2007-ccv-m.md b/_fc-publications/jessie/foundational/2007-ccv-m.md
similarity index 97%
rename from _fc-publications/jessie/founding/2007-ccv-m.md
rename to _fc-publications/jessie/foundational/2007-ccv-m.md
index 9b1c6755..a5dacdb6 100644
--- a/_fc-publications/jessie/founding/2007-ccv-m.md
+++ b/_fc-publications/jessie/foundational/2007-ccv-m.md
@@ -5,7 +5,7 @@ title: "Union and Cast in Deductive Verification"
book: "Proceedings of the C/C++ Verification Workshop (CCV)"
link: https://pdfs.semanticscholar.org/1fce/15dc2c6e8a42c5da1dd7e56fdb224f1e9ed1.pdf
year: 2007
-category: founding
+category: foundational
---
Deductive verification based on weakest-precondition calculus has
diff --git a/_fc-publications/jessie/founding/2007-hav-hm.md b/_fc-publications/jessie/foundational/2007-hav-hm.md
similarity index 91%
rename from _fc-publications/jessie/founding/2007-hav-hm.md
rename to _fc-publications/jessie/foundational/2007-hav-hm.md
index 59611edb..8961b812 100644
--- a/_fc-publications/jessie/founding/2007-hav-hm.md
+++ b/_fc-publications/jessie/foundational/2007-hav-hm.md
@@ -5,6 +5,6 @@ title: "Separation analysis for deductive verification"
book: "Proceedings of Heap Analysis and Verification (HAV)"
link: http://www.lri.fr/~marche/hubert07hav.pdf
year: 2007
-category: founding
+category: foundational
---
diff --git a/_fc-publications/jessie/founding/2007-hav-mm.md b/_fc-publications/jessie/foundational/2007-hav-mm.md
similarity index 98%
rename from _fc-publications/jessie/founding/2007-hav-mm.md
rename to _fc-publications/jessie/foundational/2007-hav-mm.md
index 61b47bb2..758cb3b3 100644
--- a/_fc-publications/jessie/founding/2007-hav-mm.md
+++ b/_fc-publications/jessie/foundational/2007-hav-mm.md
@@ -5,7 +5,7 @@ title: "Inferring local (non-)aliasing and strings for memory safety"
book: "Proceedings of Heap Analysis and Verification (HAV)"
link: https://www.researchgate.net/publication/250763933_Inferring_Local_NonAliasing_and_Strings_for_Memory_Safety_1
year: 2007
-category: founding
+category: foundational
---
We propose an original approach for checking memory safety of C
diff --git a/_fc-publications/jessie/founding/2007-inria-m.md b/_fc-publications/jessie/foundational/2007-inria-m.md
similarity index 98%
rename from _fc-publications/jessie/founding/2007-inria-m.md
rename to _fc-publications/jessie/foundational/2007-inria-m.md
index ee9ca91c..f269c1e0 100644
--- a/_fc-publications/jessie/founding/2007-inria-m.md
+++ b/_fc-publications/jessie/foundational/2007-inria-m.md
@@ -5,7 +5,7 @@ title: "Checking C Pointer Programs for Memory Safety"
book: "INRIA Research Report n°6334"
link: https://hal.inria.fr/inria-00181950/en
year: 2007
-category: founding
+category: foundational
---
We propose an original approach for checking memory safety of C
diff --git a/_fc-publications/jessie/founding/2008-vmcai-m.md b/_fc-publications/jessie/foundational/2008-vmcai-m.md
similarity index 98%
rename from _fc-publications/jessie/founding/2008-vmcai-m.md
rename to _fc-publications/jessie/foundational/2008-vmcai-m.md
index 1a240508..2525f34b 100644
--- a/_fc-publications/jessie/founding/2008-vmcai-m.md
+++ b/_fc-publications/jessie/foundational/2008-vmcai-m.md
@@ -5,7 +5,7 @@ title: "Sufficient Preconditions for Modular Assertion Checking"
book: "Proceedings of the 9th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)"
link: https://link.springer.com/chapter/10.1007/978-3-540-78163-9_18
year: 2008
-category: founding
+category: foundational
---
Assertion checking is the restriction of program verification to
diff --git a/_fc-publications/jessie/founding/2009-inria-a.md b/_fc-publications/jessie/foundational/2009-inria-a.md
similarity index 98%
rename from _fc-publications/jessie/founding/2009-inria-a.md
rename to _fc-publications/jessie/foundational/2009-inria-a.md
index fce1a43e..c5445c07 100644
--- a/_fc-publications/jessie/founding/2009-inria-a.md
+++ b/_fc-publications/jessie/foundational/2009-inria-a.md
@@ -5,7 +5,7 @@ title: "On formal methods for certifying floating-point C programs"
book: "Research Report RR-6927, INRIA"
link: http://hal.inria.fr/inria-00383793/en/
year: 2009
-category: founding
+category: foundational
---
This paper presents an implementation of an extension of the ACSL specication language in the Frama-C tool in order to prove the correctness of floating-point C programs. A first model checks that there is no over flow, i.e., proof obligations are generated by the Why tool to prove that the result of a fl oating-point operation is not greater than the maximal fl oat allowed in the given type, this model is called the Strict model. A second model, called the Full model, extends the Strict model. The Full model allows over flows and deals with special values: signed infinities, NaNs (Not-a-Number) and signed zeros as in the IEEE-754 Standard. The verification conditions generated by Why are (partially) proved by automatic theorem provers: Alt-Ergo, Simplify, Yices, Z3, CVC3 and Gappa or discharged in the interactive proof assistant Coq using two existing Coq formalization of fl oating-point arithmetic. When the Why proof obligations are written in the syntax of the Gappa library, we can use the gappa and interval tactics to achieve the proof. Several examples of fl oating-point C programs are presented in the paper to prove the efficiency of this implementation.
\ No newline at end of file
diff --git a/_fc-publications/jessie/founding/2010-jsc-mm.md b/_fc-publications/jessie/foundational/2010-jsc-mm.md
similarity index 97%
rename from _fc-publications/jessie/founding/2010-jsc-mm.md
rename to _fc-publications/jessie/foundational/2010-jsc-mm.md
index 78e9427d..7ebde2ae 100644
--- a/_fc-publications/jessie/founding/2010-jsc-mm.md
+++ b/_fc-publications/jessie/foundational/2010-jsc-mm.md
@@ -5,7 +5,7 @@ title: "Modular inference of subprogram contracts for safety checking"
book: "Journal of Symbolic Computation"
link: http://hal.inria.fr/inria-00534331/en
year: 2010
-category: founding
+category: foundational
---
Contracts expressed by logic formulas allow one to formally specify expected behavior of programs. But writing such specifications manually takes a significant amount of work, in particular for uninteresting contracts which only aim at avoiding run-time errors during the execution. Thus, for programs of large size, it is desirable to at least partially infer such contracts. We propose a method to infer contracts expressed as boolean combinations of linear equalities and inequalities by combining different kinds of static analyses: abstract interpretation, weakest precondition computation and quantifier elimination. An important originality of our approach is to proceed modularly, considering subprograms independently. The practical applicability of our approach is demonstrated on experiments performed on a library and two benchmarks of vulnerabilities of C code.
\ No newline at end of file
diff --git a/_fc-publications/jessie/founding/2010-nfm-bn.md b/_fc-publications/jessie/foundational/2010-nfm-bn.md
similarity index 97%
rename from _fc-publications/jessie/founding/2010-nfm-bn.md
rename to _fc-publications/jessie/foundational/2010-nfm-bn.md
index cf99dbd8..3f532951 100644
--- a/_fc-publications/jessie/founding/2010-nfm-bn.md
+++ b/_fc-publications/jessie/foundational/2010-nfm-bn.md
@@ -5,7 +5,7 @@ title: "Hardware-independent proofs of numerical programs"
book: "Proceedings of the Second NASA Formal Methods Symposium (NFM)"
link: http://shemesh.larc.nasa.gov/NFM2010/proceedings/NASA-CP-2010-216215.pdf
year: 2010
-category: founding
+category: foundational
---
On recent architectures, a numerical program may give different answers depending on the execution hardware and the compilation. Our goal is to formally prove properties about numerical programs that are true for multiple architectures and compilers. We propose an approach that states the rounding error of each floating-point computation whatever the environment. This approach is implemented in the Frama-C platform for static analysis of C code. Small case studies using this approach are entirely and automatically proved.
\ No newline at end of file
diff --git a/_fc-publications/metacsl/founding/2019-tacas-rkprlg.md b/_fc-publications/metacsl/foundational/2019-tacas-rkprlg.md
similarity index 98%
rename from _fc-publications/metacsl/founding/2019-tacas-rkprlg.md
rename to _fc-publications/metacsl/foundational/2019-tacas-rkprlg.md
index 50615f83..c60186f1 100644
--- a/_fc-publications/metacsl/founding/2019-tacas-rkprlg.md
+++ b/_fc-publications/metacsl/foundational/2019-tacas-rkprlg.md
@@ -5,7 +5,7 @@ title: "MetAcsl: Specification and Verification of High-Level Properties"
book: "International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)"
link: https://hal-cea.archives-ouvertes.fr/cea-02019790/en
year: 2019
-category: founding
+category: foundational
---
Modular deductive verification is a powerful technique capable to show that each function in a program satisfies its contract. However, function contracts do not provide a global view of which high-level (e.g. security-related properties of a whole software module are actually established, making it very difficult to assess them. To address this issue, this paper proposes a new specification mechanism, called meta-properties. A meta-property can be seen as an enhanced global invariant specified for a set of functions, and capable to express predicates on values of variables, as well as memory related conditions (such as separation) and read or write access constraints. We also propose an automatic transformation technique translating meta-properties into usual contracts and assertions, that can be proved by traditional deductive verification tools. This technique has been implemented as a Frama-C plugin called MetAcsl and successfully applied to specify and prove safety- and security-related meta-properties in two illustrative case studies.
\ No newline at end of file
diff --git a/_fc-publications/metacsl/founding/2019-tap-rkvrlg.md b/_fc-publications/metacsl/foundational/2019-tap-rkvrlg.md
similarity index 98%
rename from _fc-publications/metacsl/founding/2019-tap-rkvrlg.md
rename to _fc-publications/metacsl/foundational/2019-tap-rkvrlg.md
index 475d72cf..fcd3bc7e 100644
--- a/_fc-publications/metacsl/founding/2019-tap-rkvrlg.md
+++ b/_fc-publications/metacsl/foundational/2019-tap-rkvrlg.md
@@ -5,7 +5,7 @@ title: "Tame Your Annotations with MetAcsl: Specifying, Testing and Proving High
book: "Tests and Proofs (TAP)"
link: https://hal.archives-ouvertes.fr/cea-02301892/en
year: 2019
-category: founding
+category: foundational
---
A common way to specify software properties is to associate a contract to each function, allowing the use of various techniques to assess (e.g. to prove or to test) that the implementation is valid with respect to these contracts. However, in practice, high-level properties are not always easily expressible through function contracts. Furthermore, such properties may span across multiple functions, making the specification task tedious, and its assessment difficult and error-prone, especially on large code bases. To address these issues, we propose a new specification mechanism called meta-properties. Meta-properties are enhanced global invariants specified for a set of functions, capable of expressing predicates on values of variables as well as memory related conditions (such as separation) and read or write access constraints. This paper gives a detailed presentation of meta-properties and their support in a dedicated Frama-C plugin MetAcsl, and shows that they are automatically amenable to both deductive verification and testing. This is demonstrated by applying these techniques on two illustrative case studies.
\ No newline at end of file
diff --git a/_fc-publications/pathcrawler/founding/2004-ase-wmm.md b/_fc-publications/pathcrawler/foundational/2004-ase-wmm.md
similarity index 98%
rename from _fc-publications/pathcrawler/founding/2004-ase-wmm.md
rename to _fc-publications/pathcrawler/foundational/2004-ase-wmm.md
index 7c21e447..1a79f01f 100644
--- a/_fc-publications/pathcrawler/founding/2004-ase-wmm.md
+++ b/_fc-publications/pathcrawler/foundational/2004-ase-wmm.md
@@ -5,7 +5,7 @@ title: "On-the-fly generation of k-paths tests for C functions: towards the auto
book: "International Conference on Automated Software Engineering (ASE)"
link: https://hal.archives-ouvertes.fr/hal-01810203/en
year: 2004
-category: founding
+category: foundational
---
We present a method for the automatic generation of tests satisfying the all-paths
diff --git a/_fc-publications/pathcrawler/founding/2005-edcc-wmmr.md b/_fc-publications/pathcrawler/foundational/2005-edcc-wmmr.md
similarity index 98%
rename from _fc-publications/pathcrawler/founding/2005-edcc-wmmr.md
rename to _fc-publications/pathcrawler/foundational/2005-edcc-wmmr.md
index 4969ced0..90abc2fd 100644
--- a/_fc-publications/pathcrawler/founding/2005-edcc-wmmr.md
+++ b/_fc-publications/pathcrawler/foundational/2005-edcc-wmmr.md
@@ -5,7 +5,7 @@ title: "PathCrawler: automatic generation of path tests by combining static and
book: "European Dependable Computing Conference (EDCC)"
link: https://hal.archives-ouvertes.fr/hal-01810201/en
year: 2005
-category: founding
+category: foundational
---
We present the PathCrawler prototype tool for the automatic generation of test-cases satisfying the rigorous all-paths criterion, with a user-defined limit on the number of loop iterations in the covered paths. The prototype treats C code and we illustrate the test-case generation process on a representative example of a C function containing data-structures of variable dimensions, loops with variable numbers of iterations and many infeasible paths. PathCrawler is based on a novel combination of code instrumentation and constraint solving which makes it both efficient and open to extension. It suffers neither from the approximations and complexity of static analysis, nor from the number of executions demanded by the use of heuristic algorithms in function minimisation and the possibility that they fail to find a solution. We believe that it demonstrates the feasibility of rigorous and systematic testing of sequential programs coded in imperative languages.
\ No newline at end of file
diff --git a/_fc-publications/rpp/founding/2017-tacas-bklgp.md b/_fc-publications/rpp/foundational/2017-tacas-bklgp.md
similarity index 98%
rename from _fc-publications/rpp/founding/2017-tacas-bklgp.md
rename to _fc-publications/rpp/foundational/2017-tacas-bklgp.md
index bbf22dcd..6aaaac13 100644
--- a/_fc-publications/rpp/founding/2017-tacas-bklgp.md
+++ b/_fc-publications/rpp/foundational/2017-tacas-bklgp.md
@@ -5,7 +5,7 @@ title: "RPP: Automatic Proof of Relational Properties by Self-composition"
book: "Tools and Algorithms for the Construction and Analysis of Systems23rd International Conference, TACAS"
link: https://hal-cea.archives-ouvertes.fr/cea-01808885/en
year: 2017
-category: founding
+category: foundational
---
Self-composition provides a powerful theoretical approach to prove relational properties, i.e. properties relating several program executions, that has been applied to compare two runs of one or similar programs (in secure dataflow properties, code transformations, etc.). This tool demo paper presents RPP, an original implementation of self-composition for specification and verification of relational properties in C programs in the FRAMA-C platform. We consider a very general notion of relational properties invoking any finite number of function calls of possibly dissimilar functions with possible nested calls. The new tool allows the user to specify a relational property, to prove it in a completely automatic way using classic deductive verification, and to use it as a hypothesis in the proof of other properties that may rely on it.
\ No newline at end of file
diff --git a/_fc-publications/rpp/founding/2018-tap-bklgpp.md b/_fc-publications/rpp/foundational/2018-tap-bklgpp.md
similarity index 98%
rename from _fc-publications/rpp/founding/2018-tap-bklgpp.md
rename to _fc-publications/rpp/foundational/2018-tap-bklgpp.md
index f73bab8b..ac167b28 100644
--- a/_fc-publications/rpp/founding/2018-tap-bklgpp.md
+++ b/_fc-publications/rpp/foundational/2018-tap-bklgpp.md
@@ -5,7 +5,7 @@ title: "Static and Dynamic Verification of Relational Properties on Self-compose
book: "In Tests and Proofs - 12th International Conference (TAP)"
link: https://hal-cea.archives-ouvertes.fr/cea-01835470/en
year: 2018
-category: founding
+category: foundational
---
Function contracts are a well-established way of formally specifying the intended behavior of a function. However, they usually only describe what should happen during a single call. Relational properties, on the other hand, link several function calls. They include such properties as non-interference, continuity and monotonicity. Other examples relate sequences of function calls, for instance, to show that decrypting an encrypted message with the appropriate key gives back the original message. Such properties cannot be expressed directly in the traditional setting of modular deductive verification, but are amenable to verification through self-composition. This paper presents a verification technique dedicated to relational properties in C programs and its implementation in the form of a FRAMA-C plugin called RPP and based on self-composition. It supports functions with side effects and recursive functions. The proposed approach makes it possible to prove a relational property, to check it at runtime, to generate a counterexample using testing and to use it as a hypothesis in the subsequent verification. Our initial experiments on existing benchmarks confirm that the proposed technique is helpful for static and dynamic analysis of relational properties.
\ No newline at end of file
diff --git a/_fc-publications/rpp/founding/2019-thesis-blatter.md b/_fc-publications/rpp/thesis/2019-thesis-blatter.md
similarity index 100%
rename from _fc-publications/rpp/founding/2019-thesis-blatter.md
rename to _fc-publications/rpp/thesis/2019-thesis-blatter.md
diff --git a/_fc-publications/sante/founding/2010-afadl-c.md b/_fc-publications/sante/foundational/2010-afadl-c.md
similarity index 97%
rename from _fc-publications/sante/founding/2010-afadl-c.md
rename to _fc-publications/sante/foundational/2010-afadl-c.md
index 63a01d9b..0f174ba1 100644
--- a/_fc-publications/sante/founding/2010-afadl-c.md
+++ b/_fc-publications/sante/foundational/2010-afadl-c.md
@@ -4,7 +4,7 @@ authors: "Omar Chebaro"
title: "Outil SANTE : Détection d’erreurs par analyse statique et test structurel des programmes C"
book: "Proceedings of 10iemes Journées Francophones Internationales sur les Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL)"
year: 2010
-category: founding
+category: foundational
short: In French.
---
diff --git a/_fc-publications/sante/founding/2010-tap-ckgj.md b/_fc-publications/sante/foundational/2010-tap-ckgj.md
similarity index 97%
rename from _fc-publications/sante/founding/2010-tap-ckgj.md
rename to _fc-publications/sante/foundational/2010-tap-ckgj.md
index abdd9b09..730cf8a8 100644
--- a/_fc-publications/sante/founding/2010-tap-ckgj.md
+++ b/_fc-publications/sante/foundational/2010-tap-ckgj.md
@@ -5,7 +5,7 @@ title: "Combining static analysis and test generation for C program debugging"
book: "Proceedings of the 4th International Conference on Tests & Proofs (TAP)"
link: https://hal.archives-ouvertes.fr/hal-00563308/en
year: 2010
-category: founding
+category: foundational
---
This paper presents our ongoing work on a tool prototype called
diff --git a/_fc-publications/sante/founding/2011-tap-ckgj.md b/_fc-publications/sante/foundational/2011-tap-ckgj.md
similarity index 97%
rename from _fc-publications/sante/founding/2011-tap-ckgj.md
rename to _fc-publications/sante/foundational/2011-tap-ckgj.md
index 267861cd..bb29a431 100644
--- a/_fc-publications/sante/founding/2011-tap-ckgj.md
+++ b/_fc-publications/sante/foundational/2011-tap-ckgj.md
@@ -5,7 +5,7 @@ title: "The SANTE Tool: Value Analysis, Program Slicing and Test Generation for
book: "Proceedings of the 5th International Conference on Tests & Proofs (TAP)"
link: https://hal.inria.fr/inria-00622904/en
year: 2011
-category: founding
+category: foundational
---
This short paper presents a prototype tool called SANTE (Static
diff --git a/_fc-publications/sante/founding/2012-sac-ckgj.md b/_fc-publications/sante/foundational/2012-sac-ckgj.md
similarity index 98%
rename from _fc-publications/sante/founding/2012-sac-ckgj.md
rename to _fc-publications/sante/foundational/2012-sac-ckgj.md
index 0709b7dc..568b8c85 100644
--- a/_fc-publications/sante/founding/2012-sac-ckgj.md
+++ b/_fc-publications/sante/foundational/2012-sac-ckgj.md
@@ -5,7 +5,7 @@ title: "Program slicing enhances a verification technique combining static and d
book: "Proceedings of the 27th Symposium On Applied Computing (SAC)"
link: https://hal.inria.fr/hal-00746814/en
year: 2012
-category: founding
+category: foundational
---
Recent research proposed efficient methods for software
diff --git a/_fc-publications/secureflow/founding/2013-sec-astt.md b/_fc-publications/secureflow/foundational/2013-sec-astt.md
similarity index 97%
rename from _fc-publications/secureflow/founding/2013-sec-astt.md
rename to _fc-publications/secureflow/foundational/2013-sec-astt.md
index 102f8298..c15f8606 100644
--- a/_fc-publications/secureflow/founding/2013-sec-astt.md
+++ b/_fc-publications/secureflow/foundational/2013-sec-astt.md
@@ -5,7 +5,7 @@ title: "Program transformation for non-interference verification on programs wit
book: "International Information Security and Privacy Conference (SEC)"
link: http://julien.signoles.free.fr/publis/2013_sec.pdf
year: 2013
-category: founding
+category: foundational
---
Novel approaches for dynamic information flow monitoring are promising since they enable permissive (accepting a large subset of executions) yet sound (rejecting all unsecure executions) enforcement of non-interference. In this paper, we present a dynamic information flow monitor for a language supporting pointers. Our flow-sensitive monitor relies on prior static analysis in order to soundly enforce non-interference. We also propose a program transformation that preserves the behavior of initial programs and soundly inlines our security monitor. This program transformation enables both dynamic and static verification of non-interference.
\ No newline at end of file
diff --git a/_fc-publications/secureflow/founding/2017-tap-bs.md b/_fc-publications/secureflow/foundational/2017-tap-bs.md
similarity index 98%
rename from _fc-publications/secureflow/founding/2017-tap-bs.md
rename to _fc-publications/secureflow/foundational/2017-tap-bs.md
index 02413eac..b6806e1c 100644
--- a/_fc-publications/secureflow/founding/2017-tap-bs.md
+++ b/_fc-publications/secureflow/foundational/2017-tap-bs.md
@@ -5,7 +5,7 @@ title: "Hybrid Information Flow Analysis for Real-World C Code"
book: "International Conference on Tests and Proofs (TAP)"
link: http://julien.signoles.free.fr/publis/2017_tap.pdf
year: 2017
-category: founding
+category: foundational
---
Information flow analysis models the propagation of data through a software system and identifies unintended information leaks. There is a wide range of such analyses, tracking flows statically, dynamically, or in a hybrid way combining both static and dynamic approaches.
diff --git a/_fc-publications/sidan/founding/2009-crisis-dtt.md b/_fc-publications/sidan/foundational/2009-crisis-dtt.md
similarity index 98%
rename from _fc-publications/sidan/founding/2009-crisis-dtt.md
rename to _fc-publications/sidan/foundational/2009-crisis-dtt.md
index 38b4bbdc..92b5bb0d 100644
--- a/_fc-publications/sidan/founding/2009-crisis-dtt.md
+++ b/_fc-publications/sidan/foundational/2009-crisis-dtt.md
@@ -5,7 +5,7 @@ title: "SIDAN: a tool dedicated to Software Instrumentation for Detecting Attack
book: "4th International Conference on Risks and Security of Internet and Systems (CRISIS)"
link: https://hal.archives-ouvertes.fr/hal-00424574/en
year: 2009
-category: founding
+category: foundational
---
Anomaly based intrusion detection systems rely on the build of a normal behavior model. When a deviation from this normal behavior is detected, an alert is raised. This anomaly approach, unlike the misuse approach, is able to detect unknown attacks. A basic technique to build such a model for a program is to use the system call sequences of the process. To improve the accuracy and completeness of this detection model, we can add information related to the system call, such as its arguments or its execution context. But even then, attacks that target non-control-data may be missed and attacks on control-data may be adapted to bypass the detection mechanism using evasion techniques. We propose in this article an approach that focuses on the detection of non-control-data attacks. Our approach aims at exploiting the internal state of a program to detect a memory corruption on non-control-data that could lead to an illegal system call. To achieve this, we propose to build a data-oriented detection model by statically analyzing a program source code. This model is used to instrument the program by adding reasonableness checks that verify the consistent state of the data items the system calls depend on. We thus argue that it is possible to detect a program misuse issued by a non-control-data attack inside the program during its execution. While keeping a low overhead, this approach allows to detect non-control-data attacks.
\ No newline at end of file
diff --git a/_fc-publications/slicing/founding/2008-trust-ms.md b/_fc-publications/slicing/foundational/2008-trust-ms.md
similarity index 98%
rename from _fc-publications/slicing/founding/2008-trust-ms.md
rename to _fc-publications/slicing/foundational/2008-trust-ms.md
index b21e9840..9220fa5a 100644
--- a/_fc-publications/slicing/founding/2008-trust-ms.md
+++ b/_fc-publications/slicing/foundational/2008-trust-ms.md
@@ -5,7 +5,7 @@ title: "Slicing for Security of Code"
book: "Proceedings of the 1st international conference on Trusted Computing and Trust in Information Technologies (TRUST)"
link: http://julien.signoles.free.fr/publis/2008_trust.pdf
year: 2008
-category: founding
+category: foundational
---
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.
\ No newline at end of file
diff --git a/_fc-publications/stac/founding/2010-mdv-cmp.md b/_fc-publications/stac/foundational/2010-mdv-cmp.md
similarity index 98%
rename from _fc-publications/stac/founding/2010-mdv-cmp.md
rename to _fc-publications/stac/foundational/2010-mdv-cmp.md
index 1c108c64..8a141d2e 100644
--- a/_fc-publications/stac/founding/2010-mdv-cmp.md
+++ b/_fc-publications/stac/foundational/2010-mdv-cmp.md
@@ -5,7 +5,7 @@ title: "Taint Dependency Sequences: a characterization of insecure execution pat
book: "Modeling and Detecting Vulnerabilities workshop (MDV)"
link: http://www-verimag.imag.fr/PEOPLE/mounier/Papers/mdv10.pdf
year: 2010
-category: founding
+category: foundational
---
Numerous software vulnerabilities can be activated only with dedicated user inputs. Taint analysis is a security check which consists in looking for possible dependency chains between user inputs and vulnerable statements (like array accesses). Most of the existing static taint analysis tools produce some warnings on potentially vulnerable program locations. It is then up to the developer to analyze these results by scanning the possible execution paths that may lead to these locations with unsecured user inputs. We present a Taint Dependency Sequences Calculus, based on a fine-grain data and control taint analysis, that aims to help the developer in this task by providing some information on the set of paths that need to be analyzed. Following some ideas introduced in, we also propose some metrics to characterize these paths in term of "dangerousness". This approach is illustrated with the help of the Verisec Suite and by describing a prototype, called STAC.
\ No newline at end of file
diff --git a/_fc-publications/stady/founding/2014-scam-pkbgj.md b/_fc-publications/stady/foundational/2014-scam-pkbgj.md
similarity index 98%
rename from _fc-publications/stady/founding/2014-scam-pkbgj.md
rename to _fc-publications/stady/foundational/2014-scam-pkbgj.md
index 704a74b9..439018a8 100644
--- a/_fc-publications/stady/founding/2014-scam-pkbgj.md
+++ b/_fc-publications/stady/foundational/2014-scam-pkbgj.md
@@ -5,7 +5,7 @@ title: "Instrumentation of Annotated C Programs for Test Generation"
book: "14th International Working Conference on Source Code Analysis and Manipulation (SCAM)"
link: https://hal.archives-ouvertes.fr/cea-01836306/en
year: 2014
-category: founding
+category: foundational
---
Software verification and validation often rely on formal specifications that encode desired program properties. Recent research proposed a combined verification approach in which a program can be incrementally verified using alternatively deductive verification and testing. Both techniques should use the same specification expressed in a unique specification language. This paper addresses this problem within the Frama-C framework for analysis of C programs, that offers ACSL as a common specification language. We provide a formal description of an automatic translation of ACSL annotations into C code that can be used by a test generation tool either to trigger and detect specification failures, or to gain confidence, or, under some assumptions, even to confirm that the code is in conformity with respect to the annotations. We implement the proposed specification translation in a combined verification tool Study. Our initial experiments suggest that the proposed support for a common specification language can be very helpful for combined static-dynamic analyses.
\ No newline at end of file
diff --git a/_fc-publications/stady/founding/2014-tap-pkgj.md b/_fc-publications/stady/foundational/2014-tap-pkgj.md
similarity index 97%
rename from _fc-publications/stady/founding/2014-tap-pkgj.md
rename to _fc-publications/stady/foundational/2014-tap-pkgj.md
index 7e3564b2..3a8e6e53 100644
--- a/_fc-publications/stady/founding/2014-tap-pkgj.md
+++ b/_fc-publications/stady/foundational/2014-tap-pkgj.md
@@ -5,7 +5,7 @@ title: "How Test Generation Helps Software Specification and Deductive Verificat
book: "International Conference on Tests and Proofs (TAP)"
link: https://hal.inria.fr/hal-01108553/en
year: 2014
-category: founding
+category: foundational
---
This paper describes an incremental methodology of deductive verification assisted by test generation and illustrates its benefits by a set of frequent verification scenarios. We present StaDy, a new integration of the concolic test generator PathCrawler within the software analysis platform Frama-C . This new plugin treats a complete formal specification of a C program during test generation and provides the validation engineer with a helpful feedback at all stages of the specification and verification tasks.
\ No newline at end of file
diff --git a/_fc-publications/stady/founding/2016-tap-pkbgj.md b/_fc-publications/stady/foundational/2016-tap-pkbgj.md
similarity index 98%
rename from _fc-publications/stady/founding/2016-tap-pkbgj.md
rename to _fc-publications/stady/foundational/2016-tap-pkbgj.md
index 8ed83f29..ea4a245f 100644
--- a/_fc-publications/stady/founding/2016-tap-pkbgj.md
+++ b/_fc-publications/stady/foundational/2016-tap-pkbgj.md
@@ -5,7 +5,7 @@ title: "Your Proof Fails? Testing Helps to Find the Reason"
book: "International Conference on Tests and Proofs (TAP)"
link: https://arxiv.org/abs/1508.01691
year: 2016
-category: founding
+category: foundational
---
Applying deductive verification to formally prove that a program respects its formal specification is a very complex and time-consuming task due in particular to the lack of feedback in case of proof failures. Along with a non-compliance between the code and its specification (due to an error in at least one of them), possible reasons of a proof failure include a missing or too weak specification for a called function or a loop, and lack of time or simply incapacity of the prover to finish a particular proof. This work proposes a complete methodology where test generation helps to identify the reason of a proof failure and to exhibit a counterexample clearly illustrating the issue. We define the categories of proof failures, introduce two subcategories of contract weaknesses (single and global ones), and examine their properties. We describe how to transform a formally specified C program into C code suitable for testing, and illustrate the benefits of the method on comprehensive examples. The method has been implemented in StaDy, a plugin of the software analysis platform Frama-C. Initial experiments show that detecting non-compliances and contract weaknesses allows to precisely diagnose most proof failures.
\ No newline at end of file
diff --git a/_fc-publications/stady/founding/2018-fac-pkbgj.md b/_fc-publications/stady/foundational/2018-fac-pkbgj.md
similarity index 98%
rename from _fc-publications/stady/founding/2018-fac-pkbgj.md
rename to _fc-publications/stady/foundational/2018-fac-pkbgj.md
index 3f59d5aa..52e5132d 100644
--- a/_fc-publications/stady/founding/2018-fac-pkbgj.md
+++ b/_fc-publications/stady/foundational/2018-fac-pkbgj.md
@@ -5,7 +5,7 @@ title: "How testing helps to diagnose proof failures"
book: "Formal Aspects of Computing, vol. 30 issue 6"
link: https://hal.archives-ouvertes.fr/hal-01948799/en
year: 2018
-category: founding
+category: foundational
short: "Extended version of \"Your Proof Fails? Testing Helps to Find the Reason\"."
---
diff --git a/_fc-publications/taster/founding/2010-erts-ddmls.md b/_fc-publications/taster/foundational/2010-erts-ddmls.md
similarity index 97%
rename from _fc-publications/taster/founding/2010-erts-ddmls.md
rename to _fc-publications/taster/foundational/2010-erts-ddmls.md
index 6afaba91..f0ab85fc 100644
--- a/_fc-publications/taster/founding/2010-erts-ddmls.md
+++ b/_fc-publications/taster/foundational/2010-erts-ddmls.md
@@ -5,7 +5,7 @@ title: "Taster, a Frama-C plug-in to enforce Coding Standards"
book: "Proceedings of Embedded Real Time Software and Systems (ERTS²)"
link: https://www.di.ens.fr/~delmas/papers/erts10.pdf
year: 2010
-category: founding
+category: foundational
---
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.
\ No newline at end of file
diff --git a/_fc-publications/wp/founding/2012-nfm-c.md b/_fc-publications/wp/foundational/2012-nfm-c.md
similarity index 97%
rename from _fc-publications/wp/founding/2012-nfm-c.md
rename to _fc-publications/wp/foundational/2012-nfm-c.md
index 3659c75d..f113b9fc 100644
--- a/_fc-publications/wp/founding/2012-nfm-c.md
+++ b/_fc-publications/wp/foundational/2012-nfm-c.md
@@ -4,7 +4,7 @@ authors: "Loïc Correnson"
title: "Qed. Computing What Remains to Be Proved."
book: "NASA Formal Methods (NFM)"
year: 2012
-category: founding
+category: foundational
short: "Presentation of Qed, a core library of WP that simplifies proof obligations before sending them to provers."
---
diff --git a/html/publications.html b/html/publications.html
index 502d444c..aa56b683 100644
--- a/html/publications.html
+++ b/html/publications.html
@@ -18,7 +18,7 @@ css: plugin
<h1> Frama-C General </h1>
{% include publication-entries.html title="Manuals" category="manuals" plugin="general" %}
- {% include publication-entries.html title="Founding" category="founding" plugin="general" %}
+ {% include publication-entries.html title="Foundational" category="foundational" plugin="general" %}
{% include publication-entries.html title="About the Frama-C Kernel" category="kernel" plugin="general" %}
{% include publication-entries.html title="Tutorials" category="tutorials" plugin="general" %}
@@ -36,9 +36,9 @@ css: plugin
{% include publication-entries.html title="Manuals" category="manuals" plugin=plugin.id %}
{% include publication-entries.html title="Thesis" category="thesis" plugin=plugin.id %}
- {% include publication-entries.html title="Founding" category="founding" plugin=plugin.id %}
+ {% include publication-entries.html title="Foundational" category="foundational" plugin=plugin.id %}
{% include publication-entries.html title="Tutorials" category="tutorials" plugin=plugin.id %}
- {% include publication-entries.html title="Other" category="other" plugin=plugin.id %}
+ {% include publication-entries.html title="Others" category="other" plugin=plugin.id %}
{% endif %}
{% endfor %}
--
GitLab