C generic Team1 (E-ACSL) Benchmark2

From CRV

Revision as of 16:45, 3 June 2016 by E-acsl (Talk | contribs) (→‎Loop invariant)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

Jump to: navigation, search

Contents

1 Benchmark Data
- 1.1 The Trace Part
- 1.2 The Property Part

Benchmark Data

This benchmark is located in crv.liflab.ca@/home/e-acsl/crv16_benchmarks/c-generic-track/loop-invariant

The Trace Part

E-ACSL has no notion of trace

The Property Part

Informal Description

Demonstration Traces

Formal Specification

The formal property is given using the ACSL

A FO-LTL Specification

Retrieved from "http://165.22.237.132/wiki/index.php?title=C_generic_Team1_(E-ACSL)_Benchmark2&oldid=148"