Allan Blanchard

Publication Activity (10 Years)

Years Active: 2015-2024
Publications (10 Years): 13

Top Topics

Formal Verification

Hardware Designs

Concurrent Programs

Axiomatic Characterization

Top Venues

Publications

Loïc Correnson, Allan Blanchard, Adel Djoudi, Nikolai Kosmatov
Automate where Automation Fails: Proof Strategies for Frama-C/WP. TACAS (1) (2024)
Parisis Gallos, Rance 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
MedSecurance Project: Advanced Security-for-Safety Assurance for Medical Device IoT (IoMT). MIE (2023)
Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov
Towards Full Proof Automation in Frama-C Using Auto-active Verification. NFM (2019)
Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
Logic against ghosts: comparison of two proof approaches for a list module. SAC (2019)
Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C. NFM (2018)
Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
MMFilter : A CHR-Based Solver for Generation of Executions under Weak Memory Models. Comput. Lang. Syst. Struct. 53 (2018)
Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
Tutorial: Secure Your Things: Secure Development of IoT Software with Frama-C. SecDev (2018)
Frédéric Loulergue, Allan Blanchard, Nikolai Kosmatov
Ghosts for Lists: From Axiomatic to Executable Specifications. TAP@STAF (2018)
Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
A Lesson on Verification of IoT Software with Frama-C. HPCS (2018)
Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov
From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation. VPT@ETAPS (2017)
Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
A CHR-Based Solver for Weak Memory Behaviors. CSTVA@ISSTA (2016)
Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, Frédéric Loulergue
Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of C Programs. SCAM (2016)
Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, Frédéric Loulergue
A Case Study on Formal Verification of the Anaxagoros Hypervisor Paging System with Frama-C. FMICS (2015)