diff --git a/dokuwiki/publications.md b/dokuwiki/publications.md
index b531fec4ec413c50933eb935862f36f21db7b153..bd5432b2a1f397226b9c9042a9a3e5d86061ac1e 100755
--- a/dokuwiki/publications.md
+++ b/dokuwiki/publications.md
@@ -40,7 +40,7 @@ when possible and only if they do respect copyright.
- Virgile Prevosto.
**ACSL Tutorial.**
<http://frama-c.com/download/acsl-tutorial.pdf>.
- // The official tutorial of ACSL.//
+ *The official tutorial of ACSL.*
<!-- end list -->
@@ -135,7 +135,7 @@ when possible and only if they do respect copyright.
In Hermann, editor, JFLA 09, Actes des vingtièmes Journées
Francophones des Langages Applicatifs 2009, volume 7.2 of Studia
Informatica Universalis, pages 245--280, June 2009. In French.
- // Cet article présente la bibliothèque de projets de Frama-C, une
+ *Cet article présente la bibliothèque de projets de Frama-C, une
plateforme facilitant le développement d'analyseurs statiques de
programmes C. Grâce à sa description, nous présentons une
utilisation originale des foncteurs du système de modules de ML qui
@@ -144,7 +144,7 @@ when possible and only if they do respect copyright.
souhaitée de manière bien typée. En outre, nous montrons un exemple
peu fréquent d'un même foncteur appliqué plusieurs centaines de
fois. Cet article introduit aussi la plateforme Frama-C elle-même, Ã
- travers un de ses aspects essentiels, la notion de projet.//
+ travers un de ses aspects essentiels, la notion de projet.*
#### Other Articles
@@ -321,8 +321,8 @@ when possible and only if they do respect copyright.
#### Other articles
- Pascal Cuoq, Benjamin Monate, Anne Pacalet and Virgile Prevosto.
- \*\* Functional Dependencies of C Functions via Weakest
- Pre-Conditions \*\*
+ **Functional Dependencies of C Functions via Weakest
+ Pre-Conditions**
International Journal on Software Tools for Technology Transfer
(STTT), edition VSTTE 2009-2010,
[SpringerLink](http://www.springerlink.com/content/yj344380377p4011/)
@@ -331,13 +331,12 @@ when possible and only if they do respect copyright.
<!-- end list -->
- Arnaud Dieumegard and Marc Pantel.
- \*\* Vérification d’un générateur de code par génération
- d’annotations. **
+ **Vérification d’un générateur de code par génération
+ d’annotations.**
Conférence en IngénieriE du Logiciel (CIEL), Juin 2012.
<http://gpl2012.irisa.fr/sites/default/files/CIEL2012-Dieumegard-paper34.pdf>
- \* Allan Blanchard.
- ** Introduction to C Program Proof using Frama-C and its WP Plugin.
- \*\*
+ - Allan Blanchard.
+ **Introduction to C Program Proof using Frama-C and its WP Plugin.**
WP tutorial, available at <http://allan-blanchard.fr/teaching.html>.
# Jessie
@@ -377,12 +376,11 @@ when possible and only if they do respect copyright.
<http://hal.inria.fr/inria-00534331/en>
- Sylvie Boldo and Thi Minh Tuyen Nguyen.
**Hardware-independent proofs of numerical programs.**
- In Proceedings of the Second NASA Formal Methods Symposium, April
- 2010.
+ In Proceedings of the Second NASA Formal Methods Symposium, April 2010.
<http://shemesh.larc.nasa.gov/NFM2010/proceedings/NASA-CP-2010-216215.pdf>
- Ali Ayad.
- \*\* On formal methods for certifying floating-point C
- programs.\*\*
+ **On formal methods for certifying floating-point C
+ programs.**
Research Report RR-6927, INRIA, 2009.
<http://hal.inria.fr/inria-00383793/en/>
@@ -391,9 +389,8 @@ when possible and only if they do respect copyright.
- Yannick Moy.
**Sufficient Preconditions for Modular Assertion Checking.**
In Proceedings of the 9th International Conference on Verification,
- Model Checking, and Abstract Interpretation (VMCAI'08). January
- 2008.
- //Assertion checking is the restriction of program verification to
+ Model Checking, and Abstract Interpretation (VMCAI'08). January 2008.
+ *Assertion checking is the restriction of program verification to
validity of program assertions. It encompasses safety checking,
which is program verification of safety properties, like memory
safety or absence of overflows. In this paper, we consider assertion
@@ -409,14 +406,14 @@ when possible and only if they do respect copyright.
programs. It combines abstract interpretation, weakest precondition
calculus and quantifier elimination. We instantiate this method to
prove memory safety for C and Java programs, under some memory
- separation conditions. //
+ separation conditions.*
<!-- end list -->
- Yannick Moy.
**Checking C Pointer Programs for Memory Safety.**
INRIA Research Report n°6334, October 2007.
- //We propose an original approach for checking memory safety of C
+ *We propose an original approach for checking memory safety of C
pointer programs that do not include casts, structures, double
indirection and memory deallocation. This involves first identifying
aliasing and strings, which we do in a local setting rather than
@@ -443,15 +440,14 @@ when possible and only if they do respect copyright.
refinement operators, this propagation method does not require
iterating around loops. We implemented our method in Caduceus, a
tool for the verification of C programs, and successfully verified
- automatically the C standard string library functions. //
+ automatically the C standard string library functions.*
<!-- end list -->
- Yannick Moy.
**Union and Cast in Deductive Verification.**
- In Proceedings of the C/C++ Verification Workshop (CCV'07), July
- 2007.
- //Deductive verification based on weakest-precondition calculus has
+ In Proceedings of the C/C++ Verification Workshop (CCV'07), July 2007.
+ *Deductive verification based on weakest-precondition calculus has
proved effective at proving imperative programs, through a suitable
encoding of memory as functional arrays (a.k.a. the Burstall-Bornat
model). Unfortunately, this encoding of memory makes it impossible
@@ -460,7 +456,7 @@ when possible and only if they do respect copyright.
structure subtyping, on which it is possible to extend the Burstall-
Bornat encoding. We present an automatic translation from C to an
intermediate language Jessie on which this extended interpretation
- is performed. //
+ is performed.*
<!-- end list -->
@@ -468,7 +464,7 @@ when possible and only if they do respect copyright.
**Inferring local (non-)aliasing and strings for memory safety.**
In Proceedings of Heap Analysis and Verification (HAV’07), Braga,
Portugal, March 2007.
- //We propose an original approach for checking memory safety of C
+ *We propose an original approach for checking memory safety of C
pointer programs, by combining deductive verification and abstract
interpretation techniques. The approach is modular and contextual,
thanks to the use of Hoare-style annotations (pre- and
@@ -491,7 +487,7 @@ when possible and only if they do respect copyright.
way, in the framework of abstract interpretation. We implemented our
method in Caduceus, a tool for the verification of C programs, and
successfully generated appropriate annotations for the C standard
- string library functions. //
+ string library functions.*
<!-- end list -->
@@ -581,21 +577,19 @@ when possible and only if they do respect copyright.
**Verification of Numerical Programs: From Real Numbers to Floating
Point Numbers.**
In NASA Formal Methods 2013.
- // Usually, proofs involving numerical computations are conducted in
+ *Usually, proofs involving numerical computations are conducted in
the infinitely precise realm of the field of real numbers. However,
numerical computations in these algorithms are often implemented
using floating point numbers. The use of a finite representation of
real numbers introduces uncertainties as to whether the properties
verified in the theoretical setting hold in practice. This short
paper describes work in progress aimed at addressing these concerns.
- Given a
-
-formally proven algorithm, written in the Program Verification System
+ Given a formally proven algorithm, written in the Program Verification System
(PVS), the Frama-C suite of tools is used to identify sufficient
conditions and verify that under such conditions the rounding errors
arising in a C implementation of the algorithm do not affect its
correctness. The technique is illustrated using an algorithm for
-detecting loss of separation among aircraft.//
+detecting loss of separation among aircraft.*
# Aoraï
@@ -680,7 +674,7 @@ detecting loss of separation among aircraft.//
In Proceedings of the 1st international conference on Trusted
Computing and Trust in Information Technologies (TRUST'08), pages
133--142, March 2008.
- //Bugs in programs implementing security features can be
+ *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
@@ -698,67 +692,161 @@ detecting loss of separation among aircraft.//
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.//
+ same in the original program and in the sliced program.*
# PathCrawler
#### Manual
-```
- * **PathCrawler Automatic Test Generation Tool For C Programs User Manual Version 3.1.**\\ [[http://frama-c.com/download/frama-c-pathcrawler.pdf]].\\ //The user manual of the Frama-C plug-in PathCrawler.//
-```
-
-#### Founding Articles
-
-```
- * Nicky Williams, Bruno Marre and Patricia Mouy.\\ ** On-the-fly generation of k-paths tests for C functions : towards the automation of grey-box testing. **\\ In Proc. 19th IEEE Intl. Conference on Automated Software Engineering (ASE 2004), 20-25 September 2004, Linz, Austria, IEEE Computer Society, 2004, ISBN 0-7695-2131-2, pages 290-293.\\ [[http://pathcrawler-online.com/pubs/ase04copy.pdf]]\\ The final publication is available from IEEE [[http://doi.ieeecomputersociety.org/10.1109/ASE.2004.10020]]
-```
-
-```
- * Nicky Williams, Bruno Marre, Patricia Mouy and Muriel Roger.\\ ** PathCrawler: automatic generation of path tests by combining static and dynamic analysis. **\\ In Proc. 5th European Dependable Computing Conference (EDCC-5), Budapest, Hungary, April 20-22, 2005, Lecture Notes in Computer Science 3463 Springer 2005, ISBN 3-540-25723-3, Budapest, Hungary, April 2005, pages 281-292.\\ [[http://pathcrawler-online.com/pubs/edcc05.pdf]]\\ The final publication is available at www.springerlink.com. [[http://dx.doi.org/10.1007/11408901_21]]
-```
+ * **PathCrawler Automatic Test Generation Tool For C Programs User Manual Version 3.1.**
+ <http://frama-c.com/download/frama-c-pathcrawler.pdf>.
+ *The user manual of the Frama-C plug-in PathCrawler.*
+
+#### Founding Articles
+
+ - Nicky Williams, Bruno Marre and Patricia Mouy.
+ **On-the-fly generation of k-paths tests for C functions :
+ towards the automation of grey-box testing.**
+ In Proc. 19th IEEE Intl. Conference on Automated Software
+ Engineering (ASE 2004), 20-25 September 2004, Linz, Austria, IEEE
+ Computer Society, 2004, ISBN 0-7695-2131-2, pages 290-293.
+ <http://pathcrawler-online.com/pubs/ase04copy.pdf>
+ The final publication is available from IEEE
+ <http://doi.ieeecomputersociety.org/10.1109/ASE.2004.10020>
+
+<!-- end list -->
+
+ - Nicky Williams, Bruno Marre, Patricia Mouy and Muriel Roger.
+ **PathCrawler: automatic generation of path tests by combining
+ static and dynamic analysis.**
+ In Proc. 5th European Dependable Computing Conference (EDCC-5),
+ Budapest, Hungary, April 20-22, 2005, Lecture Notes in Computer
+ Science 3463 Springer 2005, ISBN 3-540-25723-3, Budapest, Hungary,
+ April 2005, pages 281-292.
+ <http://pathcrawler-online.com/pubs/edcc05.pdf>
+ The final publication is available at www.springerlink.com.
+ <http://dx.doi.org/10.1007/11408901_21>
#### Other Articles
-```
- * Nicky Williams.\\ ** WCET measurement using modified path testing. **\\ In Proc. 5th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis, Palma de Mallorca, Spain, July 2005, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 2007.\\ [[http://pathcrawler-online.com/pubs/wcet05.pdf]]\\ The final publication is available at DROPS. [[http://drops.dagstuhl.de/opus/volltexte/2007/809]]
-```
-
-```
- * Patricia Mouy, Bruno Marre, Nicky Williams and Pascale Le Gall.\\ ** Generation of all-paths unit test with function calls. **\\ In Proc. 1st Intl. Conference on Software Testing, Verification, and Validation, ICST 2008, Lillehammer, Norway, April 9-11, 2008, IEEE Computer Society, 2008, pages 32-41.\\ [[http://pathcrawler-online.com/pubs/icst08copy.pdf]]\\ The final publication is available from IEEE. [[http://doi.ieeecomputersociety.org/10.1109/ICST.2008.35]]
-```
-
-```
- * Nikolai Kosmatov.\\ ** All-paths test generation for programs with internal aliases. **\\ In Proc. 19th Intl. Symposium on Software Reliability Engineering (ISSRE 2008), Redmond, Seattle, USA, 11-14 November 2008, IEEE Computer Society, 2008, pages 147-156.\\ [[http://pathcrawler-online.com/pubs/issre08copy.pdf]]\\ The final publication is available from IEEE. [[http://dx.doi.org/10.1109/ISSRE.2008.25]]
-```
-
-```
- * Bernard Botella, Mickaël Delahaye, Stéphane Hong-Tuan-Ha, Nikolai Kosmatov, Patricia Mouy, Muriel Roger and Nicky Williams.\\ ** Automating Structural Testing of C Programs: Experience with PathCrawler. **\\ In Proc. 4th Intl. Workshop on Automation of Software Test, AST 2009, Vancouver, BC, Canada, May 18-19, 2009, IEEE Computer Society 2009, pages 70-78.\\ [[http://pathcrawler-online.com/pubs/ast09industrycopy.pdf]]\\ The final publication is available from IEEE. [[http://dx.doi.org/10.1109/IWAST.2009.5069043]]
-```
-
-```
- * Nicky Williams and Muriel Roger.\\ ** Test Generation Strategies to Measure Worst-Case Execution Time. **\\ In Proc. 4th Intl. Workshop on Automation of Software Test, AST 2009, Vancouver, BC, Canada, May 18-19, 2009, IEEE Computer Society 2009, pages 88-96.\\ [[http://pathcrawler-online.com/pubs/ast09researchcopy.pdf]]\\ The final publication is available from IEEE. [[http://dx.doi.org/10.1109/IWAST.2009.5069045]]
-```
-
-```
- * Nikolai Kosmatov.\\ ** On Complexity of All-Paths Test Generation. From Practice to Theory. **\\ In Proc. Testing: Academic and Industrial Conference - Practice and Research Techniques (TAIC PART 2009), Windsor, United Kingdom, September 2009, IEEE Computer Society Press, 2009, ISBN 978-0-7695-3820-4, pages 144-153.\\ [[http://pathcrawler-online.com/pubs/taic09copy.pdf]]\\ The final publication is available from IEEE. [[http://dx.doi.org/10.1109/TAICPART.2009.26]]
-```
-
-```
- * Nicky Williams.\\ ** Abstract path testing with PathCrawler. **\\ [[http://pathcrawler-online.com/pubs/ast10copy.pdf]]\\ ©ACM, 2010. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Proc. 5th Workshop on Automation of Software Test (AST'10), Cape Town, South Africa, May 2-8 2010, ACM New York, NY, USA, 2010, ISBN 978-1-60558-970-1, pages 35-42. [[http://doi.acm.org/10.1145/1808266.1808272]]
-```
-
-```
- * Nikolai Kosmatov, Bernard Botella, Muriel Roger and Nicky Williams.\\ ** Online Test Generation with PathCrawler. Tool demo. **\\ Best demo award. \\ In Proc. of the 3rd International Workshop on Constraints in Software Testing, Verification, and Analysis (CSTVA 2011), Berlin, Germany, March 2011, IEEE Computer Society Press, 2011, ISBN 978-1-4577-0019-4, pages 316-317.\\ [[http://pathcrawler-online.com/pubs/kosmatov_brw_cstva_2011copy.pdf]]\\ The final publication is available from IEEE. [[http://dx.doi.org/10.1109/ICSTW.2011.85]]
-```
-
-```
- * Nicky Williams and Nikolai Kosmatov.\\ ** Structural Testing with PathCrawler. Tutorial Synopsis. **\\ In Proc. 12th International Conference on Quality Software (QSIC 2012), Xi'an, China, August 27-29, 2012, IEEE Computer Society, 2012, ISBN 978-0-7695-4833-3, pages 289-292.\\ [[http://pathcrawler-online.com/pubs/qsic12copy.pdf]]\\ The final publication will be available from IEEE. [[http://www.ieee.org]]
-```
-
-```
- * Nikolai Kosmatov, Nicky Williams, Bernard Botella, Muriel Roger, Omar Chebaro.\\ ** A Lesson on Structural Testing with PathCrawler-online.com. **\\ In Proc. Tests and Proofs - 6th International Conference, TAP 2012, Prague, Czech Republic, May 31 - June 1, 2012, Springer, Lecture Notes in Computer Science, vol. 7305, 2012, ISBN 978-3-642-30472-9, pages 169-175.\\ [[http://pathcrawler-online.com/pubs/tap_2012_pconline_final.pdf]]\\ The final publication is available at www.springerlink.com. [[http://dx.doi.org/10.1007/978-3-642-30473-6_15]]
-```
+ - Nicky Williams.
+ **WCET measurement using modified path testing.**
+ In Proc. 5th Intl. Workshop on Worst-Case Execution Time (WCET)
+ Analysis, Palma de Mallorca, Spain, July 2005, Schloss Dagstuhl -
+ Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 2007.
+ <http://pathcrawler-online.com/pubs/wcet05.pdf>
+ The final publication is available at DROPS.
+ <http://drops.dagstuhl.de/opus/volltexte/2007/809>
+
+<!-- end list -->
+
+ - Patricia Mouy, Bruno Marre, Nicky Williams and Pascale Le Gall.
+ **Generation of all-paths unit test with function calls.**
+ In Proc. 1st Intl. Conference on Software Testing, Verification, and
+ Validation, ICST 2008, Lillehammer, Norway, April 9-11, 2008, IEEE
+ Computer Society, 2008, pages 32-41.
+ <http://pathcrawler-online.com/pubs/icst08copy.pdf>
+ The final publication is available from IEEE.
+ <http://doi.ieeecomputersociety.org/10.1109/ICST.2008.35>
+
+<!-- end list -->
+
+ - Nikolai Kosmatov.
+ **All-paths test generation for programs with internal aliases.**
+ In Proc. 19th Intl. Symposium on Software Reliability Engineering
+ (ISSRE 2008), Redmond, Seattle, USA, 11-14 November 2008, IEEE
+ Computer Society, 2008, pages 147-156.
+ <http://pathcrawler-online.com/pubs/issre08copy.pdf>
+ The final publication is available from IEEE.
+ <http://dx.doi.org/10.1109/ISSRE.2008.25>
+
+<!-- end list -->
+
+ - Bernard Botella, Mickaël Delahaye, Stéphane Hong-Tuan-Ha, Nikolai
+ Kosmatov, Patricia Mouy, Muriel Roger and Nicky Williams.
+ **Automating Structural Testing of C Programs: Experience with
+ PathCrawler.**
+ In Proc. 4th Intl. Workshop on Automation of Software Test, AST
+ 2009, Vancouver, BC, Canada, May 18-19, 2009, IEEE Computer Society
+ 2009, pages 70-78.
+ <http://pathcrawler-online.com/pubs/ast09industrycopy.pdf>
+ The final publication is available from IEEE.
+ <http://dx.doi.org/10.1109/IWAST.2009.5069043>
+
+<!-- end list -->
+
+ - Nicky Williams and Muriel Roger.
+ **Test Generation Strategies to Measure Worst-Case Execution
+ Time.**
+ In Proc. 4th Intl. Workshop on Automation of Software Test, AST
+ 2009, Vancouver, BC, Canada, May 18-19, 2009, IEEE Computer Society
+ 2009, pages 88-96.
+ <http://pathcrawler-online.com/pubs/ast09researchcopy.pdf>
+ The final publication is available from IEEE.
+ <http://dx.doi.org/10.1109/IWAST.2009.5069045>
+
+<!-- end list -->
+
+ - Nikolai Kosmatov.
+ **On Complexity of All-Paths Test Generation. From Practice to
+ Theory.**
+ In Proc. Testing: Academic and Industrial Conference - Practice and
+ Research Techniques (TAIC PART 2009), Windsor, United Kingdom,
+ September 2009, IEEE Computer Society Press, 2009, ISBN
+ 978-0-7695-3820-4, pages 144-153.
+ <http://pathcrawler-online.com/pubs/taic09copy.pdf>
+ The final publication is available from IEEE.
+ <http://dx.doi.org/10.1109/TAICPART.2009.26>
+
+<!-- end list -->
+
+ - Nicky Williams.
+ **Abstract path testing with PathCrawler.**
+ <http://pathcrawler-online.com/pubs/ast10copy.pdf>
+ ©ACM, 2010. This is the author's version of the work. It is posted
+ here by permission of ACM for your personal use. Not for
+ redistribution. The definitive version was published in Proc. 5th Workshop on Automation of Software
+ Test (AST'10), Cape Town, South Africa, May 2-8 2010, ACM New York, NY,
+ USA, 2010, ISBN 978-1-60558-970-1, pages 35-42.
+ <http://doi.acm.org/10.1145/1808266.1808272>
+
+<!-- end list -->
+
+ - Nikolai Kosmatov, Bernard Botella, Muriel Roger and Nicky
+ Williams.
+ **Online Test Generation with PathCrawler. Tool demo.**
+ Best demo award.
+ In Proc. of the 3rd International Workshop on Constraints in
+ Software Testing, Verification, and Analysis (CSTVA 2011), Berlin,
+ Germany, March 2011, IEEE Computer Society Press, 2011, ISBN
+ 978-1-4577-0019-4, pages 316-317.
+ <http://pathcrawler-online.com/pubs/kosmatov_brw_cstva_2011copy.pdf>
+ The final publication is available from IEEE.
+ <http://dx.doi.org/10.1109/ICSTW.2011.85>
+
+<!-- end list -->
+
+ - Nicky Williams and Nikolai Kosmatov.
+ **Structural Testing with PathCrawler. Tutorial Synopsis.**
+ In Proc. 12th International Conference on Quality Software (QSIC
+ 2012), Xi'an, China, August 27-29, 2012, IEEE Computer Society,
+ 2012, ISBN 978-0-7695-4833-3, pages 289-292.
+ <http://pathcrawler-online.com/pubs/qsic12copy.pdf>
+ The final publication will be available from IEEE.
+ <http://www.ieee.org>
+
+<!-- end list -->
+
+ - Nikolai Kosmatov, Nicky Williams, Bernard Botella, Muriel Roger,
+ Omar Chebaro.
+ **A Lesson on Structural Testing with PathCrawler-online.com.**
+ In Proc. Tests and Proofs - 6th International Conference, TAP 2012,
+ Prague, Czech Republic, May 31 - June 1, 2012, Springer, Lecture
+ Notes in Computer Science, vol. 7305, 2012, ISBN 978-3-642-30472-9,
+ pages 169-175.
+ <http://pathcrawler-online.com/pubs/tap_2012_pconline_final.pdf>
+ The final publication is available at www.springerlink.com.
+ <http://dx.doi.org/10.1007/978-3-642-30473-6_15>
# External Plug-ins
@@ -768,22 +856,39 @@ These plug-ins may be either closed or open source.
#### Cost
-```
- * Nicolas Ayache, Roberto M. Amadio and Yann Régis-Gianas. \\ ** Certifying and reasoning on cost annotations in C programs. **\\ In Proceedings of the 17th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2012), Paris, France, August 2012.\\ [[http://hal.inria.fr/hal-00702665]]\\ // We present a so-called labelling method to enrich a compiler in order to turn it into a “cost annotating compilerâ€, that is, a compiler which can lift pieces of information on the execution cost of the object code as cost annotations on the source code. These cost annotations characterize the execution costs of code fragments of constant complexity. ... we present a Frama-C plugin that uses our cost annotating compiler to automatically infer trustworthy logic assertions about the concrete worst case execution cost of programs written in a fragment of the C language. ... We report our experimentations on some C programs, especially programs generated by a compiler for the synchronous programming language Lustre used in critical embedded software.//
-```
-
-#### Fan-C
-
-```
- * Pascal Cuoq, David Delmas, Stéphane Duprat and Victoria Moya Lamiel.\\ **Fan-C, a Frama-C plug-in for data flow veri fication. **\\ In Proceedings of Embedded Real Time Software and Systems (ERTS'12). \\ [[http://www.erts2012.org/Site/0P2RUC89/5C-3.pdf]]
-```
+ - Nicolas Ayache, Roberto M. Amadio and Yann Régis-Gianas.
+ **Certifying and reasoning on cost annotations in C programs.**
+ In Proceedings of the 17th International Workshop on Formal Methods
+ for Industrial Critical Systems (FMICS 2012), Paris, France, August 2012.
+ <http://hal.inria.fr/hal-00702665>
+ *We present a so-called labelling method to enrich a compiler in
+ order to turn it into a “cost annotating compilerâ€, that is, a
+ compiler which can lift pieces of information on the execution cost
+ of the object code as cost annotations on the source code. These
+ cost annotations characterize the execution costs of code fragments
+ of constant complexity. ... we present a Frama-C plugin that uses
+ our cost annotating compiler to automatically infer trustworthy
+ logic assertions about the concrete worst case execution cost of
+ programs written in a fragment of the C language. ... We report our
+ experimentations on some C programs, especially programs generated
+ by a compiler for the synchronous programming language Lustre used
+ in critical embedded software.*
+
+#### Fan-C
+
+ - Pascal Cuoq, David Delmas, Stéphane Duprat and Victoria Moya
+ Lamiel.
+ **Fan-C, a Frama-C plug-in for data flow verification.**
+ In Proceedings of Embedded Real Time Software and Systems
+ (ERTS'12).
+ <http://www.erts2012.org/Site/0P2RUC89/5C-3.pdf>
#### SANTE
- Omar Chebaro, Nikolaï Kosmatov, Alain Giorgetti and Jacques
Julliand.
- \*\*The SANTE Tool: Value Analysis, Program Slicing and Test
- Generation for C Program Debugging. \*\*
+ **The SANTE Tool: Value Analysis, Program Slicing and Test
+ Generation for C Program Debugging.**
In Proceedings of the 5th International Conference on Tests & Proofs
(TAP 2011), Zurich, Switzerland, June 2011.
*This short paper presents a prototype tool called SANTE (Static
@@ -793,7 +898,7 @@ These plug-ins may be either closed or open source.
generate alarms when it can not guarantee the absence of errors.
Then the program is reduced by program slicing. Alarm-guided test
generation is then used to analyze the simplified program(s) in
- order to confirm or reject alarms. *
+ order to confirm or reject alarms.*
<!-- end list -->
@@ -815,14 +920,36 @@ These plug-ins may be either closed or open source.
technique independently.*
<!-- end list -->
-
-```
- * Omar Chebaro.\\ **Outil SANTE : Détection d’erreurs par analyse statique et test structurel des programmes C.**\\ In Proceedings of 10iemes Journées Francophones Internationales sur les Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'10), pages 75-79. June 2010. In French.
-```
-
-```
- * Omar Chebaro, Nikolaï Kosmatov, Alain Giorgetti and Jacques Julliand.\\ **Program slicing enhances a verification technique combining static and dynamic analysis.**\\ In Proceedings of the 27th Symposium On Applied Computing (SAC 2012), pages 1284-1291, Trento, Italy, March 2012.\\ //Recent research proposed efficient methods for software verification combining static and dynamic analysis, where static analysis reports possible runtime errors (some of which may be false alarms) and test generation confirms or rejects them. However, test generation may time out on real-sized programs before confirming some alarms as real bugs or rejecting some others as unreachable. To overcome this problem, we propose to reduce the source code by program slicing before test generation. This paper presents new optimized and adaptive usages of program slicing, provides underlying theoretical results and the algorithm these usages rely on. The method is implemented in a tool prototype called sante (Static ANalysis and TEsting). Our experiments show that our method with program slicing outperforms previous combinations of static and dynamic analysis. Moreover, simplifying the program makes it easier to analyze detected errors and remaining alarms. To appear.//
-```
+ - Omar Chebaro.
+ **Outil SANTE : Détection d’erreurs par analyse statique et test
+ structurel des programmes C.**
+ In Proceedings of 10iemes Journées Francophones Internationales sur
+ les Approches Formelles dans l'Assistance au Développement de
+ Logiciels (AFADL'10), pages 75-79. June 2010. In French.
+
+<!-- end list -->
+
+ - Omar Chebaro, Nikolaï Kosmatov, Alain Giorgetti and Jacques
+ Julliand.
+ **Program slicing enhances a verification technique combining static
+ and dynamic analysis.**
+ In Proceedings of the 27th Symposium On Applied Computing (SAC
+ 2012), pages 1284-1291, Trento, Italy, March 2012.
+ *Recent research proposed efficient methods for software
+ verification combining static and dynamic analysis, where static
+ analysis reports possible runtime errors (some of which may be false
+ alarms) and test generation confirms or rejects them. However, test
+ generation may time out on real-sized programs before confirming
+ some alarms as real bugs or rejecting some others as unreachable. To
+ overcome this problem, we propose to reduce the source code by
+ program slicing before test generation. This paper presents new
+ optimized and adaptive usages of program slicing, provides
+ underlying theoretical results and the algorithm these usages rely
+ on. The method is implemented in a tool prototype called sante
+ (Static ANalysis and TEsting). Our experiments show that our method
+ with program slicing outperforms previous combinations of static and
+ dynamic analysis. Moreover, simplifying the program makes it easier
+ to analyze detected errors and remaining alarms. To appear.*
#### SIDAN