Research articles and conferences

Software verification

• Software: Frama-C plugins
  • Frama-C-StaDy: Static & Dynamic verification of C programs
  • Frama-C-Mutation: Generation of mutant programs
  • Frama-C-Inline: Inlining of ACSL predicates and logic functions
• How Testing Helps to Diagnose Proof Failures.
  • Author preview
  • Proceedings
  • Benchmarking suite for Frama-C-StaDy
• Static and Dynamic Verification of Relational Properties on Self-Composed C Code.
  • Author preview
  • Proceedings
• Your Proof Fails? Testing Helps to Find the Reason.
  • Best Paper Award
  • Author preview
  • Proceedings
• PhD Thesis: Contribution à la vérification de programmes C par combinaison de tests et de preuves.
  • Final
  • Archived
• Sequential Generation of Structured Arrays and Its Deductive Verification.
  • Author preview
  • Proceedings
• Instrumentation of Annotated C Programs for Test Generation.
  • Author preview
  • Proceedings
• How Test Generation Helps Software Specification and Deductive Verification in Frama-C.
  • Author preview
  • Proceedings
• An Optimized Memory Monitoring for Runtime Assertion Checking of C Programs.
  • Author preview
  • Proceedings

Fault Injection Simulation

• FISSC: a Fault Injection and Simulation Secure Collection.
  • Author preview
  • Proceedings

Parallel Programming with OCaml (BSML)

• Functional Parallel Programming with Revised Bulk Synchronous Parallel ML.
  • Author preview
  • Proceedings