Symbolic abstract contract synthesis in a rewriting framework

DOI10.1007/978-3-319-63139-4_11MaRDI QIDQ2409736zbMATH OpenOpenAlexFDO

Authors María Alpuente, D. Pardo, A. Villanueva

Publication date 13 October 2017

Full work available at URL https://arxiv.org/abs/1608.05619

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

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.

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

Cited in

(5)

• Abstract contract synthesis and verification in the symbolic \(\mathbb{K}\) framework
• Contract lenses: Reasoning about bidirectional programs via calculation
• KindSpec
• Maximal specification synthesis
• An active learning approach to synthesizing program contracts

Describes a project that uses

Uses Software

• z3
• Daikon

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)