Automated Synthesis of Software Contracts with KindSpec.

In this paper, we describe KindSpec, an automated tool that synthesizes software contracts from programs that are written in a significant fragment of C that supports pointer-based structures, heap manipulation, and recursion. By relying on a semantic definition of the C language in the $$\mathbb {K}$$ semantic framework, KindSpec leverages the symbolic execution capabilities of $$\mathbb {K}$$ to axiomatically explain any program function. This is done by using observer routines in the same program to characterize the program states before and after the function execution. The generated contracts are expressed in the form of logical axioms that specify the precise input/output behavior of the C routines, including both general axioms for default behavior and exceptional axioms for the specification error behavior. We summarize the main services provided by KindSpec, which also include a novel refinement facility that improves the quality and accuracy of the synthesized contracts. Finally, we provide an experimental evaluation that assesses its effectiveness.