Keyword: imperative program

• HoareTut: A Tutorial on Reflecting in Coq the generation of Hoare proof obligations
  Sylvain Boulmé