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