Skip to content
Snippets Groups Projects
Commit 87de0406 authored by Julien Signoles's avatar Julien Signoles Committed by Allan Blanchard
Browse files

[publis] ^M seems to be important

parent ee5d0eb4
No related branches found
No related tags found
1 merge request!11publis
Hide whitespace changes
Inline Side-by-side
dokuwiki/publications.md
+ 258
− 258
View file @ 87de0406
...@@ -9,19 +9,19 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive, ...@@ -9,19 +9,19 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive,
### Manuals ### Manuals
- Loïc Correnson, Pascal Cuoq, Florent Kirchner, André Maroneze, - Loïc Correnson, Pascal Cuoq, Florent Kirchner, André Maroneze,
Virgile Prevosto, Armand Puccetti, Julien Signoles, and Boris Yakobowski. Virgile Prevosto, Armand Puccetti, Julien Signoles, and Boris Yakobowski.
**Frama-C User Manual.** **Frama-C User Manual.**
<http://frama-c.com/download/frama-c-user-manual.pdf>. <http://frama-c.com/download/frama-c-user-manual.pdf>.
*The manual introducing common features to all analyzers.* *The manual introducing common features to all analyzers.*
<!-- end list --> <!-- end list -->
- Julien Signoles, Thibaud Antignac, Loïc Correnson, Matthieu Lemerre, - Julien Signoles, Thibaud Antignac, Loïc Correnson, Matthieu Lemerre,
and Virgile Prevosto. and Virgile Prevosto.
**Frama-C Plug-in Development Guide**. **Frama-C Plug-in Development Guide**.
<http://frama-c.com/download/frama-c-plugin-development-guide.pdf>. <http://frama-c.com/download/frama-c-plugin-development-guide.pdf>.
*The manual for developing a Frama-C plug-in.* *The manual for developing a Frama-C plug-in.*
<!-- end list --> <!-- end list -->
- Patrick Baudin, Jean-Christophe Filliâtre, Claude Marché, Benjamin - Patrick Baudin, Jean-Christophe Filliâtre, Claude Marché, Benjamin
Monate, Yannick Moy, and Virgile Prevosto. Monate, Yannick Moy, and Virgile Prevosto.
**ACSL: ANSI/ISO C Specification Language.**. **ACSL: ANSI/ISO C Specification Language.**.
...@@ -39,42 +39,42 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive, ...@@ -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>. <http://dx.doi.org/10.1007/s00165-014-0326-7>.
Extended version of the following paper. Extended version of the following paper.
<!-- end list --> <!-- end list -->
- Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, - Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto,
Julien Signoles, and Boris Yakobowski. Julien Signoles, and Boris Yakobowski.
**Frama-C, A Software Analysis Perspective.** **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. 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.* composite analyses, and some of its industrial achievements.*
<!-- end list --> <!-- end list -->
#### Articles about the Frama-C Kernel #### Articles about the Frama-C Kernel
- Julien Signoles. - Julien Signoles.
**Software Architecture of Code Analysis Frameworks Matters: **Software Architecture of Code Analysis Frameworks Matters:
The Frama-C Example.** The Frama-C Example.**
In Formal Integrated Development Environment (F-IDE), June 2015. In Formal Integrated Development Environment (F-IDE), June 2015.
<http://julien.signoles.free.fr/publis/2015_fide.pdf> <http://julien.signoles.free.fr/publis/2015_fide.pdf>
*This papers presents the Frama-C architecture and discusses its design *This papers presents the Frama-C architecture and discusses its design
choices.* choices.*
<!-- end list --> <!-- end list -->
- Loïc Correnson, and Julien Signoles. - Loïc Correnson, and Julien Signoles.
**Combining Analyses for C Program Verification.** **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. Industrial Critical Systems 2012 (FMICS), August 2012.
<http://julien.signoles.free.fr/publis/2012_fmics.pdf> <http://julien.signoles.free.fr/publis/2012_fmics.pdf>
*This paper explains how Frama-C combines several partial results *This paper explains how Frama-C combines several partial results
coming from its plug-ins into a fully consolidated validity status coming from its plug-ins into a fully consolidated validity status
for each program property.* for each program property.*
<!-- end list --> <!-- end list -->
- Pascal Cuoq, Damien Doligez, and Julien Signoles. - Pascal Cuoq, Damien Doligez, and Julien Signoles.
**Lightweight Typed Customizable Unmarshaling.** **Lightweight Typed Customizable Unmarshaling.**
In Workshop on ML, September 2011. In Workshop on ML, September 2011.
<http://blog.frama-c.com/public/unmarshal.pdf>. <http://blog.frama-c.com/public/unmarshal.pdf>.
*This short paper presents how Frama-C unmarshal its data.* *This short paper presents how Frama-C unmarshal its data.*
<!-- end list --> <!-- end list -->
- Pascal Cuoq, Julien Signoles, Patrick Baudin, Richard Bonichon, - 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, ...@@ -176,9 +176,9 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive,
<!-- end list --> <!-- end list -->
- Pascal Cuoq and Damien Doligez. - 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.** 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 *This article describes weak pointers, weak hashtables and hashconsing as
implemented in OCaml and used in a former version of Eva.* implemented in OCaml and used in a former version of Eva.*
<!-- end list --> <!-- end list -->
...@@ -301,15 +301,231 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive, ...@@ -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 *Presentation of the runtime memory model used by a former version of
E-ACSL.* E-ACSL.*
<!-- end list --> <!-- 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 #### 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 - The main web page, including the manual and many other resources, is
<http://krakatoa.lri.fr/> <http://krakatoa.lri.fr/>
#### Theses ### Thesis
- Yannick Moy. - Yannick Moy.
**Automatic Modular Static Safety Checking for C Programs.** **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, ...@@ -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. Thèse de doctorat, Université Paris-Sud, October 2011.
<http://proval.lri.fr/publications/bardou11phd.pdf>. <http://proval.lri.fr/publications/bardou11phd.pdf>.
#### Founding Articles ### Founding Articles
- Yannick Moy and Claude Marché. - Yannick Moy and Claude Marché.
**Modular inference of subprogram contracts for safety checking.** **Modular inference of subprogram contracts for safety checking.**
In Journal of Symbolic Computation, 2010. In Journal of Symbolic Computation, 2010.
<http://hal.inria.fr/inria-00534331/en> <http://hal.inria.fr/inria-00534331/en>
<!-- end list -->
- Sylvie Boldo and Thi Minh Tuyen Nguyen. - Sylvie Boldo and Thi Minh Tuyen Nguyen.
**Hardware-independent proofs of numerical programs.** **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> <http://shemesh.larc.nasa.gov/NFM2010/proceedings/NASA-CP-2010-216215.pdf> <!-- end list -->
- Ali Ayad. - Ali Ayad.
**On formal methods for certifying floating-point C **On formal methods for certifying floating-point C
programs.** programs.**
Research Report RR-6927, INRIA, 2009. Research Report RR-6927, INRIA, 2009.
<http://hal.inria.fr/inria-00383793/en/> <http://hal.inria.fr/inria-00383793/en/>
<!-- end list --> <!-- end list -->
- Yannick Moy. - Yannick Moy.
...@@ -370,7 +588,6 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive, ...@@ -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 calculus and quantifier elimination. We instantiate this method to
prove memory safety for C and Java programs, under some memory prove memory safety for C and Java programs, under some memory
separation conditions.* separation conditions.*
<!-- end list --> <!-- end list -->
- Yannick Moy. - Yannick Moy.
...@@ -404,7 +621,6 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive, ...@@ -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 iterating around loops. We implemented our method in Caduceus, a
tool for the verification of C programs, and successfully verified 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 --> <!-- end list -->
- Yannick Moy. - Yannick Moy.
...@@ -420,9 +636,8 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive, ...@@ -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 Bornat encoding. We present an automatic translation from C to an
intermediate language Jessie on which this extended interpretation intermediate language Jessie on which this extended interpretation
is performed.* is performed.*
<!-- end list --> <!-- end list -->
- Yannick Moy and Claude Marché. - Yannick Moy and Claude Marché.
**Inferring local (non-)aliasing and strings for memory safety.** **Inferring local (non-)aliasing and strings for memory safety.**
In Proceedings of Heap Analysis and Verification (HAV’07), Braga, 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, ...@@ -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 method in Caduceus, a tool for the verification of C programs, and
successfully generated appropriate annotations for the C standard successfully generated appropriate annotations for the C standard
string library functions.* string library functions.*
<!-- end list --> <!-- end list -->
- Thierry Hubert and Claude Marché. - Thierry Hubert and Claude Marché.
...@@ -460,7 +674,7 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive, ...@@ -460,7 +674,7 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive,
Portugal, March 2007. Portugal, March 2007.
<http://www.lri.fr/~marche/hubert07hav.pdf> <http://www.lri.fr/~marche/hubert07hav.pdf>
#### Other Articles ### Other Articles
- Jochen Burghardt, Jens Gerlach, Hans Pohl and Juan Soto. - Jochen Burghardt, Jens Gerlach, Hans Pohl and Juan Soto.
**An Experience Report on the Verification of Algorithms in the C++ **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 ...@@ -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 arising in a C implementation of the algorithm do not affect its
correctness. The technique is illustrated using an algorithm for correctness. The technique is illustrated using an algorithm for
detecting loss of separation among aircraft.* 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. - Nicolas Ayache, Roberto M. Amadio and Yann Régis-Gianas.
**Certifying and reasoning on cost annotations in C programs.** **Certifying and reasoning on cost annotations in C programs.**
...@@ -789,7 +789,7 @@ These plug-ins may be either closed or open source. ...@@ -789,7 +789,7 @@ These plug-ins may be either closed or open source.
by a compiler for the synchronous programming language Lustre used by a compiler for the synchronous programming language Lustre used
in critical embedded software.* in critical embedded software.*
#### Fan-C ## Fan-C
- Pascal Cuoq, David Delmas, Stéphane Duprat and Victoria Moya - Pascal Cuoq, David Delmas, Stéphane Duprat and Victoria Moya
Lamiel. Lamiel.
...@@ -798,7 +798,7 @@ These plug-ins may be either closed or open source. ...@@ -798,7 +798,7 @@ These plug-ins may be either closed or open source.
(ERTS'12). (ERTS'12).
<http://www.erts2012.org/Site/0P2RUC89/5C-3.pdf> <http://www.erts2012.org/Site/0P2RUC89/5C-3.pdf>
#### SANTE ## SANTE
- Omar Chebaro, Nikolaï Kosmatov, Alain Giorgetti and Jacques - Omar Chebaro, Nikolaï Kosmatov, Alain Giorgetti and Jacques
Julliand. Julliand.
...@@ -866,7 +866,7 @@ These plug-ins may be either closed or open source. ...@@ -866,7 +866,7 @@ These plug-ins may be either closed or open source.
dynamic analysis. Moreover, simplifying the program makes it easier dynamic analysis. Moreover, simplifying the program makes it easier
to analyze detected errors and remaining alarms. To appear.* to analyze detected errors and remaining alarms. To appear.*
#### SIDAN ## SIDAN
- Jonathan-Christopher Demay, Éric Totel and Frédéric Tronel. - Jonathan-Christopher Demay, Éric Totel and Frédéric Tronel.
**SIDAN: a tool dedicated to Software Instrumentation for Detecting **SIDAN: a tool dedicated to Software Instrumentation for Detecting
...@@ -874,7 +874,7 @@ These plug-ins may be either closed or open source. ...@@ -874,7 +874,7 @@ These plug-ins may be either closed or open source.
4th International Conference on Risks and Security of Internet and 4th International Conference on Risks and Security of Internet and
Systems (CRISIS'2009), October 2009. Systems (CRISIS'2009), October 2009.
#### STAC ## STAC
- Dumitru Ceara, Laurent Mounier and Marie-Laure Potet. - Dumitru Ceara, Laurent Mounier and Marie-Laure Potet.
**Taint Dependency Sequences: a characterization of insecure **Taint Dependency Sequences: a characterization of insecure
...@@ -882,7 +882,7 @@ These plug-ins may be either closed or open source. ...@@ -882,7 +882,7 @@ These plug-ins may be either closed or open source.
Modeling and Detecting Vulnerabilities workshop (MDV'10), associated Modeling and Detecting Vulnerabilities workshop (MDV'10), associated
to ICST 2010, April 2010. to ICST 2010, April 2010.
#### Taster ## Taster
- David Delmas, Stéphane Duprat, Victoria Moya Lamiel and Julien - David Delmas, Stéphane Duprat, Victoria Moya Lamiel and Julien
Signoles. Signoles.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment