English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Despite its many unquestionable benefits, formal specifications are notwidely used in industrial software development. In order to reduce the time andeffort required to write formal specifications, in this paper we propose atechnique for automatically discovering specifications from real code. Theproposed methodology relies on the symbolic execution capabilities recentlyprovided by the K framework that we exploit to automatically infer formalspecifications from programs that are written in a non-trivial fragment of C,called KernelC. Roughly speaking, our symbolic analysis of KernelC programsexplains the execution of a (modifier) function by using other (observer)routines in the program. We implemented our technique in the automated toolKindspec 2.0, which generates axioms that describe the precise input/outputbehavior of C routines that handle pointer-based structures (i.e., resultvalues and state change). We describe the implementation of our system anddiscuss the differences w.r.t. our previous work on inferring specificationsfrom C code.

Automatic Inference of Specifications in the K Framework