Frama-C
  • Features
  • Documentation
  • Publications
  • Blog
  • Jobs
  • Contact
  • Download

Blog

Back

Tag Archives: abstract-debugging

The Eva Abstract Debugger: A new way to explore and interact with the Frama-C/Eva static analyzer
Jules Massart on 2 February 2026

This is an invited post by Jules Massart on his 6-month internship (from March to August 2025) in the Frama-C team, where he developed the Eva Abstract Debugger under the supervision of Michele Alberti, David Bühler, and Virgile Prevosto. Building on the original idea of Abstract Debuggers [1], Jules shows...

Read More

Tags

abstract-debugging skein value ACSL Jessie derived-analysis unspecified-behavior CIL OCaml floating-point rant memcpy value-builtins conversions-and-promotions icpc2011 csmith position donut facetious-colleagues slicing CompCert big-round-numbers trail nitrogen link benchmarks rte obviously-terminates cybersecurity linking type-checking developer visitor restrict undefined-behavior rers2012 cfg WP c11 c99 anonymous-arrays zlib metrics collaboration FLT_EVAL_METHOD function-pointers c-reduce Eva gui tutorial open-source-case-studies scripts usability windows-cygwin-wsl docker github ci test Ivette GUI event machdep parsing formal-spec MetAcsl RPP Aoraï Typestates
Copyright © 2007-2026 Frama-C. All Rights Reserved.
  • Terms Of Use
  • Authors
  • Acknowledgements