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