2013/01/21 by Marı́a Alpuente, Marco A. Feliú, Alicia Villanueva · 1 voice
Computer Science · #Formal Methods in Verification #Machine Learning and Algorithms #Software Testing and Debugging Techniques
paper · doi:10.1145/2426890.2426914
openalex publication_date 2013/01/21 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/29
Formal specifications can be used for various software engineering activities ranging from finding errors to documenting software and automatic test-case generation. Automatically discovering specifications for heap-manipulating programs is a challenging task. In this paper, we propose a technique for automatically inferring formal specifications from C code which is based on the symbolic execution and automated reasoning tandem "Matching Logic/K framework". We implemented our technique for a fragment of C called KernelC, in the automated tool KingSpec, which generates axioms that describe the precise input/output behavior of C routines that handle pointer-based structures, i.e., result values and state change. These specifications can be written either in Matching Logic itself, which is useful for further automated analysis within the K formal environment, or in sugared axiomatic form, which favors better human inspection. Since we rely on rewriting logic K semantics specification of programming languages, our approach can be easily extended to any language for which %that a formal semantics in K is given.