Dr Allan Blanchard of CEA-LIST, one of the authors of the Frama-C platform, presents two free online sessions on software safety and security, on 13 and 20 October 2026.
The Cameroon Computer Society (CmrCS) is holding a workshop on the use of formal methods to improve the safety and security of computer systems. It runs over two afternoons, Tuesday 13 and Tuesday 20 October 2026, four hours of teaching in each, and is presented by Dr Allan Blanchard, researcher and deputy head of the Software Reliability and Security Laboratory at CEA-LIST, in Paris and Saclay.
Formal methods are mathematical techniques for establishing what a program does and does not do. Instead of running a program on a set of inputs and watching what happens, they reason about every execution the program admits. Testing shows that a fault is present; these techniques show that a whole class of fault is absent.
The presenter
CEA-LIST is a French public research institute working on smart digital systems. Dr Blanchard is named among the authors of Frama-C, the platform the workshop teaches, which is co-developed at CEA-LIST and at Inria Saclay. He works mainly on WP, its deductive verification plug-in. He is, in other words, teaching a tool he helps write.
His research is on the analysis of concurrent code by proof. Before CEA-LIST he was a post-doctoral researcher at Inria Nord Europe on the EU H2020 VESSEDIA project, which set out to make formal methods easier to apply to internet-of-things software; that work used Eva and WP to establish the absence of runtime errors in Contiki, a lightweight operating system for IoT devices. He has given Frama-C tutorials at conferences in Portugal, Cyprus, Serbia and France.
Why this matters here
Most engineers and students in Cameroon meet verification as a lecture topic and never see a tool run over real code, and fewer still are taught by one of the people who builds it. Certification regimes in avionics, nuclear instrumentation and security evaluation are built on these techniques. They are also what turns “we tested it and found nothing” into a claim with a stated scope.
CmrCS carries this work through its Cybersecurity Workgroup and its AI Taskforce. Software written and maintained in Cameroon stands to gain: a classroom of twenty-five people who have run an analyser over C code is a different starting point from a classroom that has only read about one.
What the workshop covers
The workshop 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 material builds on that.
It then turns to Frama-C, which its developers describe as “an open-source extensible and collaborative platform dedicated to source-code analysis of C software”. It is used in teaching, research and industry, including for certification under standards such as DO-178, IEC 60880 and Common Criteria EAL 6 and 7. Its analyses come as plug-ins, and the workshop covers three of them.
The three Frama-C plug-ins
Eva computes variation domains for a program’s variables. It works by abstract interpretation, reasoning over sets of possible values rather than single ones, and is used to establish the absence of runtime errors.
WP proves contracts written in ACSL, the specification language Frama-C uses. Eva asks whether a program can go wrong; WP asks whether it does what its specification says. This is the plug-in Dr Blanchard works on.
E-ACSL checks annotations while the program runs, rather than proving them beforehand. That reaches code and conditions static analysis leaves open.
The last part of the workshop covers what guarantee each technique gives, and how the plug-ins combine on systems and properties none of them settles alone.
Who should attend
The workshop is aimed at master’s students, and at researchers and practitioners working in mathematics, logic or software verification. Frama-C analyses C, so some reading knowledge of C is useful. It is designed for a classroom of 20 to 25, and places are limited.
The first session introduces the concepts; the second is the practical half. The two sessions make one workshop, and each has its own registration.
What you can do
Register for each session on its own page. Registration is free, and joining details are sent by email to registered participants.
- Session one, Tuesday 13 October 2026, 13:00 to 17:30 WAT
- Session two, Tuesday 20 October 2026, 13:00 to 17:30 WAT
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.
