The Cameroon Computer Society is holding a two-session online workshop on the use of formal methods to improve the safety and security of computer systems. It is presented by Dr Allan Blanchard of CEA-LIST, in Paris and Saclay, one of the authors of the Frama-C platform the workshop teaches. This is the first of the two sessions. It is free, and places are limited.

Formal methods are mathematical techniques for establishing what a program does and does not do. Session one introduces the ideas and the tool; session two puts them to work on code.

The presenter

Dr Allan Blanchard is a researcher and deputy head of the Software Reliability and Security Laboratory at CEA-LIST, a French public research institute working on smart digital systems. He is named among the authors of Frama-C, which is co-developed at CEA-LIST and at Inria Saclay, and he works mainly on WP, its deductive verification plug-in. His research is on the analysis of concurrent code by proof, and he has given Frama-C tutorials at conferences in Portugal, Cyprus, Serbia and France.

What this session covers

The session opens on what matters in software quality: what a perfect analysis tool would do, and why no such tool can exist. Accept different constraints and you get different techniques, each with its own trade-offs. The rest of the workshop builds on that.

It then turns to Frama-C, an open-source platform for the analysis of C source code, and to three of its plug-ins:

• Eva computes variation domains for a program’s variables, by abstract interpretation, and is used to establish the absence of runtime errors.
• WP proves ACSL contracts, checking that a program conforms to its specification.
• E-ACSL checks annotations while the program runs, rather than before it runs.

The session ends on what guarantee each technique gives, and on how the plug-ins combine to analyse systems and properties none of them settles alone.

Who it is for

Master’s students, and others working in mathematics, logic or software verification. Frama-C analyses C, so some reading knowledge of C is useful. The workshop is designed for a classroom of 20 to 25.

Practical details

Tuesday 13 October 2026, 13:00 to 17:30 WAT. Four hours of teaching, with a 30-minute break. Online.

How to register

A lecturer who would like to put a group of students forward can write to contact@camcompsoc.org with the subject “Formal Methods Workshop – October”, listing the students and their email addresses.

Session two

Session two follows on Tuesday 20 October, at the same time. It has its own registration, on its page.