Difference between revisions of "C implicit track"

Revision as of 16:31, 3 June 2016

The C implicit track is concerned with the monitoring of implicit properties of C programs. This is the first time we are running this track and want to be somewhat guided by the participants of the track. The idea is that programs will be submitted and general implicit properties (such as memory safety) should be checked.

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 BenchmarkY).

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

Benchmark Template - C implicit 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: Illegal heap dereference

Team 2