VerifiableC[1] provides Hoare rules for (a large subset[2] of) C that include function calls, pointers and heap allocation, and some amount of concurrency. It

VerifiableC[1] provides Hoare rules for (a large subset[2] of) C that include function calls, pointers and heap allocation, and some amount of concurrency. It does use an extension to Hoare logic, called separation logic, to achieve some of these features. In particular, separation logic's frame rule is instrumental for the modularization needed for semantics of function calls. [1]https://vst.cs.princeton.edu/veric/ https://vst.cs.princeton.edu/veric/ [2]excludes setjmp/longjmp, unstructured switch statements, goto and maybe a few other moderately exotic constructions.