Search

SSERL

Allan Blanchard

Logic against ghosts: comparison of two proof approaches for a list module
Towards Full Proof Automation in Frama-C Using Auto-active Verification
A Lesson on Verification of IoT Software with Frama-C
Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C
Ghosts for Lists: From Axiomatic to Executable Specifications
MMFilter : A CHR-Based Solver for Generation of Executions under Weak Memory Models
Tutorial: Secure Your Things: Secure Development of IoT Software with Frama-C
From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation
A CHR-Based Solver for Weak Memory Behaviors
Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of C Programs