Frédéric Loulergue

Latest

Logic against ghosts: comparison of two proof approaches for a list module
Parallel programming with Coq: map and reduce skeletons on trees
Towards Full Proof Automation in Frama-C Using Auto-active Verification
A Cloud Brokerage Solution: Formal Methods Meet Security in Cloud Federations
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
Interactive Bulk Synchronous Parallel Functional Programming in a Browser
MMFilter : A CHR-Based Solver for Generation of Executions under Weak Memory Models
Parallel Programming with OCaml: A Tutorial
Strong Security Guarantees: From Alloy to Coq (Research Poster)
Towards the Generation of Correct Java Programs (Research Poster)
Tutorial: Secure Your Things: Secure Development of IoT Software with Frama-C
Verified Programs for Frequent Itemset Mining
A BSPlib-style API for Bulk Synchronous Parallel ML
A Java Framework for High Level Parallel Programming Using Powerlists
A Verified Accumulate Algorithmic Skeleton
Automated Generation of BSP Automata
Calculating Parallel Programs in Coq Using List Homomorphisms
Formalization of a Big Graph API in Coq
From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation
Imperative BSPlib-style Communications in BSML
Implementing Algorithmic Skeletons with Bulk Synchronous Parallel ML
Introduction to the Special Issue on Practical Aspects of High-Level Parallel Programming
Replicated Synchronization for Imperative BSP Programs
Towards a Verified Parallel Implementation of Frequent Itemset Mining
A CHR-Based Solver for Weak Memory Behaviors
Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of C Programs