2016/08/19 by Marı́a Alpuente, Alpuente, María, Daniel Pardo +3
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Programming Languages (cs.PL) #Security and Verification in Computing #Software Engineering Research
paper · pdf · doi:10.48550/arxiv.1608.05619
openalex publication_date 2016/08/19 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.