From 87de0406706a0dbaaa58c8ab11d72b81fde19db1 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 7 Nov 2019 16:01:29 +0100
Subject: [PATCH] [publis] ^M seems to be important
---
dokuwiki/publications.md | 516 +++++++++++++++++++--------------------
1 file changed, 258 insertions(+), 258 deletions(-)
diff --git a/dokuwiki/publications.md b/dokuwiki/publications.md
index 45ac7877..1a073436 100644
--- a/dokuwiki/publications.md
+++ b/dokuwiki/publications.md
@@ -9,19 +9,19 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive,
### Manuals
- Loïc Correnson, Pascal Cuoq, Florent Kirchner, André Maroneze,
- Virgile Prevosto, Armand Puccetti, Julien Signoles, and Boris Yakobowski.
- **Frama-C User Manual.**
+ Virgile Prevosto, Armand Puccetti, Julien Signoles, and Boris Yakobowski.
+ **Frama-C User Manual.**
<http://frama-c.com/download/frama-c-user-manual.pdf>.
*The manual introducing common features to all analyzers.*
<!-- end list -->
-
+
- Julien Signoles, Thibaud Antignac, Loïc Correnson, Matthieu Lemerre,
and Virgile Prevosto.
**Frama-C Plug-in Development Guide**.
<http://frama-c.com/download/frama-c-plugin-development-guide.pdf>.
*The manual for developing a Frama-C plug-in.*
<!-- end list -->
-
+
- Patrick Baudin, Jean-Christophe Filliâtre, Claude Marché, Benjamin
Monate, Yannick Moy, and Virgile Prevosto.
**ACSL: ANSI/ISO C Specification Language.**.
@@ -39,42 +39,42 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive,
<http://dx.doi.org/10.1007/s00165-014-0326-7>.
Extended version of the following paper.
<!-- end list -->
-
- - Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto,
+
+ - Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto,
Julien Signoles, and Boris Yakobowski.
**Frama-C, A Software Analysis Perspective.**
- In proceedings of International Conference on Software Engineering
+ In proceedings of International Conference on Software Engineering
and Formal Methods 2012 (SEFM), October 2012.
- *This paper presents a synthetic view of Frama-C, its main and
+ *This paper presents a synthetic view of Frama-C, its main and
composite analyses, and some of its industrial achievements.*
<!-- end list -->
#### Articles about the Frama-C Kernel
-
- - Julien Signoles.
+
+ - Julien Signoles.
**Software Architecture of Code Analysis Frameworks Matters:
- The Frama-C Example.**
- In Formal Integrated Development Environment (F-IDE), June 2015.
- <http://julien.signoles.free.fr/publis/2015_fide.pdf>
+ The Frama-C Example.**
+ In Formal Integrated Development Environment (F-IDE), June 2015.
+ <http://julien.signoles.free.fr/publis/2015_fide.pdf>
*This papers presents the Frama-C architecture and discusses its design
- choices.*
+ choices.*
<!-- end list -->
-
+
- Loïc Correnson, and Julien Signoles.
**Combining Analyses for C Program Verification.**
- In proceedings of International Workshop on Formal Methods for
+ In proceedings of International Workshop on Formal Methods for
Industrial Critical Systems 2012 (FMICS), August 2012.
- <http://julien.signoles.free.fr/publis/2012_fmics.pdf>
- *This paper explains how Frama-C combines several partial results
- coming from its plug-ins into a fully consolidated validity status
+ <http://julien.signoles.free.fr/publis/2012_fmics.pdf>
+ *This paper explains how Frama-C combines several partial results
+ coming from its plug-ins into a fully consolidated validity status
for each program property.*
<!-- end list -->
-
+
- Pascal Cuoq, Damien Doligez, and Julien Signoles.
- **Lightweight Typed Customizable Unmarshaling.**
- In Workshop on ML, September 2011.
- <http://blog.frama-c.com/public/unmarshal.pdf>.
- *This short paper presents how Frama-C unmarshal its data.*
+ **Lightweight Typed Customizable Unmarshaling.**
+ In Workshop on ML, September 2011.
+ <http://blog.frama-c.com/public/unmarshal.pdf>.
+ *This short paper presents how Frama-C unmarshal its data.*
<!-- end list -->
- Pascal Cuoq, Julien Signoles, Patrick Baudin, Richard Bonichon,
@@ -176,9 +176,9 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive,
<!-- end list -->
- Pascal Cuoq and Damien Doligez.
- **Hashconsing in an incrementally garbage-collected system: a story
+ **Hashconsing in an incrementally garbage-collected system: a story
of weak pointers and hashconsing in OCaml 3.10.2.**
- In Workshop on ML, September 2008.
+ In Workshop on ML, September 2008.
*This article describes weak pointers, weak hashtables and hashconsing as
implemented in OCaml and used in a former version of Eva.*
<!-- end list -->
@@ -301,15 +301,231 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive,
*Presentation of the runtime memory model used by a former version of
E-ACSL.*
<!-- end list -->
-
-# Jessie
+
+# Aoraï
+
+#### Manual
+
+ - Nicolas Stouls.
+ **Aoraï Plug-in Tutorial.**
+ <http://frama-c.com/download/aorai/aorai-manual.pdf>.
+ *The official manual of the Frama-C plug-in Aoraï.*
+
+#### Founding Article
+
+ - Julien Groslambert and Nicolas Stouls.
+ **Vérification de propriétés LTL sur des programmes C par génération
+ d'annotations.**
+ <http://hal.archives-ouvertes.fr/inria-00568947/>
+ In Proceedings of Approches Formelles dans l'Assistance au
+ Développement de Logiciels 2009 (AFADL'09), January 2009. In
+ French.
+
+#### Case studies
+
+ - See [this page](/assets/dokuwiki/aorai-security) for a case study
+ showing the use of Aoraï in generating a threat scenario in a
+ driver.
+
+
+# Security Slicing
+
+#### Founding Article
+
+ - Benjamin Monate and Julien Signoles.
+ **Slicing for Security of Code.**
+ In Proceedings of the 1st international conference on Trusted
+ Computing and Trust in Information Technologies (TRUST'08), pages
+ 133--142, March 2008.
+ *Bugs in programs implementing security features can be
+ catastrophic: for example they may be exploited by malign users to
+ gain access to sensitive data. These exploits break the
+ confidentiality of information. All security analyses assume that
+ softwares implementing security features correctly implement the
+ security policy, *i.e.* are security bug-free. This assumption is
+ almost always wrong and IT security administrators consider that any
+ software that has no security patches on a regular basis should be
+ replaced as soon as possible. As programs implementing security
+ features are usually large, manual auditing is very error prone and
+ testing techniques are very expensive. This article proposes to
+ reduce the code that has to be audited by applying a program
+ reduction technique called *slicing*. Slicing transforms a source
+ code into an equivalent one according to a set of criteria. We show
+ that existing slicing criteria do *not* preserve the confidentiality
+ of information. We introduce a new automatic and correct
+ source-to-source method properly preserving the confidentiality of
+ information *i.e.* confidentiality is guaranteed to be exactly the
+ same in the original program and in the sliced program.*
+
+# 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>
+
+<!-- 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>
+
+<!-- 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
+
+These publications are related to Frama-C plug-ins which are not
+available from the official Frama-C website (<http://frama-c.com>).
+These plug-ins may be either closed or open source.
+
+
+## Jessie
+
+### Manual
+
- The main web page, including the manual and many other resources, is
<http://krakatoa.lri.fr/>
-#### Theses
+### Thesis
- Yannick Moy.
**Automatic Modular Static Safety Checking for C Programs.**
@@ -331,22 +547,24 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive,
Thèse de doctorat, Université Paris-Sud, October 2011.
<http://proval.lri.fr/publications/bardou11phd.pdf>.
-#### Founding Articles
+### Founding Articles
- Yannick Moy and Claude Marché.
**Modular inference of subprogram contracts for safety checking.**
In Journal of Symbolic Computation, 2010.
<http://hal.inria.fr/inria-00534331/en>
+<!-- end list -->
+
- Sylvie Boldo and Thi Minh Tuyen Nguyen.
**Hardware-independent proofs of numerical programs.**
In Proceedings of the Second NASA Formal Methods Symposium, April 2010.
- <http://shemesh.larc.nasa.gov/NFM2010/proceedings/NASA-CP-2010-216215.pdf>
+ <http://shemesh.larc.nasa.gov/NFM2010/proceedings/NASA-CP-2010-216215.pdf> <!-- end list -->
+
- Ali Ayad.
**On formal methods for certifying floating-point C
programs.**
Research Report RR-6927, INRIA, 2009.
<http://hal.inria.fr/inria-00383793/en/>
-
<!-- end list -->
- Yannick Moy.
@@ -370,7 +588,6 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive,
calculus and quantifier elimination. We instantiate this method to
prove memory safety for C and Java programs, under some memory
separation conditions.*
-
<!-- end list -->
- Yannick Moy.
@@ -404,7 +621,6 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive,
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.*
-
<!-- end list -->
- Yannick Moy.
@@ -420,9 +636,8 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive,
Bornat encoding. We present an automatic translation from C to an
intermediate language Jessie on which this extended interpretation
is performed.*
-
<!-- end list -->
-
+
- Yannick Moy and Claude Marché.
**Inferring local (non-)aliasing and strings for memory safety.**
In Proceedings of Heap Analysis and Verification (HAV’07), Braga,
@@ -451,7 +666,6 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive,
method in Caduceus, a tool for the verification of C programs, and
successfully generated appropriate annotations for the C standard
string library functions.*
-
<!-- end list -->
- Thierry Hubert and Claude Marché.
@@ -460,7 +674,7 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive,
Portugal, March 2007.
<http://www.lri.fr/~marche/hubert07hav.pdf>
-#### Other Articles
+### Other Articles
- Jochen Burghardt, Jens Gerlach, Hans Pohl and Juan Soto.
**An Experience Report on the Verification of Algorithms in the C++
@@ -553,223 +767,9 @@ 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.*
-
-# Aoraï
-
-#### Manual
-
- - Nicolas Stouls.
- **Aoraï Plug-in Tutorial.**
- <http://frama-c.com/download/aorai/aorai-manual.pdf>.
- *The official manual of the Frama-C plug-in Aoraï.*
-
-#### Founding Article
-
- - Julien Groslambert and Nicolas Stouls.
- **Vérification de propriétés LTL sur des programmes C par génération
- d'annotations.**
- <http://hal.archives-ouvertes.fr/inria-00568947/>
- In Proceedings of Approches Formelles dans l'Assistance au
- Développement de Logiciels 2009 (AFADL'09), January 2009. In
- French.
-
-#### Case studies
-
- - See [this page](/assets/dokuwiki/aorai-security) for a case study
- showing the use of Aoraï in generating a threat scenario in a
- driver.
-
-
-# Security Slicing
-
-#### Founding Article
-
- - Benjamin Monate and Julien Signoles.
- **Slicing for Security of Code.**
- In Proceedings of the 1st international conference on Trusted
- Computing and Trust in Information Technologies (TRUST'08), pages
- 133--142, March 2008.
- *Bugs in programs implementing security features can be
- catastrophic: for example they may be exploited by malign users to
- gain access to sensitive data. These exploits break the
- confidentiality of information. All security analyses assume that
- softwares implementing security features correctly implement the
- security policy, *i.e.* are security bug-free. This assumption is
- almost always wrong and IT security administrators consider that any
- software that has no security patches on a regular basis should be
- replaced as soon as possible. As programs implementing security
- features are usually large, manual auditing is very error prone and
- testing techniques are very expensive. This article proposes to
- reduce the code that has to be audited by applying a program
- reduction technique called *slicing*. Slicing transforms a source
- code into an equivalent one according to a set of criteria. We show
- that existing slicing criteria do *not* preserve the confidentiality
- of information. We introduce a new automatic and correct
- source-to-source method properly preserving the confidentiality of
- information *i.e.* confidentiality is guaranteed to be exactly the
- same in the original program and in the sliced program.*
-
-# 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>
-
-<!-- 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>
-
-<!-- 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
-
-These publications are related to Frama-C plug-ins which are not
-available from the official Frama-C website (<http://frama-c.com>).
-These plug-ins may be either closed or open source.
-#### Cost
+## Cost
- Nicolas Ayache, Roberto M. Amadio and Yann Régis-Gianas.
**Certifying and reasoning on cost annotations in C programs.**
@@ -789,7 +789,7 @@ These plug-ins may be either closed or open source.
by a compiler for the synchronous programming language Lustre used
in critical embedded software.*
-#### Fan-C
+## Fan-C
- Pascal Cuoq, David Delmas, Stéphane Duprat and Victoria Moya
Lamiel.
@@ -798,7 +798,7 @@ These plug-ins may be either closed or open source.
(ERTS'12).
<http://www.erts2012.org/Site/0P2RUC89/5C-3.pdf>
-#### SANTE
+## SANTE
- Omar Chebaro, Nikolaï Kosmatov, Alain Giorgetti and Jacques
Julliand.
@@ -866,7 +866,7 @@ These plug-ins may be either closed or open source.
dynamic analysis. Moreover, simplifying the program makes it easier
to analyze detected errors and remaining alarms. To appear.*
-#### SIDAN
+## SIDAN
- Jonathan-Christopher Demay, Éric Totel and Frédéric Tronel.
**SIDAN: a tool dedicated to Software Instrumentation for Detecting
@@ -874,7 +874,7 @@ These plug-ins may be either closed or open source.
4th International Conference on Risks and Security of Internet and
Systems (CRISIS'2009), October 2009.
-#### STAC
+## STAC
- Dumitru Ceara, Laurent Mounier and Marie-Laure Potet.
**Taint Dependency Sequences: a characterization of insecure
@@ -882,7 +882,7 @@ These plug-ins may be either closed or open source.
Modeling and Detecting Vulnerabilities workshop (MDV'10), associated
to ICST 2010, April 2010.
-#### Taster
+## Taster
- David Delmas, Stéphane Duprat, Victoria Moya Lamiel and Julien
Signoles.
--
GitLab