  Despite its many unquestionable benefits, formal specifications are not
widely used in industrial software development. In order to reduce the time and
effort required to write formal specifications, in this paper we propose a
technique for automatically discovering specifications from real code. The
proposed methodology relies on the symbolic execution capabilities recently
provided by the K framework that we exploit to automatically infer formal
specifications from programs that are written in a non-trivial fragment of C,
called KernelC. Roughly speaking, our symbolic analysis of KernelC programs
explains the execution of a (modifier) function by using other (observer)
routines in the program. We implemented our technique in the automated tool
Kindspec 2.0, 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). We describe the implementation of our system and
discuss the differences w.r.t. our previous work on inferring specifications
from C code.
