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

New teaching page

parent c32b726f
No related branches found
No related tags found
1 merge request!49New tutorials and teaching pages
Showing
with 110 additions and 13 deletions
......@@ -52,6 +52,7 @@ plugin: <plug-in identifier>
authors: "<the authors>" <-- optional
title: "<Title of the publication>
book: "<Name of the conference/journal>" <-- optional
place: "<University/School where the teaching takes place>" <-- optional ("teaching" category)
link: URL to access to the publication <-- optional
year: year of publication
category: "<kind of publication>"
......@@ -66,6 +67,7 @@ In the "General" directory, the category can be:
- foundational
- kernel
- tutorials
- teaching
In other directories, it can be:
......@@ -74,6 +76,23 @@ In other directories, it can be:
- foundational
- tutorials
- other
- teaching
Note that if you think you need a new category, it can be added, but the file
`html/publications.html` should be updated accordingly.
Notes:
- if you think you need a new category, it can be added, but the file `html/publications.html`
should be updated accordingly,
- publications in the `teaching` category only appear on the "Teaching" page.
# I want to associate my publication to a HTML content or to store some files
If your publication includes some content that should be stored on the server,
add a directory named according to the name of your file in the `download`
directory. For example for: `_fc-publications/eva/2019-vmcai-bby.md`, we
should create a directory `download/publications/2019-vmcai-bby`.
If you want to generate specific HTML pages for your publication (for example
online exercices for a publication in the `teaching` category), proceed as
above, but in the `html` directory instead of `download`. See for example
the directory: `html/publications/2010-ensiie-vslg` and its corresponding
publication file `_fc-publications/general/2010-ensiie-vslg`.
\ No newline at end of file
---
plugin: general
authors: "José N. Oliveira, Luís S. Barbosa, José B. Barros, Alcino Cunha, Maria João Frade and Jorge Sousa Pinto"
title: "Formal Methods in Software Engineering"
place: "University of Minho"
link: https://mei.di.uminho.pt/?q=en/1112/mfes-uk
year: 2007-2012
category: teaching
---
---
plugin: general
authors: Virgile Prevosto, Julien Signoles and Tristan Le Gall
title: "Static Analysis Course"
place: "ENSIIE Evry"
year: 2010-2018
category: teaching
short: In French.
---
Below is the list of exercices done with Frama-C during the Static
Analysis Course at ENSIIE:
* [2010-2011](/html/publications/2010-ensiie-vslg/ensiie2010-2011-ias-tp.html)
* [2011-2012](/html/publications/2010-ensiie-vslg/ensiie2011-2012-ias-tp.html)
* [2012-2013](/html/publications/2010-ensiie-vslg/ensiie2012-2013-ias-tp.html)
* [2013-2014](/html/publications/2010-ensiie-vslg/ensiie2013-2014-ias-tp.html)
* [2014-2015](/html/publications/2010-ensiie-vslg/ensiie2014-2015-ias-tp.html)
* [2015-2016](/html/publications/2010-ensiie-vslg/ensiie2015-2016-ias-tp.html)
* [2016-2017](/html/publications/2010-ensiie-vslg/ensiie2016-2017-ias-tp.html)
* [2017-2018](/html/publications/2010-ensiie-vslg/ensiie2017-2018-ias-tp.html)
---
plugin: general
authors: Eugene Kornykhin
title: "Formal Specification and Verification"
place: "Moscow State University"
year: 2012-2013
link: https://sed.ispras.ru/fmprac
category: teaching
short: In Russian.
---
......@@ -3,9 +3,9 @@ plugin: "general"
authors: "David Mentré"
title: "Practical introduction to Frama-C"
book: "Mitsubishi Electric R&D Centre Europe"
link: "/download/tutorials/2013-merce-m/introduction-to-frama-c_v2.pdf"
link: "/download/publications/2013-merce-m/introduction-to-frama-c_v2.pdf"
year: 2013
category: tutorials
---
[Examples](/download/tutorials/2013-merce-m/introduction-slides-examples.tar.gz)
\ No newline at end of file
[Examples](/download/publications/2013-merce-m/introduction-slides-examples.tar.gz)
\ No newline at end of file
......@@ -7,6 +7,6 @@ year: 2013
category: tutorials
---
- Frama-C Overview: [Slides](/download/tutorials/2013-stance-p/frama_c_overview.pdf), [Simple plugin](/download/tutorials/2013-stance-p/simple_metrics.ml)
- Value Analysis: [Slides](/download/tutorials/2013-stance-p/value_tutorial.pdf) and [Examples](/download/tutorials/2013-stance-p/value_examples.tar.gz)
- WP: [Slides](/download/tutorials/2013-stance-p/wp_advanced_slides.pdf) and [Examples](/download/tutorials/2013-stance-p/wp_examples.tar.gz)
\ No newline at end of file
- Frama-C Overview: [Slides](/download/publications/2013-stance-p/frama_c_overview.pdf), [Simple plugin](/download/publications/2013-stance-p/simple_metrics.ml)
- Value Analysis: [Slides](/download/publications/2013-stance-p/value_tutorial.pdf) and [Examples](/download/publications/2013-stance-p/value_examples.tar.gz)
- WP: [Slides](/download/publications/2013-stance-p/wp_advanced_slides.pdf) and [Examples](/download/publications/2013-stance-p/wp_examples.tar.gz)
\ No newline at end of file
---
plugin: general
authors: "Guillaume Petiot, Alain Giorgetti, Jacques Julliand"
title: "Course on Frama-C"
place: "Université de Franche-Comté"
link: "/download/publications/2013-ufc-pgj/tp1.pdf"
year: 2013-2014
category: teaching
short: In French.
---
---
plugin: general
authors: "Martin Peres and Steve D. Lazaro"
title: "Language-based security"
place: "University College London"
link: http://www.mupuf.org/blog/2014/02/10/a_return_into_the_world_of_frama-c
year: 2014
category: teaching
---
\ No newline at end of file
......@@ -3,7 +3,7 @@ plugin: "wp"
authors: "Virgile Prevosto, Nikolay Kosmatov and Julien Signoles"
title: "Specification and Proof of Programs with Frama-C"
book: "Integrated Formal Methods (iFM)"
link: "/download/tutorials/2013-ifm-pks/slides.pdf"
link: "/download/publications/2013-ifm-pks/slides.pdf"
year: 2013
category: tutorials
short: "A tutorial about the Frama-C plug-in WP."
......@@ -11,4 +11,4 @@ short: "A tutorial about the Frama-C plug-in WP."
Despite the spectacular progress made by the developers of formal verification tools, their usage remains basically reserved for the most critical software. More and more engineers and researchers today are interested in such tools in order to integrate them into their everyday work. This half-day tutorial proposes a practical introduction during which the participants will write C program specifications, observe the proof results, analyze proof failures and fix them. Participants will be taught how to write a specification for a C program, in the form of function contracts, and easily prove it with an automatic tool in Frama-C, a freely available software verification toolset. Those who will have Frama-C installed (e.g. from ready-to-install packages frama-c, why, alt-ergo under Linux) will also run automatic proof of programs on their computer. Program specifications will be written in the specification language ACSL similar to other specification languages like JML that some participants may know. ACSL-syntax is intentionally close to C and can be easily learned on-the-fly.
[Annotated files](/download/tutorials/2013-ifm-pks/frama_c_tutorial_examples.tar.gz)
\ No newline at end of file
[Annotated files](/download/publications/2013-ifm-pks/frama_c_tutorial_examples.tar.gz)
\ No newline at end of file
......@@ -3,7 +3,7 @@ plugin: "wp"
authors: "Virgile Prevosto"
title: "Frama-C WP tutorial"
book: "Laboratoire d'Informatique Fondamentale d'Orléans"
link: "/download/tutorials/2014-lifo-p/slides.pdf"
link: "/download/publications/2014-lifo-p/slides.pdf"
year: 2014
category: tutorials
short: "A tutorial about the Frama-C plug-in WP."
......@@ -11,4 +11,4 @@ short: "A tutorial about the Frama-C plug-in WP."
[LIFO's website](https://www.univ-orleans.fr/lifo/)
[Annotated files](/download/tutorials/2014-lifo-p/solutions.tar.gz)
\ No newline at end of file
[Annotated files](/download/publications/2014-lifo-p/solutions.tar.gz)
\ No newline at end of file
---
plugin: wp
authors: Andrei Paskevich and Julien Signoles
title: "Course on Deductive Verification"
place: "University Paris Saclay"
year: 2015
category: teaching
short: In French.
---
Course on Deductive Verification in [Master MPRI](https://www.universite-paris-saclay.fr/formation/master/informatique/m1-master-parisien-de-recherche-en-informatique-mpri#programme) (1st year) at [University Paris-Saclay](https://www.universite-paris-saclay.fr/en) (France), given by [Andrei Paskevich](http://tertium.org/) (Why3) and [Julien Signoles](http://julien.signoles.free.fr/index.en.html) (Frama-C), since 2015.
Our exercises use both Frama-C/WP and [Why3](http://why3.lri.fr/) ([in a browser](http://why3.lri.fr/try/)). [A tarball](/download/publications/2015-ups-ps/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.
\ No newline at end of file
{% assign publis = site.fc-publications | where:"plugin",include.plugin | where:"category",include.category %}
{% if include.plugin %}
{% assign publis = site.fc-publications | where:"plugin",include.plugin | where:"category",include.category %}
{% else %}
{% assign publis = site.fc-publications | where:"category",include.category %}
{% endif %}
{% if 0 != publis.size %}
{% if include.title %}<h4> {{ include.title }} </h4>{% endif %}
......@@ -9,8 +13,9 @@
{% assign content = pub.content | strip_newlines %}
<summary {% if content == "" %} class="empty" {% endif %}>
{% if pub.authors %}<div>{{ pub.authors }}</div>{% endif %}
<div><b>{{ pub.title }}</b>{% if pub.link %} [<a href="{{ pub.link }}">PDF</a>] {% endif %}</div>
<div><b>{{ pub.title }}</b>{% if pub.link %} [<a href="{{ pub.link }}">link</a>] {% endif %}</div>
{% if pub.book %} <div>In {{ pub.book }}, {{ pub.year }}</div> {% endif %}
{% if pub.place %} <div>In {{ pub.place }}, {{ pub.year }}</div> {% endif %}
{% if pub.short %}<div><em>{{ pub.short }}</em></div>{% endif %}
</summary>
{% if content != "" %}
......
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