Difference between revisions of "C generic track"

From CRV
Jump to: navigation, search
(Created page with "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 ex...")
 
(Team 1 (E-ACSL))
 
(3 intermediate revisions by 2 users not shown)
Line 17: Line 17:
 
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].
 
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 generic Team1 Benchmark1 |  Benchmark 1 ]]
+
* [[ C generic Team0 Benchmark1 |  Benchmark 1 ]]
  
  
== Team 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.
 +
 
 +
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].
 +
 
 +
* [[ C generic Team1 (E-ACSL) Benchmark1 | Benchmark 1: Integer overflow via addition ]]
 +
* [[ C generic Team1 (E-ACSL) Benchmark2 | Benchmark 2: Loop invariant ]]
 +
* [[ C generic Team1 (E-ACSL) Benchmark3 | Benchmark 3: Vampire number ]]
  
 
== Team 2 ==
 
== Team 2 ==

Latest revision as of 10:00, 5 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].


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 ACSL. E-ACSL supports function contracts, assertions, user-defined predicates and built-in predicates.

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.

Team 2