View source for C implicit track

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 [http://www.ficticiousAddress.com].

* [[ C implicit Team0 Benchmark1 |  Benchmark 1 ]]


== Team 1 (E-ACSL) ==

[http://frama-c.com/eacsl.html E-ACSL] is both a formal specification language and a [http://frama-c.com Frama-C] plugin for runtime assertion checking of C code.

The [http://frama-c.com/download/e-acsl/e-acsl.pdf 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 [http://frama-c.com/download/e-acsl/e-acsl-0.6.tar.gz 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 [http://www-list.cea.fr CEA LIST]

Further information about E-ACSL can be found [http://frama-c.com/eacsl.html here].

== Team 2  ==