No Smoke without Fire: Detecting Specification Inconsistencies with Frama-C/WP

[ 2024 ] Conference || Allan Blanchard, Loïc Correnson, Adel Djoudi, Nikolai Kosmatov

Formally Expressing What a Program Should Do: The ACSL Language

[ 2024 ] Chapter || Allan Blanchard, Claude Marché, Virgile Prevosto

Formally Verifying that a Program Does What It Should: The Wp Plug-in

[ 2024 ] Chapter || Allan Blanchard, François Bobot, Patrick Baudin, Loïc Correnson

Automate where Automation Fails: Proof Strategies for Frama-C/WP

[ 2024 ] Conference || Loïc Correnson, Allan Blanchard, Adel Djoudi, Nikolai Kosmatov

Towards Full Proof Automation in Frama-C using Auto-Active Verification

[ 2019 ] Conference || Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov

Logic against Ghosts: Comparison of Two Proof Approaches for a List Module

[ 2019 ] Conference Best Paper Award || Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue

MMFilter: A CHR-Based Solver for Generation of Executions under Weak Memory Models

[ 2018 ] Journal || Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue

A Lesson on Verification of IoT Software with Frama-C

[ 2018 ] Tutorial || Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue

Ghosts for Lists: from Axiomatic to Executable Specifications

[ 2018 ] Conference || Frédéric Loulergue, Allan Blanchard, Nikolai Kosmatov

Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C

[ 2018 ] Conference || Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue

Aide à la vérification de programmes concurrents par transformation de code et de spécifications

[ 2017 ] Thesis || Allan Blanchard

Concurrent Program Verification by Code Transformation: Correctness

[ 2017 ] Report || Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov

From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation

[ 2017 ] Workshop || Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov

Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of C Programs

[ 2016 ] Conference || Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, Frédéric Loulergue

A CHR-Based Solver for Weak Memory Behaviors

[ 2016 ] Workshop || Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue

A Case Study on Formal Verification of the Anaxagoros Hypervisor Paging System with Frama-C

[ 2015 ] Workshop || Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, Frédéric Loulergue