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.

PDF Version

Details of teaching

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.

Object-oriented programming basic

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.

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).

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.

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, ...).

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.

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.

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.

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.

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.