Frama-C+WP Tutorial

Frama-C (FRAmework for Modular Analysis of C programs) is a set of interoperable program analyzers for C programs. I have used this software during all my PhD thesis, mostly for deductive proof using the WP plugin. So, I wrote a tutorial that allows to learn ACSL (the specification language of Frama-C) and the use of WP by practice, also getting some theorical rudiments about deductive proof.

Link to PDF version (EN)

Frama-C (FRAmework for Modular Analysis of C programs) est un ensemble d'analyseurs pour les programmes C. J'ai utilisé Frama-C pendant toute ma thèse, en particulier le greffon de preuve déductive WP. J'ai donc écrit un tutoriel qui a pour but d'apprendre ACSL (le langage de spécification de Frama-C) et l'utilisation de WP par la pratique, tout en ayant la possibilité d'acquérir quelques rudiments théoriques à propos de la preuve.

Lien vers la version PDF (FR)

Version en ligne sur Zeste De Savoir (FR)


Person

Existence Proof

Person

xkcd.com

Summary/Récapitulatif

2016-2017 Algorithmic basics 1st year technology degree IUT Orléans 16h
2016-2017 Object-oriented programming basics 1st year technology degree IUT Orléans 28h
2016-2017 Object-oriented design - basics 1st year technology degree IUT Orléans 45h
2016-2017 Object-oriented design - advanced notions 2nd year technology degree IUT Orléans 40h
2016-2017 Graphs and Languages 1st year technology degree IUT Orléans 32h
2016-2017 Parallelism and Concurrency 2nd year technology degree IUT Orléans 24h
2015-2016 Program test and proof 4th year of engineering school ENSIIE 10h
2015-2016 Proof of Programs with Frama-C 5th year of engineering school UPMC - Polytech 4h
2015-2016 First order logic and Logic Programming 3rd year of engineering school UVSQ - ISTY 26h
2014-2015 Proof of Programs with Frama-C 5th year of engineering school UPMC - Polytech 4h
2014-2015 C programming 3rd year of engineering school UVSQ - ISTY 16h
Total : 245h

Details/Détails

Algorithmic basics

This module is built as tutorial and progressively brings students to object oriented programming. The key idea is the notion of API as a way to abstract from data representation.

Ce module, construit sous la forme d'un tutoriel, a pour but d'amener progressivement les étudiants vers la programmation orientée objet en leur faisant d'abord assimiler la notion d'interface de programmation et le besoin de s'abstraire de la représentation des données sous jacentes.

Object-oriented programming basics

This module completes the basics notions acquired during the module "Algorithmic basics" with more advanced notions. Exceptions, encapsulation and variation of behavior using inheritance are addressed. We use the Java language.

Cette série de TP complète les bases acquises pendant le module de programmation "Programmation - vers l'objet" avec des notions plus poussées. Les notions d'exceptions, d'encapsulation et de variation de comportement par héritage y sont notamment abordées. Le langage utilisé est Java.

Object-oriented design - basics

The goal of this module is to acquire basic notions about object-oriented designed using the UML, with an emphase on use case diagrams, sequence diagrams and class diagrams (we also skim through object and collaboration diagrams).

Le but de cours est d'acquérir les notions de bases en conception orientée objet par l'intermédiaire du langage UML, avec un centrage sur les diagrammes de cas d'utilisation, de séquence et de classe (les diagrammes d'objet et de collaboration sont simplement mentionnés).

Object-oriented design - advanced notions

The goal of this module is to complete the basics acquired in the module "Object-oriented design - basics". Design notions are manipulated through UML and the code generation tool Umbrello. Some design-patterns are studied.

Le but de cours est de compléter les bases acquises précédemment en objet dans le module "Object-oriented design - basics". Les éléments de conception sont manipulés à travers le formalisme UML et mis en pratique avec l'outil de génération et de rétro-ingénierie Umbrello. Plusieurs patrons de conception sont notamment étudiés.

Graphs and Languages

This module comprises two aspects of fondamental computer science : automatons and graph algorithms. In the "language" part, we talk about regular languages and operations on automatons (intersection, union, ...). In the "graph" part, different search algorithms are taught as well as simple properties about graphs (connectivity, cycles, shortest pathes, ...).

Ce module comprend deux aspects de l'informatique fondamentale : les automates de mots et les algorithmes de graphes. Dans la partie langage, on s'intéresse à traiter les langages réguliers et les opérations sur les automates correspondant. Dans la partie graphe, les différents types de parcours sont abordés ainsi que les propriétés simples dans les graphes (connexité, cycles, plus courts chemins, ...).

Parallelism and Concurrency

This module presents different aspects of distributed programming, using shared and distributed memory. It includes monitors, semaphores, mutexes, synchronization using barriers and remote execution (RMI). We use the Java language.

Le but de ce module est de voir différent aspects de la programmation répartie, en mémoire partagée ou distribuée. Notamment la notion de moniteur, de sémaphores et mutexes, de synchronisation à base de barrières et d'exécution à distance (RMI). Le langage utilisé est Java.

Program Test and Proof

In these lectures, different validation technics are presented, including test and proof. For the "test" part, some code coverage criterion are studied, as well as symbolic execution. The "proof" part is about weakest precondition calculs. These notions are practiced using Java JUnit and Pathcrawler for test, and Frama-C and WP for proof.

L'objectif de ce cours est de présenter des techniques de validation du logiciel, dans le domaine du test et de la preuve. Pour le test, cela comprend divers critères de couverture de code et leur évaluation, ainsi que des notions d'exécution symbolique. La partie preuve concerne le calcul de plus faible pré-condition. Ces notions sont mises en pratique par l' usage de Java JUnit et Pathcrawler pour le test et de Frama-C avec WP pour la preuve.

Proof of programs with Frama-C

The goal of these lectures is to practice program proof using Frama-C and WP. A serie of programs is given to student with an increasing difficulty. The idea is to make them understand the benefits that we can get with program proof.

Cette série de TP a pour objectif de mettre en pratique des notions en preuve de programme à travers les outils Frama-C et WP. Le but est de spécifier et prouver un ensemble de petits programmes C avec une difficulté croissante pour comprendre les apports de la preuve pour la validation de programmes.

First order logic and Logic Programming

Introduction to first order logic (propositions, connectives, quantifiers). We illustrate this logic using Prolog which allows to compute results from definitions expressed using logic.

Cours d'introduction à la logique des prédicats du premier ordre (proposition, connecteurs, quantificateurs). On illustre le fonctionnement de cette logique par l'usage du langage Prolog qui permet de calculer à partir de définitions exprimées sous forme logique.

C Programming

20h project in C language, the goal of this module is to teach basics notions in C that are needed to follow the different modules that are then proposed to student. It includes algorithmic basics and its translation to C language and the correct use of the language features.

Encadrement d'un projet de C sur 20h qui a pour objectif d'inculquer rapidement toutes les notions basiques du langage C nécessaires aux étudiants pour pouvoir suivre les modules qui leurs sont proposés le reste de l'année. Cela inclut l'algorithmique et sa traduction vers le C ainsi que l'usage correct des fonctionnalités du langage.