C and C++

From Openproofs

Proving programs written in C and C++ can be challenging. Neither language strongly enforces types, both rely heavily on pointers (which are challenging for most proof systems to handle), and both rely on manual memory management (which is also challenging to handle for most proof systems).

Caduceus was developed to handle C. More recently, the Jessie plug-in to the Frama-C framework has been developed as a follow-on to Caduceus.