Weakest precondition generator

With Anne Pacalet.

A pre-condition algorithm on C with correctness proof in Coq. For the Frama-C project.

Documents