Deliverable 6

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
• An Active Learning Approach to Synthesizing Program Contracts, Sandip Ghosal, Bengt Jonsson, Philipp Rümmer, SEFM’23, LNCS
• Contract Strengthening through Constrained Horn Clause Verification, Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, HCVS/VPT’22