KindSpec

Symbolic abstract contract synthesis in a rewriting framework. We propose an automated technique for inferring software contracts from programs that are written in a non-trivial fragment of C, called KernelC, that supports pointer-based structures and heap manipulation. Starting from the semantic definition of KernelC in the $mathbb {K}$ framework, we enrich the symbolic execution facilities recently provided by C with novel capabilities for assertion synthesis that are based on abstract subsumption. Roughly speaking, we define an abstract symbolic technique that explains the execution of a (modifier) C function by using other (observer) routines in the same program. We implemented our technique in the automated tool KindSpec 2.0, which generates logical axioms that define the precise input/output behavior of the C routines.