01
Frama-C and ACSL: Deductive Verification for C at Scale
Frama-C brought multiple static-analysis and deductive-verification techniques into one extensible platform for industrial C, with ACSL contracts serving as a shared language for expressing what code should guarantee.
↗