Welcome!

KindSpec is an automated tool 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 semantic K framework, we enrich the symbolic execution facilities recently provided by K with novel capabilities for assertion synthesis that are based on abstract subsumption. Roughly speaking, KindSpec generates a method contract for a (modifier) C function by using other (observer) routines in the same program. The synthesized contract essentially consists of logical axioms that express pre- and post-condition assertions that define the precise input/output behavior of the C routine.

Because of the abstraction, some inferred axioms cannot be guaranteed to be correct and are kept apart as candidate (or overly general) axioms. A refinement post-processing can be performed that removes every candidate axiom for which an instance is refuted and then filters out any redundant elements from the surviving axioms.