Software prototype for the automated inference of program specifications as logical axioms.

  • KindSpec: paper that describes a tool that derives axiom-like specifications from C code.

Other related works:

  • Capturing constrained constructor patterns in matching logic, Xiaohong Chen, Dorel Lucanu, Grigore Roşu, JLAMP