Symbolic abstract contract synthesis in a rewriting framework
From MaRDI portal
Publication:2409736
DOI10.1007/978-3-319-63139-4_11zbMATH Open1485.68051arXiv1608.05619OpenAlexW2512021169MaRDI QIDQ2409736FDOQ2409736
Authors: María Alpuente, D. Pardo, A. Villanueva 
Publication date: 13 October 2017
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.
Full work available at URL: https://arxiv.org/abs/1608.05619
Recommendations
- Abstract contract synthesis and verification in the symbolic \(\mathbb{K}\) framework
- Modular inference of subprogram contracts for safety checking
- Maximal specification synthesis
- An abstract contract theory for programs with procedures
- Higher order symbolic execution for contract verification and refutation
Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Cited In (5)
Uses Software
This page was built for publication: Symbolic abstract contract synthesis in a rewriting framework
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2409736)
