Allan Blanchard

15 papers C 3Misc 1Journal 1Unranked 9
YearRankTypeTitle / Venue / Authors
2024 — conf
Automate where Automation Fails: Proof Strategies for Frama-C/WP.
TACAS (1)
Loïc Correnson, Allan Blanchard, Adel Djoudi, Nikolai Kosmatov
2024 C conf
No Smoke Without Fire: Detecting Specification Inconsistencies with Frama-C/WP.
TAP
Allan Blanchard, Loïc Correnson, Adel Djoudi, Nikolai Kosmatov
2023 — conf
MedSecurance Project: Advanced Security-for-Safety Assurance for Medical Device IoT (IoMT).
MIE
Parisis Gallos, Rance J. DeLong, Nicholas Matragkas, Allan Blanchard, Chokri Mraidha, Gregory Epiphaniou, Carsten Maple, Konstantinos Katzis, Jaime Delgado, Silvia Llorente, Pedro Maló, Andreas Menychtas, Christos Panagopoulos, Ilias Maglogiannis, Petros Papachristou, Mariana Soares, Paula Breia, Ana Cristina Vidal, Martin Ratz, Ross Williamson, Eduard Erwee, Lukasz Stasiak, Orfeu Flores, Carla Clemente, John Mantas, Patrick Weber, Theodoros N. Arvanitis, Scott Hansen
2019 Misc conf
Logic against ghosts: comparison of two proof approaches for a list module.
SAC
Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
2019 — conf
Towards Full Proof Automation in Frama-C Using Auto-active Verification.
NFM
Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov
2018 — conf
A Lesson on Verification of IoT Software with Frama-C.
HPCS
Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
2018 — conf
Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C.
NFM
Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
2018 — conf
Ghosts for Lists: From Axiomatic to Executable Specifications.
TAP@STAF
Frédéric Loulergue, Allan Blanchard, Nikolai Kosmatov
2018 J jnl
MMFilter : A CHR-Based Solver for Generation of Executions under Weak Memory Models.
Comput. Lang. Syst. Struct.
Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
2018 — conf
Tutorial: Secure Your Things: Secure Development of IoT Software with Frama-C.
SecDev
Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
2017 — conf
From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation.
VPT@ETAPS
Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov
2016 — conf
A CHR-Based Solver for Weak Memory Behaviors.
CSTVA@ISSTA
Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
2016 — —
Assisted Concurrent Program Verification by Code and Specification Transformation. (Aide à la vérification de programmes concurrents par transformation de code et de spécifications).
Allan Blanchard
2016 C conf
Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of C Programs.
SCAM
Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, Frédéric Loulergue
2015 C conf
A Case Study on Formal Verification of the Anaxagoros Hypervisor Paging System with Frama-C.
FMICS
Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, Frédéric Loulergue