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