Symbolic Abstract Contract Synthesis in a Rewriting Framework

TL;DR

This paper introduces an automated method for inferring software contracts from complex C programs using symbolic execution and abstract subsumption within the K framework, implemented in the KindSpec 2.0 tool.

Contribution

It presents a novel symbolic assertion synthesis technique for KernelC programs, enhancing automatic contract inference with abstract subsumption capabilities.

Findings

Successfully infers pre- and post-conditions for KernelC functions

Integrates assertion synthesis with symbolic execution in the K framework

Implemented in the KindSpec 2.0 tool for practical use

Abstract

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 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, 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 express pre- and post-condition assertions by defining the precise input/output behaviour of the C routines.