Skip to content
Snippets Groups Projects
Commit f0626839 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

Removes dokuwiki pages that are now elsewhere

parent 8aa6ba8b
No related branches found
No related tags found
1 merge request!49New tutorials and teaching pages
---
layout: clean_page
---
Below is the list of exercices done with Frama-C during the Static
Analysis Course at ENSIIE:
* [2010-2011](/dokuwiki/ensiie2010-2011-ias-tp.html)
* [2011-2012](/dokuwiki/ensiie2011-2012-ias-tp.html)
* [2012-2013](/dokuwiki/ensiie2012-2013-ias-tp.html)
* [2013-2014](/dokuwiki/ensiie2013-2014-ias-tp.html)
* [2014-2015](/dokuwiki/ensiie2014-2015-ias-tp.html)
* [2015-2016](/dokuwiki/ensiie2015-2016-ias-tp.html)
* [2016-2017](/dokuwiki/ensiie2016-2017-ias-tp.html)
* [2017-2018](/dokuwiki/ensiie2017-2018-ias-tp.html)
---
layout: clean_page
---
# Exercises on Frama-C
## Value Analysis plug-in
- [Lab work at ENSIIE - 2014 (in French)](/dokuwiki/ensiie2013-2014-ias-tp.html)
- [Lab work at ENSIIE - 2013 (in French)](/dokuwiki/ensiie2012-2013-ias-tp.html)
- [Lab work at ENSIIE - 2012 (in French)](/dokuwiki/ensiie2011-2012-ias-tp.html)
- [Lab work at ENSIIE - 2011 (in French)](/dokuwiki/ensiie2010-2011-ias-tp.html)
## WP plug-in
- [Deductive Verification at University Paris Saclay (since 2015)](/dokuwiki/UPS-2015.html)
- [Lab work at UFC - 2013-2014: WP (in French)](/dokuwiki/ufc2013-2014-pep-tp.html)
---
layout: clean_page
---
# Jessie
This page presents some tips about the [Jessie
plugin](http://frama-c.com/jessie.html) of Frama-C.
## Extracting proof obligation from a Jessie project
<http://cavale.gforge.enseeiht.fr/files/extract_obligation>
```
usage: extract_obligation -f=funname -o=obligation [-s=solver] sources
Options:
-s=<solver> or --solver=<solver> with solver in {coq,smtlib,alt-ergo} (default is coq)
-f=<fun> or --function=<fun> with fun a function in sources
-o=<obl> or --obligation=<obl> with obl an obligation associated to the function (the name in available in the frama-c gui with jessie plugin)\\
```
## Known issues
To submit a bug for the tools of the Why platform, visit
<https://gforge.inria.fr/tracker/?atid=4012&group_id=999&func=browse>
- **\\sum, \\prod, etc. are not supported by Jessie**
See [this
message](http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-March/000985.html)
from frama-c-discuss.
<!-- end list -->
- **Timeout for provers not working under MS-Windows**
This is a known issue in Why 2.18 and earlier versions. See [this
fix](http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2008-December/000301.html).
<!-- end list -->
- **Code highlighting in gWhy does not work**
This may happen when processing DOS-encoded files.
Fix: Convert file to unix encoding (C-x RET f undecided-unix in
Emacs).
---
layout: clean_page
---
# Frama-C in teaching
This page lists various courses that are using Frama-C in their lab
lessons.
## In English
- [University of Minho: Formal Methods in Software
Engineering](http://mei.di.uminho.pt/?q=en/1112/mfes-uk)
- [University College London: Language-based
security](http://www.mupuf.org/blog/2014/02/10/a_return_into_the_world_of_frama-c)
## In French
- [ENSIIE Evry: Static Analysis of Programs](/dokuwiki/ensiie.html)
- [École Polytechnique: Initiation to Program
Proof](http://www.enseignement.polytechnique.fr/profs/informatique/Sylvie.Putot/Enseignement/SemantiqueValidation/TP6.html)
## In other languages
- [Moscow State University: Formal Specification and Verification (in
Russian)](http://sed.ispras.ru/fmprac)
---
layout: clean_page
---
- [rv-2013](/dokuwiki/tutorial/rv-2013.html): tutorial held at
[RV 2013](http://rv2013.gforge.inria.fr/) in Rennes (France).
- [ifm-2013](/dokuwiki/tutorial/ifm-2013.html): tutorial held at
[iFM 2013](http://www.it.abo.fi/iFM2013/) in Turku (Finland).
- [Stance](/dokuwiki/tutorial/Stance.html): Training sessions done
within the [Stance](http://www.stance-project.eu/) FP7 project.
- [MERCE 2013](/dokuwiki/tutorial/MERCE_2013.html): Training
session made by Mitsubishi Electric R\&D Centre Europe in 2013
- [LIFO-2014](/dokuwiki/tutorial/LIFO-2014.html): presentation of WP
made at the LIFO laboratory of Orléans University
A tutorial on the [WP plugin](http://www.frama-c.com/wp.html) has been
given at
[iFM 2013](http://www.it.abo.fi/iFM2013/workshops_and_tutorials.php) in
Turku (Finland), on June 11th, 2013.
[Slides](/assets/dokuwiki/tutorial/ifm-2013/slides.pdf) and [C
examples](/assets/dokuwiki/tutorial/ifm-2013/frama_c_tutorial_examples.tar.gz)
are available.
The examples archive contains both unannotated implementation as
exercises and a solution that can be entirely verified by the WP plug-in
as distributed in the Fluorine 2 (20130501) version of Frama-C. For the
more advanced examples, some special options of wp are needed in order
for the provers to complete the proof automatically. Theses options are
given at the bottom of each file.
This page gather material that has been presented at the seminar of the
[LIFO laboratory](http://www.univ-orleans.fr/lifo/?lang=en) of Orléans
University on 2014-10-13.
- [slides from the
presentation](/mantis/frama-c/tutorial/lifo-2014/slides.pdf)
- [annotated
programs](/mantis/frama-c/tutorial/lifo-2014/solutions.tar.gz)
corresponding to the code shown in the slides. Note that the lemmas
in `binary_search_tree.c` cannot be discharged in the current
version of Frama-C, because WP does not generate a complete
environment.
Some [presentation
slides](/assets/dokuwiki/tutorial/introduction-to-frama-c_v2.pdf) and
[examples](/assets/dokuwiki/tutorial/introduction-slides-examples.tar.gz)
are used within Mitsubishi Electric.
A tutorial on the [E-ACSL plugin](http://www.frama-c.com/eacsl.html) has
been given at [RV 2013](http://rv2013.gforge.inria.fr/) in Rennes
(France), on September 24th, 2013.
[Slides](/assets/dokuwiki/tutorial/slides.pdf) and [C
examples](/assets/dokuwiki/tutorial/eacsl_examples.tgz) are available.
The examples archive contains both unannotated implementation as
exercises and a solution that can be entirely run by the E-ACSL plug-in
version 0.3 (with Frama-C Fluorine 20130601). The exact way to run each
example is given at the bottom of the corresponding file.
Within the Stance project, some training sessions on Frama-C have been
organized. This includes in particular the following presentations:
- Overview of the platform:
[slides](/assets/dokuwiki/tutorial/frama_c_overview.pdf) and
[example of a very simple
plugin](/assets/dokuwiki/tutorial/simple_metrics.ml)
- Value Analysis:
[slides](/assets/dokuwiki/tutorial/stance/value_tutorial.pdf) and
[code
examples](/assets/dokuwiki/tutorial/stance/value_examples.tar.gz)
- WP (advanced presentation, following a first course):
[slides](/assets/dokuwiki/tutorial/wp_advanced_slides.pdf) and
[code examples](/assets/dokuwiki/frama-c/tutorial/wp_examples.tar.gz)
---
layout: clean_page
---
# Travaux Pratiques Frama-C / WP
Université de Franche-Comté, Master 1 Informatique PEP, Année 2013-2014
Enseignants : Guillaume PETIOT, Alain GIORGETTI, Jacques JULLIAND
## Introduction
Le but de ces TP est d'utiliser l'outil [Frama-C](http://frama-c.com) et
en particulier son outil de vérification déductive
[WP](http://frama-c.com/wp.html). La version installée à l'université de
Franche-Comté est Fluorine 3 :
[Fluorine-20130601](http://frama-c.com/download.html).
## Première séance
[tp1.pdf](/assets/dokuwiki/tp1.pdf) [va.pdf](/assets/dokuwiki/va.pdf)
## Seconde séance
(bientôt)
---
layout: clean_page
---
## Deductive Verification with Frama-C/WP
Context: course on Deductive Verification in [master
FIIL](https://www.universite-paris-saclay.fr/en/education/master/m2-fondements-de-linformatique-et-ingenierie-du-logiciel-foundations-of-computer#presentation-m2)
(2d year) at [University
Paris-Saclay](https://www.universite-paris-saclay.fr/en) (France), since
2015.
Teachers: [Andrei Paskevich](http://tertium.org/) (Why3) and [Julien
Signoles](http://julien.signoles.free.fr/index.en.html) (Frama-C).
Our exercises use both Frama-C/WP and [Why3](http://why3.lri.fr/) ([in a
browser](http://why3.lri.fr/try/)). [A
tarball](/assets/dokuwiki/wp-ups.tar.gz) contains most of our material
related to Frama-C/WP (in French, still evolving each year). The
training exercises are embedded in slides, the ones for the final
practical session are directly provided in .c files.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment