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 70c8e803edcf0f8836325ff43dee163038c0cb62..147c1077fc203f75c635387b58ae5c04e60bcd58 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 455c2bd6d9dae3b11fb9b5842e3bdb29995093d0..de5a516ebeca80362c5bc327502a3fdd8f417103 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 e2b87e6929edf73080ce3ac012a031fb4bf3494c..16ca150b6229d71ebcdd8a22872f799d2853a30c 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 bf4011c5169850bee63dd56aa66be0285da3fc1e..d2fcb4ef4fbcaf43d78da78d66f174a421a840cd 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 7c2bf4310bb7998495f9046a966655aef18cde6a..ffe12df3648988aad9f7d25315dd89fb356c907f 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 6ff37e28b72ca044d1e4d34e1d8eeec143c38e2b..2bf557a9d7be89dbb0152548d212397895cb5a5c 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 4bebe3d53ab5c05dc8ab389764fef889bb343874..f32cc6ad7cdd922ea08f2cb490aaf58525ac3103 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 368e20326dbfa9550e4c9792695c976c115a7f9b..b8010568af748a725332beeb82781081fc0cbd59 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 69fbae02b3c87d4a190104506398acd14d8f1de8..d2e73bb5ee342c09928a0d494752fd95e43b1fc5 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 9741341585eeecf0552015d6620d8decdaa6d29e..4cf1dde89408a1bc7c14f1f67c476389ee42198a 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 3e3038fdda9b23189519dbdd2ecd33703b0f0a4a..0a63ed6b74e7ec8ca68c34dc5b91cd669235a92c 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 9b606047f5fa870ce745f5b867951ad293fa9abd..f2450f0b9bfc938cb3dd4b196c743d98c8b21998 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 dc81d871fa3bd3201bd9c3bd236da684fe711b1d..e07afed6b46360cae41facc7e353ab67bac46269 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 5855e9867389999a89697c6651929f5d4f3ff0d0..1fd1f62739db6a47b371a58f7ee3f71981171e86 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 9b1c675583b6e9e266c45ce07e8a1b19ec41068a..a5dacdb6d0a9e4872f79a10e2cdd994f6aec5af4 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 59611edb4102d25369ff552374dd21b2b97a92dd..8961b812cb4480a9b1a8d91798925d3e40cfed2a 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 61b47bb2b3ff82a6ae42b730e55167c8be475ead..758cb3b3deb7ad7137adef1abe5c0d55beb177a3 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 ee9ca91ce47b60bb00af7cbba9219ca824ac9e0f..f269c1e0def1bae168e458d49dc06b3afda041c6 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 1a24050825de6075dd75aa0e1a20d6e48831111d..2525f34b45ddd7bce11add80b760c02bab9dd1c1 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 fce1a43ef0b86a65275196d921135618b6d0482d..c5445c07db69a54341af145cf591ead2f666e892 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 78e9427d1077ef228f104f440c27b70c39305072..7ebde2aef98667f97f4457ead9763f93a3239352 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 cf99dbd80f8c691649a2c53e8d52d33ef5d13790..3f5329511826fab6d92ed23406e667957bdc9996 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 50615f8354df2b8e68d93b621bfb9134908d8346..c60186f15e80475a8b5be455937b83fcf3ad8a33 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 475d72cfbb78243238c2467c1e06759f706b9e81..fcd3bc7eff188989e978c6f6b68c32cb5814ab4b 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 7c21e4476f467ad9a466c0b679ed23fa97d4f580..1a79f01f6ab43b294904cd6d067e7d6afde09138 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 4969ced0000bf8a534c8a77e27396c03e2c62e19..90abc2fd81ef5c170331a2adf341977bb1b06b95 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 bbf22dcda899ade2ead880da1c5a28d43f510ce2..6aaaac1314eb49cb8c693b451fd43587c4c01e23 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 f73bab8bd2eb00be53b9b296f735fcdecc9b4901..ac167b2899b406308cf11f9824728f44f7931637 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 63a01d9bbc99005a2ba0647976946a635e37fe84..0f174ba147730adaa1c5ddbec8f240e9bafa3fe4 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 abdd9b09fc3c34b3aab6d7c0f8a5810c06e7305d..730cf8a87796b84fc9accc5866d1f562c817e953 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 267861cd4018fad33d876126dcc36c12fa143a01..bb29a4314a4cc32ecdbfdb9ee9a619d22bf041a5 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 0709b7dcb71d63cb34265671cc9559278fef27df..568b8c85b2bba5459a4c9391c1c2e133640a10a8 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 102f8298fa99aee9a80e7245cf4f473e3aa87af1..c15f86065c48d3ffdb5d94795357d8e3bad84b11 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 02413eaccfa91cda10b6d0f4db69452f6e0e1116..b6806e1c3e808f82a581a0628875cdcda448bf49 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 38b4bbdcda54d59f75a698a768d9f78d7c7fd87b..92b5bb0d8220551e34ba6efb9385b2baff0bc4fd 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 b21e984072fdb494f725f92299ff31bee35ac12e..9220fa5a3ba5c8d3e711d881a90b510879f25ae3 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 1c108c643f30795107d32d641a73710ea00c4b22..8a141d2ed590baa330d9e8a338cc8e46d3406712 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 704a74b9e8abda31ae77d6119391ecd2e092ea00..439018a872f287baca633cbab1fa5c9b4011c78a 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 7e3564b2c98a0daf1845d72983728610f0446a3b..3a8e6e5347fec38f80d2ced798fcc96724fa1d7e 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 8ed83f296449317ffc1e4f76f192c0984bac910b..ea4a245f0aa50f7d1fb228f8a16c31447dd1b913 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 3f59d5aaabec30732a0521c4866a9de4f9ecf64c..52e5132dd46bd0fb332dd16971ea49f3be0a342c 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 6afaba9129b1f24b9e0c7434bccdebe520a0dff9..f0ab85fc8b14e5565535489813e8aef0dd7261de 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 3659c75d81c828dd3e51128cb1e6c353b763a423..f113b9fc53251252f7c398c84ac81a767d7f9478 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 502d444cf009e062b06dec5a672c270523500400..aa56b683501cfe5e53782fda5a838fb3d7fd2d42 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 %}