\*\*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/>
...
@@ -391,9 +389,8 @@ when possible and only if they do respect copyright.
...
@@ -391,9 +389,8 @@ when possible and only if they do respect copyright.
- Yannick Moy.
- Yannick Moy.
**Sufficient Preconditions for Modular Assertion Checking.**
**Sufficient Preconditions for Modular Assertion Checking.**
In Proceedings of the 9th International Conference on Verification,
In Proceedings of the 9th International Conference on Verification,
Model Checking, and Abstract Interpretation (VMCAI'08). January
Model Checking, and Abstract Interpretation (VMCAI'08). January 2008.
2008.
*Assertion checking is the restriction of program verification to
//Assertion checking is the restriction of program verification to
validity of program assertions. It encompasses safety checking,
validity of program assertions. It encompasses safety checking,
which is program verification of safety properties, like memory
which is program verification of safety properties, like memory
safety or absence of overflows. In this paper, we consider assertion
safety or absence of overflows. In this paper, we consider assertion
...
@@ -409,14 +406,14 @@ when possible and only if they do respect copyright.
...
@@ -409,14 +406,14 @@ when possible and only if they do respect copyright.
programs. It combines abstract interpretation, weakest precondition
programs. It combines abstract interpretation, weakest precondition
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.
**Checking C Pointer Programs for Memory Safety.**
**Checking C Pointer Programs for Memory Safety.**
INRIA Research Report n°6334, October 2007.
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
pointer programs that do not include casts, structures, double
indirection and memory deallocation. This involves first identifying
indirection and memory deallocation. This involves first identifying
aliasing and strings, which we do in a local setting rather than
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.
...
@@ -443,15 +440,14 @@ when possible and only if they do respect copyright.
refinement operators, this propagation method does not require
refinement operators, this propagation method does not require
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.
**Union and Cast in Deductive Verification.**
**Union and Cast in Deductive Verification.**
In Proceedings of the C/C++ Verification Workshop (CCV'07), July
In Proceedings of the C/C++ Verification Workshop (CCV'07), July 2007.
2007.
*Deductive verification based on weakest-precondition calculus has
//Deductive verification based on weakest-precondition calculus has
proved effective at proving imperative programs, through a suitable
proved effective at proving imperative programs, through a suitable
encoding of memory as functional arrays (a.k.a. the Burstall-Bornat
encoding of memory as functional arrays (a.k.a. the Burstall-Bornat
model). Unfortunately, this encoding of memory makes it impossible
model). Unfortunately, this encoding of memory makes it impossible
...
@@ -460,7 +456,7 @@ when possible and only if they do respect copyright.
...
@@ -460,7 +456,7 @@ when possible and only if they do respect copyright.
structure subtyping, on which it is possible to extend the Burstall-
structure subtyping, on which it is possible to extend the Burstall-
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 -->
...
@@ -468,7 +464,7 @@ when possible and only if they do respect copyright.
...
@@ -468,7 +464,7 @@ when possible and only if they do respect copyright.
**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,
Portugal, March 2007.
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
pointer programs, by combining deductive verification and abstract
interpretation techniques. The approach is modular and contextual,
interpretation techniques. The approach is modular and contextual,
thanks to the use of Hoare-style annotations (pre- and
thanks to the use of Hoare-style annotations (pre- and
...
@@ -491,7 +487,7 @@ when possible and only if they do respect copyright.
...
@@ -491,7 +487,7 @@ when possible and only if they do respect copyright.
way, in the framework of abstract interpretation. We implemented our
way, in the framework of abstract interpretation. We implemented our
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 -->
...
@@ -581,21 +577,19 @@ when possible and only if they do respect copyright.
...
@@ -581,21 +577,19 @@ when possible and only if they do respect copyright.
**Verification of Numerical Programs: From Real Numbers to Floating
**Verification of Numerical Programs: From Real Numbers to Floating
Point Numbers.**
Point Numbers.**
In NASA Formal Methods 2013.
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,
the infinitely precise realm of the field of real numbers. However,
numerical computations in these algorithms are often implemented
numerical computations in these algorithms are often implemented
using floating point numbers. The use of a finite representation of
using floating point numbers. The use of a finite representation of
real numbers introduces uncertainties as to whether the properties
real numbers introduces uncertainties as to whether the properties
verified in the theoretical setting hold in practice. This short
verified in the theoretical setting hold in practice. This short
paper describes work in progress aimed at addressing these concerns.
paper describes work in progress aimed at addressing these concerns.
Given a
Given a formally proven algorithm, written in the Program Verification System
formally proven algorithm, written in the Program Verification System
(PVS), the Frama-C suite of tools is used to identify sufficient
(PVS), the Frama-C suite of tools is used to identify sufficient
conditions and verify that under such conditions the rounding errors
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ï
# Aoraï
...
@@ -680,7 +674,7 @@ detecting loss of separation among aircraft.//
...
@@ -680,7 +674,7 @@ detecting loss of separation among aircraft.//
In Proceedings of the 1st international conference on Trusted
In Proceedings of the 1st international conference on Trusted
Computing and Trust in Information Technologies (TRUST'08), pages
Computing and Trust in Information Technologies (TRUST'08), pages
133--142, March 2008.
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
catastrophic: for example they may be exploited by malign users to
gain access to sensitive data. These exploits break the
gain access to sensitive data. These exploits break the
confidentiality of information. All security analyses assume that
confidentiality of information. All security analyses assume that
...
@@ -698,67 +692,161 @@ detecting loss of separation among aircraft.//
...
@@ -698,67 +692,161 @@ detecting loss of separation among aircraft.//
of information. We introduce a new automatic and correct
of information. We introduce a new automatic and correct
source-to-source method properly preserving the confidentiality of
source-to-source method properly preserving the confidentiality of
information *i.e.* confidentiality is guaranteed to be exactly the
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
# PathCrawler
#### Manual
#### Manual
```
***PathCrawler Automatic Test Generation Tool For C Programs User Manual Version 3.1.**
* **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.//
*The user manual of the Frama-C plug-in PathCrawler.*
#### Founding Articles
#### Founding Articles
```
- Nicky Williams, Bruno Marre and Patricia Mouy.
* 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]]
**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
* 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]]
Computer Society, 2004, ISBN 0-7695-2131-2, pages 290-293.
- 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
#### Other Articles
```
- Nicky Williams.
* 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]]
**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 -
* 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]]
<!-- end list -->
```
- Patricia Mouy, Bruno Marre, Nicky Williams and Pascale Le Gall.
```
**Generation of all-paths unit test with function calls.**
* 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]]
In Proc. 1st Intl. Conference on Software Testing, Verification, and
```
Validation, ICST 2008, Lillehammer, Norway, April 9-11, 2008, IEEE
* 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]]
```
- Nikolai Kosmatov.
**All-paths test generation for programs with internal aliases.**
```
In Proc. 19th Intl. Symposium on Software Reliability Engineering
* 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]]
<http://dx.doi.org/10.1109/ISSRE.2008.25>
```
<!-- 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]]
- 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.**
* 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]]
In Proc. 4th Intl. Workshop on Automation of Software Test, AST
```
2009, Vancouver, BC, Canada, May 18-19, 2009, IEEE Computer Society
The final publication is available at www.springerlink.com.
<http://dx.doi.org/10.1007/978-3-642-30473-6_15>
# External Plug-ins
# External Plug-ins
...
@@ -768,22 +856,39 @@ These plug-ins may be either closed or open source.
...
@@ -768,22 +856,39 @@ 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. **\\ 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.//
**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.
#### Fan-C
<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
* 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]]
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
#### SANTE
- Omar Chebaro, Nikolaï Kosmatov, Alain Giorgetti and Jacques
- Omar Chebaro, Nikolaï Kosmatov, Alain Giorgetti and Jacques
Julliand.
Julliand.
\*\*The SANTE Tool: Value Analysis, Program Slicing and Test
**The SANTE Tool: Value Analysis, Program Slicing and Test
Generation for C Program Debugging.\*\*
Generation for C Program Debugging.**
In Proceedings of the 5th International Conference on Tests & Proofs
In Proceedings of the 5th International Conference on Tests & Proofs
(TAP 2011), Zurich, Switzerland, June 2011.
(TAP 2011), Zurich, Switzerland, June 2011.
*This short paper presents a prototype tool called SANTE (Static
*This short paper presents a prototype tool called SANTE (Static
...
@@ -793,7 +898,7 @@ These plug-ins may be either closed or open source.
...
@@ -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.
generate alarms when it can not guarantee the absence of errors.
Then the program is reduced by program slicing. Alarm-guided test
Then the program is reduced by program slicing. Alarm-guided test
generation is then used to analyze the simplified program(s) in
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 -->
<!-- end list -->
...
@@ -815,14 +920,36 @@ These plug-ins may be either closed or open source.
...
@@ -815,14 +920,36 @@ These plug-ins may be either closed or open source.
technique independently.*
technique independently.*
<!-- end list -->
<!-- end list -->
- Omar Chebaro.
```
**Outil SANTE : Détection d’erreurs par analyse statique et test
* 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.
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.//
```
<!-- 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.*
