Symbolic Abstract Contract Synthesis in a Rewriting Framework
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.
Cite
@article{arxiv.1608.05619,
title = {Symbolic Abstract Contract Synthesis in a Rewriting Framework},
author = {María Alpuente and Daniel Pardo and Alicia Villanueva},
journal= {arXiv preprint arXiv:1608.05619},
year = {2016}
}
Comments
Pre-proceedings paper presented at the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016), Edinburgh, Scotland UK, 6-8 September 2016 (arXiv:1608.02534)