Difference between revisions of "C generic track"

Revision as of 16:44, 3 June 2016

The C generic track is concerned with the monitoring of C programs. A benchmark will consist of a C program and a specification (see the rules document).

Please follow the example of Team 0 in how to organise your submission i.e. provide a team name and description and create a page per benchmark (named Track TeamX BenchmarkX).

Please use the below template to create your benchmark Wiki pages. Do not modify the template.

Benchmark Template - C generic track

Team 0 (ExampleName)

The ExampleName tool works by magic dust and hope, utilising a new constant time algorithm for sorting. This paragraph is an example of the fact that there should be a few sentences written about the team and its tool. The tool is developed by John Lennon and Tintin. Further information about the tool can be found at [1].

• Benchmark 1

Team 1 (E-ACSL)

E-ACSL is both a formal specification language and a Frama-C plugin for runtime assertion checking of C code.

The E-ACSL specification language is an executable subset of the behavioral specification language for C programs called [http://frama- c.com/acsl.html ACSL]. E-ACSL supports function contracts, assertions, user-defined predicates and built-in predicates (like \valid(p) indicating that reading from or writing to a memory location pointed to by a pointer p is safe).

The E-ACSL Frama-C plugin E-ACSL Frama-C plugin automatically converts a given C program (say P) containing E-ACSL annotations into a program P' instrumented with assertions that verify E-ACSL properties at runtime.

E-ACSL is developed by the Software Security Laboratory at CEA LIST

Further information about E-ACSL can be found here.

• Benchmark 1: Integer overflow via addition
• Benchmark 2: Loop invariant
• Benchmark 3: Vampire number

Team 2