CRV-2015 Benchmark Phase (February 15, 2015 -> March 15, 2015)

In this phase, competitors provide programs/traces and properties to be shared between participants. A program and an associated property is referred to as a contribution in the following. Each participating team is allowed to provide up to 5 (five) contributions. Contributions should be should be usable independently. CRV’15 chairs may (or not) provide contributions from CSRV’14. Contributions follow one of the two forms below depending on whether one is interested in programs or traces.

For Programs (Java and C tracks):
Each contribution should be structured as follows:

  • Program package:
    • program source code
    • script to compile
    • script to run
    • explanation
  • Specification package a collection of files, each containing:
    • a property that contains:
      • a formal representation of it
      • informal explanation
      • short traces demonstrating valid and invalid behaviours
      • verdict, i.e., what is the evaluation of the property on the program
    • instrumentation instrume setup (manually inserted print statements or AspectJ file with a script to instrument)
    • explanation (including the number of events the program is supposed to generate)

Each specification consists of a list of properties, with instrumentation information, with explanation. The instrumentation information maps the events referred to in the properties to concrete program events. A property consists of a formalization (automata, formula, etc), and informal description, and whether the program satisfies the property (i.e., what is the expected verdict). Instrumentation is a mapping from concrete events (in the program) to abstract events (in the specification). For instance, if one considers the HasNext property on iterators, the mapping should indicate that the hasNext() event in the property refers to a call to the hasnext() method on an Iterator object. We allow for several concrete events to be associated to one abstract event.

Remark 1: Consider that too comprehensive properties may refrain people from wanting to compete on this property.
Remark 2: “Nondeterministic” programs should be avoided as they may interfere with verdict detection.
Remark 3: Each submitted benchmark should be standalone, i.e., it should not depend on any thirdparty program.

For Traces (offline track):
Each contribution should be structured as follows:

  • Trace
  • Specification package a collection of files, each containing:
    • a formal representation of it
    • informal explanation
    • short traces demonstrating valid and invalid behaviour
    • verdict, i.e., what is the evaluation of the property on the program
  • script to run
  • explanation

Instrumentation is a mapping from concrete events (in the trace) to abstract events (in the specification). Traces are sequences of named records of the form:

NAME{
field1 : value1,
...
fieldn : valuen
}

An event has a name and arguments each of which has a name and a value. Logs will be accepted in several formats1, given through the examples below (where an_event_name ranges over the set of possible event names, a_field_name ranges over the set of possible field names, a_value ranges over the set of possible runtime values.

  • In XML:

    <log>

      <event>

       <name>an_event_name</name>

       <field>

         <name>a_field_name</name>

         <value>a_value</value>

       </field>

       <field>

         <name>a_field_name</name>

         <value>a_value</value>

       </field>

     </event>

     <event>

       <name>EVR</name>

       <field>

         <name>a_field_name</name>

         <value>a_value</value>

       </field>

       <field>

         <name>a_field_name</name>

         <value>a_value</value>

       </field>

     </event>

    </log>

     

  • In CVS format (following http://www.ietf.org/rfc/rfc4180.txt)2:

    event, a_field_name, a_field_name, a_field_name
    an_event_name, a_field_value, a_field_value, a_field_value

  • In JSON format (following https://tools.ietf.org/html/rfc7159 ):

    an_event_name: {
    a_field_name: “a_value”,
    a_field_name: “a_value”
    }

1During the evaluation phase, traces will be provided in the three formats to let participants choose the format they prefer.
2The spaces are intended and required.