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

We present a novel proof by induction algorithm, which combines k-inductionwith invariants to model check C programs with bounded and unbounded loops. Thek-induction algorithm consists of three cases: in the base case, we aim to finda counterexample with up to k loop unwindings; in the forward condition, wecheck whether loops have been fully unrolled and that the safety property Pholds in all states reachable within k unwindings; and in the inductive step,we check that whenever P holds for k unwindings, it also holds after the nextunwinding of the system. For each step of the k-induction algorithm, we inferinvariants using affine constraints (i.e., polyhedral) to specify pre- andpost-conditions. The algorithm was implemented in two different ways, with andwithout invariants using polyhedral, and the results were compared.Experimental results show that both forms can handle a wide variety of safetyproperties; however, the k-induction algorithm adopting polyhedral solves moreverification tasks, which demonstrate an improvement of the induction algorithmeffectiveness.

Model Checking C Programs with Loops via k-Induction and Invariants