Merge branch 'publications-add-dois' into 'master'

Publications add dois

See merge request !183

_fc-publications/stady/2016-tap-pkbgj.md

@@ -3,9 +3,10 @@ plugin: "stady"
 authors: "Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti and Jacques Julliand"
 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
+link: "https://arxiv.org/abs/1508.01691"
+doi: "10.1007/978-3-319-41135-4_8"
 year: 2016
 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
+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.

_fc-publications/stady/2018-fac-pkbgj.md

@@ -3,10 +3,11 @@ plugin: "stady"
 authors: "Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti and Jacques Julliand"
 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
+link: "https://hal.archives-ouvertes.fr/hal-01948799/en"
+doi: "10.1007/s00165-018-0456-4"
 year: 2018
 category: foundational
 short: "Extended version of \"Your Proof Fails? Testing Helps to Find the Reason\"."
 ---
 
-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 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 C program formally specified in an executable specification language 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
+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 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 C program formally specified in an executable specification language 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.

_fc-publications/taster/2010-erts-ddmls.md

@@ -3,7 +3,7 @@ plugin: "taster"
 authors: "David Delmas, Stéphane Duprat, Victoria Moya Lamiel and Julien Signoles"
 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
+link: "https://www.di.ens.fr/~delmas/papers/erts10.pdf"
 year: 2010
 category: foundational
 ---

_fc-publications/wp/2010-sttt-cmpp.md → _fc-publications/wp/2011-sttt-cmpp.md

@@ -4,8 +4,9 @@ authors: "Pascal Cuoq, Benjamin Monate, Anne Pacalet and Virgile Prevosto"
 title: "Functional Dependencies of C Functions via Weakest Pre-Conditions"
 book: "International Journal on Software Tools for Technology Transfer (STTT)"
 link: "https://link.springer.com/article/10.1007/s10009-011-0192-z"
+doi: "10.1007/s10009-011-0192-z"
 year: 2011
 category: other
 ---
 
-We present functional dependencies, a convenient, formal, but high-level, specification format for a piece of procedural software (function). Functional dependencies specify the set of memory locations, which may be modified by the function, and for each modified location, the set of memory locations that influence its final value. Verifying that a function respects pre-defined functional dependencies can be tricky: the embedded world uses C and Ada, which have arrays and pointers. Existing systems we know of that manipulate functional dependencies, Caveat and SPARK, are restricted to pointer-free subsets of these languages. This article deals with the functional dependencies in a programming language with full aliasing. We show how to use a weakest pre-condition calculus to generate a verification condition for pre-existing functional dependencies requirements. This verification condition can then be checked using automated theorem provers or proof assistants. With our approach, it is possible to verify the specification as it was written beforehand. We assume little about the implementation of the verification condition generator itself. Our study takes place inside the C analysis framework Frama-C, where an experimental implementation of the technique described here has been implemented on top of the WP plug-in in the development version of the tool.
\ No newline at end of file
+We present functional dependencies, a convenient, formal, but high-level, specification format for a piece of procedural software (function). Functional dependencies specify the set of memory locations, which may be modified by the function, and for each modified location, the set of memory locations that influence its final value. Verifying that a function respects pre-defined functional dependencies can be tricky: the embedded world uses C and Ada, which have arrays and pointers. Existing systems we know of that manipulate functional dependencies, Caveat and SPARK, are restricted to pointer-free subsets of these languages. This article deals with the functional dependencies in a programming language with full aliasing. We show how to use a weakest pre-condition calculus to generate a verification condition for pre-existing functional dependencies requirements. This verification condition can then be checked using automated theorem provers or proof assistants. With our approach, it is possible to verify the specification as it was written beforehand. We assume little about the implementation of the verification condition generator itself. Our study takes place inside the C analysis framework Frama-C, where an experimental implementation of the technique described here has been implemented on top of the WP plug-in in the development version of the tool.

_fc-publications/wp/2012-nfm-c.md

@@ -3,9 +3,10 @@ plugin: "wp"
 authors: "Loïc Correnson"
 title: "Qed. Computing What Remains to Be Proved."
 book: "NASA Formal Methods (NFM)"
+link: "http://dx.doi.org/10.1007/978-3-319-06200-6_17"
 year: 2012
 category: foundational
 short: "Presentation of Qed, a core library of WP that simplifies proof obligations before sending them to provers."
 ---
 
-We propose a framework for manipulating in a efficient way terms and formulæ in classical logic modulo theories. Qed was initially designed for the generation of proof obligations of a weakest-precondition engine for C programs inside the Frama-C framework, but it has been implemented as an independent library. Key features of Qed include on-the-fly strong normalization with various theories and maximal sharing of terms in memory. Qed is also equipped with an extensible simplification engine. We illustrate the power of our framework by the implementation of non-trivial simplifications inside the Wp plug-in of Frama-C. These optimizations have been used to prove industrial, critical embedded softwares.
\ No newline at end of file
+We propose a framework for manipulating in a efficient way terms and formulæ in classical logic modulo theories. Qed was initially designed for the generation of proof obligations of a weakest-precondition engine for C programs inside the Frama-C framework, but it has been implemented as an independent library. Key features of Qed include on-the-fly strong normalization with various theories and maximal sharing of terms in memory. Qed is also equipped with an extensible simplification engine. We illustrate the power of our framework by the implementation of non-trivial simplifications inside the Wp plug-in of Frama-C. These optimizations have been used to prove industrial, critical embedded softwares.