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

Blog

Back

Tag Archives: formal

On Dedicated Specification Languages Beyond ACSL contracts
Virgile Prevosto on 13 June 2025

La critique du langage ne peut éluder ce fait que nos paroles nous engagent et que nous devons leur être fidèles. — Albert Camus This post was originally written for the SecOPERA project’s blog. A crucial, but often neglected aspect of formal software evaluation process, is how we specify the...

Read More

Tags

formal 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 spec, ACSL, MetAcsl, RPP, Aoraï, Typestates
Copyright © 2007-2025 Frama-C. All Rights Reserved.
  • Terms Of Use
  • Authors
  • Acknowledgements