start2 and time as well as corresponding data values, e.g., true, false and 201302, respectively. It includes a number of traces that are separated by events with name log. That is, between consecutive traces there is an entry such as the following.

```xml
<event>
  <name>log</name>
  <field>
    <name>id</name>
    <value>1</value>
  </field>
</event>
```

Single positions within a trace are represented by events with name step such as, for example,

```xml
<event>
  <name>step</name>
  <field>
    <name>alarm</name>
    <value>true</value>
  </field>
  <field>
    <name>init</name>
    <value>0</value>
  </field>
  <field>
    <name>time</name>
    <value>770576</value>
  </field>
</event>
```

The property is to be evaluated separately on the traces represented in the log file.

**Description of the property** The property expresses that alarm events occurring within a time frame of 60 s after a start2 event constitute an error. That is, the difference of the values of the attribute time between any two start2/alarm events is supposed to be at least 60,000 ms.

Formally, considering the log file as a linearly ordered structure (T, <) of events e ∈ T the task is to compute a predicate F ⊆ T comprising those positions that exhibit a failure. We define the predicate by

$$F(e) :\Leftrightarrow \left( \begin{array}{l} \text{field}(e, \text{alarm}) = \text{true} \land \\ t(e, \text{time}) = x \Rightarrow \exists e' < e : \\ t(e', \text{start2}) = \text{true} \land \\ x - t(e', \text{time}) < 60,000 \end{array} \right)$$

for all events e ∈ T and all time stamps x where we assume T to give rise to mapping t : T × A → V that maps lines and attribute names A to values V.

As an example, consider the sequence:

```
start2      stop      alarm
200,000    230,000  240,000
```

where the first line indicates the Boolean attributes that hold and the second line indicates the corresponding values of the attribute time. The last position in the sequence is violating the property because of the early alarm. However, the sequence

```
start1 alarm start2 stop alarm
100,000 110,000 200,000 230,000 260,000
```

satisfies the property, i.e., it has no position exhibiting a failure.

### 4.3.12 Duration of machine operations

**Description of the log** This benchmark is based on the same log file as the one described in Sect. 4.3.11.

**Description of the property** The benchmark considers processes that are started upon start1 events. A stop event stops all these running processes. Failures are stop events that occur more than 30 s after the most recent start1 event and if since then no stop event has occurred. That is, the difference of the values of the attribute time between two consecutive start1/stop events is supposed to be at most 30,000 ms.

As is the case with the benchmark in Sect. 4.3.11, the failure predicate F is such that for all e ∈ T, F(e) holds if and only if for all time stamps x ∈ V, the following formula holds:

$$ 
\begin{align*}
t(e, \text{stop}) &= \text{true} \land t(e, \text{time}) = x \Rightarrow \exists e' < e : \\
t(e', \text{start1}) &= \text{true} \land \\
x - t(e', \text{time}) &> 30,000 \land \\
(\forall e' < e'' < e : t(e'', \text{start1}) \neq \text{true} \land \\
t(e'', \text{stop}) \neq \text{true})
\end{align*}
$$

for all events e ∈ T. As an example, consider the sequence

```
start1      start2      stop      alarm
100,000    200,000    230,000  240,000
```

where at the third position the property is violated because of the late stop event. However, the sequence

```
start1      stop      start2      stop      alarm
100,000    110,000   200,000    230,000  260,000
```

does not violate the property.
### 4.3.13 Maximal error rates of machines operations

*Description of the log* This benchmark is based on the same log file as the one described in Sect. 4.3.11.

*Description of the property* This quantitative property specifies that the number of errors is at most a fraction $2 \cdot 10^{-5}$ (i.e., 0.002%) of the number of performed operation cycles. The log file provides information about the number of registered errors and the number of performed cycles at every position.

An event $e \in T$ constitutes a failure if and only if

$$t(e, \text{error\_count}) > 0 \land t(e, \text{cycle\_count}) > 0 \land \\ t(e, \text{error\_count}) > 0.00002 \cdot t(e, \text{cycle\_count}).$$

### 4.3.14 Ordering of machine operations

*Description of the log* This benchmark is based on the same log file as the one described in Sect. 4.3.11.

*Description of the property* The trace is divided into groups, phases and runs, and the latter are parameterized by (process) IDs. All processes $x$ have to proceed the three steps *init*, *run* and *finish* in that order. Then, they may restart and proceed again. They must always finish. While actions of an individual process must be correctly ordered, they can be interleaved with the actions from other processes. For example, valid interleavings are

```
init run init finish run finish
1 1 2 1 2 2
```

and

```
init init run init run run finish finish finish
1 2 1 3 3 2 2 3 1
```

A phase is such an interleaved sequence preceded by an event *phaseStart*. Whenever a phase starts, all running processes started before must have finished. Phases belong to a group. The beginning of a group of phases is indicated by an event *groupStart*, and the end of a group is indicated by an event *groupEnd*. Groups cannot interleave and any process event (*init*, *run*, *finish*) and phase start event must happen within a group, i.e., between two consecutive *groupStart*/*groupEnd* events. The running time of a group must be smaller than 480 seconds, i.e., the difference of the corresponding time stamps must respect that constraint.

To formalize these requirements, we split it up into individual constraints:

- $P_1$: Groups do not overlap

- $P_2$: Ending groups must have started

- $P_3$: Phases are included in groups

- $P_4$: All processes must have finished before the next phase

- $P_5$: Init before run

- $P_6$: Run before finish

- $P_7$: Init after finish

- $P_8$: Init, run, finish not outside group

- $P_9$: Group duration is less than 480 s

We formulate these properties in a combination of Linear-time Temporal Logic (LTL) and First-order Logic (FO) as described in [39]. To this end, the log file is interpreted as sequence of FO structures modelling events and attached data. Every event $e$ provides an interpretation for the unary predicate symbols *init*, *run*, *finish*, the Boolean propositions *groupStart*, *groupEnd*, *phaseStart* and the constant *time* by

$$ 
\begin{align*}
\mathit{init}(x) &:= 0 < x = t(e, \mathit{init}) \\
\mathit{run}(x) &:= 0 < x = t(e, \mathit{run}) \\
\mathit{finish}(x) &:= 0 < x = t(e, \mathit{finish}) \\
\mathit{groupStart} &:= t(e, \mathit{group\_start}) = \mathit{true} \\
\mathit{groupEnd} &:= t(e, \mathit{group\_end}) = \mathit{true} \\
\mathit{phaseStart} &:= t(e, \mathit{phase\_start}) = \mathit{true} \\
\mathit{time} &:= t(e, \mathit{time})
\end{align*}
$$

As above, we assume that the function $t$ maps attributes and event representations in the log file to the corresponding values. Whenever a field *group_start*, *group_end* or *phase_start* is not explicitly specified in the log, the respective value is assumed to be false. We now express the constraints above by the formulae

$$P_1 = \mathit{groupStart} \Rightarrow \bar{Y}(\neg \mathit{groupStart} \ \mathit{WS} \ \mathit{groupEnd})$$

$$P_2 = \mathit{groupEnd} \Rightarrow Y(\neg \mathit{groupEnd} \ \mathit{SgroupStart})$$

$$P_3 = \mathit{phaseStart} \Rightarrow \neg \mathit{groupEnd} \ \mathit{SgroupStart})$$

$$P_4 = \forall x \ \mathit{phaseStart} \Rightarrow \neg (\mathit{init}(x) \lor \mathit{run}(x)) \ \mathit{WS} \ \mathit{finish}(x)$$

$$P_5 = \forall x \ \mathit{run}(x) \implies Y(\neg \mathit{run}(x) \ \mathit{Sinit}(x))$$

$$P_6 = \forall x \ \mathit{finish}(x) \implies Y(\neg \mathit{finish}(x) \ \mathit{Srun}(x))$$

$$P_7 = \forall x \ \mathit{init}(x) \implies \bar{Y}(\neg (\mathit{init}(x) \lor \mathit{run}(x)) \ \mathit{WS} \ \mathit{finish}(x))$$

$$P_8 = \forall x (\neg \mathit{groupStart} \ \mathit{WS} \ \mathit{groupEnd}) \\ \qquad \implies \neg \mathit{finish}(x) \land \neg \mathit{init}(x) \land \neg \mathit{run}(x)$$

$$P_9 = \forall x \ \mathit{groupEnd} \land \\ \qquad (\neg \mathit{groupStart} \ \mathit{S}(\mathit{groupStart} \land \mathit{time} = x)) \\ \qquad \implies \mathit{time} - x < 480,000)$$

with the past-time temporal operators $Y$ (yesterday), $\bar{Y}$ (weak yesterday), $S$ (since) and $\mathit{WS}$ (weak since).
### 4.3.13 Maximal error rates of machines operations

Description of the log This benchmark is based on the same log file as the one described in Sect. 4.3.11.

Description of the property This quantitative property specifies that the number of errors is at most a fraction $2 \cdot 10^{-5}$ (i.e., 0.002%) of the number of performed operation cycles. The log file provides information about the number of registered errors and the number of performed cycles at every position.

An event $e \in T$ constitutes a failure if and only if

$$t(e, \text{error\_count}) > 0 \land t(e, \text{cycle\_count}) > 0 \land \\ t(e, \text{error\_count}) > 0.00002 \cdot t(e, \text{cycle\_count}).$$

### 4.3.14 Ordering of machine operations

Description of the log This benchmark is based on the same log file as the one described in Sect. 4.3.11.

Description of the property The trace is divided into groups, phases and runs, and the latter are parameterized by (process) IDs. All processes $x$ have to proceed the three steps `init`, `run` and `finish` in that order. Then, they may restart and proceed again. They must always finish. While actions of an individual process must be correctly ordered, they can be interleaved with the actions from other processes. For example, valid interleavings are

```
init run init finish run finish
1 1 2 1 2 2
```

and

```
init init run init run run finish finish finish
1 2 1 3 3 2 2 3 1
```

A phase is such an interleaved sequence preceded by an event `phaseStart`. Whenever a phase starts, all running processes started before must have finished. Phases belong to a group. The beginning of a group of phases is indicated by an event `groupStart`, and the end of a group is indicated by an event `groupEnd`. Groups cannot interleave and any process event (`init`, `run`, `finish`) and phase start event must happen within a group, i.e., between two consecutive `groupStart`/`groupEnd` events. The running time of a group must be smaller than 480 seconds, i.e., the difference of the corresponding time stamps must respect that constraint.

To formalize these requirements, we split it up into individual constraints:

- $P_1$: Groups do not overlap

- $P_2$: Ending groups must have started

- $P_3$: Phases are included in groups

- $P_4$: All processes must have finished before the next phase

- $P_5$: Init before run

- $P_6$: Run before finish

- $P_7$: Init after finish

- $P_8$: Init, run, finish not outside group

- $P_9$: Group duration is less than 480 s

We formulate these properties in a combination of Linear-time Temporal Logic (LTL) and First-order Logic (FO) as described in [39]. To this end, the log file is interpreted as sequence of FO structures modelling events and attached data. Every event $e$ provides an interpretation for the unary predicate symbols `init`, `run`, `finish`, the Boolean propositions `groupStart`, `groupEnd`, `phaseStart` and the constant `time` by

$$ 
\begin{align*}
\texttt{init}(x) &:= 0 < x = t(e, \texttt{init}) \\
\texttt{run}(x) &:= 0 < x = t(e, \texttt{run}) \\
\texttt{finish}(x) &:= 0 < x = t(e, \texttt{finish}) \\
\texttt{groupStart} &:= t(e, \texttt{group\_start}) = \texttt{true} \\
\texttt{groupEnd} &:= t(e, \texttt{group\_end}) = \texttt{true} \\
\texttt{phaseStart} &:= t(e, \texttt{phase\_start}) = \texttt{true} \\
\texttt{time} &:= t(e, \texttt{time})
\end{align*}
$$

As above, we assume that the function $t$ maps attributes and event representations in the log file to the corresponding values. Whenever a field `group_start`, `group_end` or `phase_start` is not explicitly specified in the log, the respective value is assumed to be false. We now express the constraints above by the formulae

$$P_1 = \text{groupStart} \Rightarrow \bar{Y}(\neg \text{groupStart} \text{ WS groupEnd})$$

$$P_2 = \text{groupEnd} \Rightarrow Y(\neg \text{groupEnd} \text{ SgroupStart})$$

$$P_3 = \text{phaseStart} \Rightarrow \neg \text{groupEnd} \text{ SgroupStart})$$

$$P_4 = \forall x \text{ phaseStart} \Rightarrow \neg (\text{init}(x) \lor \text{run}(x)) \text{ WS finish}(x)$$

$$P_5 = \forall x \text{ run}(x) \Rightarrow Y(\neg \text{run}(x) \text{ Sinit}(x))$$

$$P_6 = \forall x \text{ finish}(x) \Rightarrow Y(\neg \text{finish}(x) \text{ Srun}(x))$$

$$P_7 = \forall x \text{ init}(x) \Rightarrow \bar{Y}(\neg (\text{init}(x) \lor \text{run}(x)) \text{ WS finish}(x))$$

$$P_8 = \forall x (\neg \text{groupStart} \text{ WS groupEnd}) \\ \Rightarrow \neg \text{finish}(x) \land \neg \text{init}(x) \land \neg \text{run}(x)$$

$$P_9 = \forall x \text{ groupEnd} \land \\ (\neg \text{groupStart} \text{ S}(\text{groupStart} \land \text{time} = x)) \\ \Rightarrow \text{time} - x < 480,000)$$

with the past-time temporal operators $Y$ (yesterday), $\bar{Y}$ (weak yesterday), $S$ (since) and $WS$ (weak since).
The task is to compute all positions in the log file where any of these properties is violated.

### 4.3.15 Existence of a leader Rover

This benchmark is provided by the QEA team.

*Description of the log* The supplied trace file contains 9756 events in CSV format and satisfies the property.

*Description of the property* This property relates to the self-organization of communicating rovers and captures the situation where (at least) one rover is able to communicate with all other (known) rovers.

The property states that there exists a leader (rover) who has pinged every other (known) rover and received an acknowledgement. The leader does not need to ping itself, and communication is bidirectional, i.e., any rover can ping any other rover. For example, the following trace satisfies the property as B pings A and C and receives an acknowledgement.

```
ping(B, A).ping(B, C).ack(C, B).ack(A, B)
```

The following trace is not correct as B does not ping D.

```
ping(B, A).ping(B, C).ack(C, B).ack(A, B).ping(D, B)
```

The property can be captured by the following QEA. The syntax of QEA is described in Sect. 4.2.20.

The automaton structure of this QEA is simple; it detects the language ping followed by ack. The quantifications are non-trivial. As expected, there is an existential quantification followed by a universal quantification and the constraint that r1 and r2 are not equal. The Join statement captures the fact that the domains of quantification for r1 and r2 should be equal. This is important as domains of quantification are extracted from the trace using the alphabet of the automaton and without this declaration the domains may not be equal.

```
qea {
  Exists (r1) Forall (r2) Where (r1!=r2)
    Join (r1, r2)
  skip (start) { ping (r1, r2) -> pinged
  }
  skip (pinged) { ack (r2, r1) -> success
  }
}
```

### 4.3.16 Granting resources to tasks

This benchmark is provided by the QEA team.

*Description of the log* The supplied trace file contains 1,000,002 events in CSV format and violates the property.

There are two errors: 1) a resource is cancelled by a task not holding it; and 2) a resource is granted to multiple tasks.

*Description of the property* This benchmark is related to resource management in a context where resources can be granted to tasks. The property here is that every resource should only be held by at most one task at any one time. If a resource is granted to a task, it should be cancelled before being granted to another task. This is therefore a mutual exclusion property.

The property can be captured by the following QEA. This quantifies over resources r and uses two free variables t1 and t2 to check mutual exclusion of the task holding the resource. Note that in the granted state any grant event leads to failure and a cancel event with a different task will lead to failure as this is a next state.

```
qea {
  Forall (r)
    accept next (free) { grant (t1, r) -> granted }
    accept next (granted) {
      grant (t2, r) -> failure
      cancel (t2, r) if [ t1 = t2 ] -> free
    }
}
```

### 4.3.17 Nested command messages

This benchmark is provided by the QEA team.

*Description of the log* The supplied trace file contains 1200 events in CSV format and violates the property.

*Description of the property* This benchmark relates to a communication consisting of command and success messages. The property states that if command with identifier B starts after command with identifier A has started, then command B must succeed before command A succeeds. It can be assumed that every command is started and succeeds exactly once, i.e., this is a property that has been checked separately.

The QEA defining this property is described as follows. Two commands c1 and c2 are quantified over and the states none, startedOne and startedTwo indicate whether command 1 or 2 has started, respectively. Note that the property is symmetric, so there are two instances for each pair of commands reflecting the two orderings of commands.

```
qea {
  Forall (c1, c2)
    accept next (none) {
      com (c2) -> none; suc (c2) -> none
      com (c1) -> startedOne
    }
    accept next (startedOne) {
      com (c2) -> startedTwo
      suc (c2) -> none
    }
    accept next (startedTwo) {
      suc (c2) -> startedOne
    }
}
```
The task is to compute all positions in the log file where any of these properties is violated.

### 4.3.15 Existence of a leader Rover

This benchmark is provided by the QEA team.

*Description of the log* The supplied trace file contains 9756 events in CSV format and satisfies the property.

*Description of the property* This property relates to the self-organization of communicating rovers and captures the situation where (at least) one rover is able to communicate with all other (known) rovers.

The property states that there exists a leader (rover) who has pinged every other (known) rover and received an acknowledgement. The leader does not need to ping itself, and communication is bidirectional, i.e., any rover can ping any other rover. For example, the following trace satisfies the property as B pings A and C and receives an acknowledgement.

```
ping(B, A).ping(B, C).ack(C, B).ack(A, B)
```

The following trace is not correct as B does not ping D.

```
ping(B, A).ping(B, C).ack(C, B).ack(A, B).ping(D, B)
```

The property can be captured by the following QEA. The syntax of QEA is described in Sect. 4.2.20.

The automaton structure of this QEA is simple; it detects the language ping followed by ack. The quantifications are non-trivial. As expected, there is an existential quantification followed by a universal quantification and the constraint that r1 and r2 are not equal. The Join statement captures the fact that the domains of quantification for r1 and r2 should be equal. This is important as domains of quantification are extracted from the trace using the alphabet of the automaton and without this declaration the domains may not be equal.

```
qea {
  Exists (r1) Forall (r2) Where (r1!=r2)
    Join (r1, r2)
  skip (start) { ping (r1, r2) -> pinged
  }
  skip (pinged) { ack (r2, r1) -> success
  }
}
```

### 4.3.16 Granting resources to tasks

This benchmark is provided by the QEA team.

*Description of the log* The supplied trace file contains 1,000,002 events in CSV format and violates the property.

There are two errors: 1) a resource is cancelled by a task not holding it; and 2) a resource is granted to multiple tasks.

*Description of the property* This benchmark is related to resource management in a context where resources can be granted to tasks. The property here is that every resource should only be held by at most one task at any one time. If a resource is granted to a task, it should be cancelled before being granted to another task. This is therefore a mutual exclusion property.

The property can be captured by the following QEA. This quantifies over resources r and uses two free variables t1 and t2 to check mutual exclusion of the task holding the resource. Note that in the granted state any grant event leads to failure and a cancel event with a different task will lead to failure as this is a next state.

```
qea {
  Forall (r)
    accept next (free) { grant (t1,r) -> granted }
    accept next (granted) {
      grant (t2,r) -> failure
      cancel (t2,r) if [ t1 = t2 ] -> free
    }
}
```

### 4.3.17 Nested command messages

This benchmark is provided by the QEA team.

*Description of the log* The supplied trace file contains 1200 events in CSV format and violates the property.

*Description of the property* This benchmark relates to a communication consisting of command and success messages. The property states that if command with identifier B starts after command with identifier A has started, then command B must succeed before command A succeeds. It can be assumed that every command is started and succeeds exactly once, i.e., this is a property that has been checked separately.

The QEA defining this property is described as follows. Two commands c1 and c2 are quantified over and the states none, startedOne and startedTwo indicate whether command 1 or 2 has started, respectively. Note that the property is symmetric, so there are two instances for each pair of commands reflecting the two orderings of commands.

```
qea {
  Forall (c1, c2)
    accept next (none) {
      com (c2) -> none; suc (c2) -> none
      com (c1) -> startedOne
    }
    accept next (startedOne) {
      com (c2) -> startedTwo
      suc (c2) -> none
    }
    accept next (startedTwo) {
      suc (c2) -> startedOne
    }
}
```
It was noted by Klaus Havelund that this QEA could be rewritten to more accurately reflect the assumption about commands starting and succeeding exactly once. As for the benchmark described in Sect. 4.2.23, a modified version of the property can be found in [52].

### 4.3.18 Resource lifecycle

This benchmark is provided by the QEA team.

As the benchmark in Sect. 4.3.16, this benchmark is related to resource management.

*Description of the log* The supplied trace file contains 1 million events in CSV format and violates the property. The violation occurs due to a resource not being cancelled when the trace finishes.

*Description of the property* In this case, the property concerns the lifecycle of a resource. Implicitly this is with respect to a single task, i.e., we assume the trace only contains events from a single tasks interaction. A variant of this property appears in [52] where the task is also quantified.

The steps of the lifecycle are as follows:

- A resource may be requested

- A requested resource may be denied or granted

- A granted resource may be rescinded or cancelled

- A resource may only be requested when not currently requested or granted

- A granted resource must eventually be cancelled

This is captured by the following QEA which quantifies over the resource *r* and captures the lifecycle in the automaton structure.

```
qea {
    Forall (r)
    accept next (free) {
        request(r) -> requested
    }
    accept next (requested) {
        deny(r) -> free
        grant(r) -> granted
    }
    accept next (granted) {
        cancel(r) -> free
        rescind(r) -> granted
    }
}
```

### 4.3.19 Respecting conflicts of resources

This benchmark is provided by the QEA team.

As the benchmark in Sect. 4.3.16, this benchmark is related to resource management.

*Description of the log* The supplied trace file contains 100 2954 events in CSV format and satisfies the property.

*Description of the property* This benchmark focuses on conflicts between resources. It is assumed that conflicts between resources are declared at the beginning of operation and that after this point resources that are in conflict with each other cannot be granted at the same time. It is assumed a resource cannot be put in conflict with itself.

A QEA for this property is given as follows. It quantifies over two resources *r1* and *r2* and detects a conflict declaration between these two resources. After this point, there is a mutual exclusion between the two resources.

```
qea {
    Forall (r1, r2)
    accept skip (start) {
        conflict(r1, r2) -> free
        conflict(r2, r1) -> free
    }
    accept skip (free) {
        grant(r1) -> granted1
        grant(r2) -> granted2
    }
    accept next (granted1) {
        cancel(r1) -> free
    }
    accept next (granted2) {
        cancel(r2) -> free
    }
}
```

## 5 Evaluation: calculating scores

In this section, we present in detail the algorithm to calculate the final score for each tool. Consider one of the three competition tracks (C, Java, and Offline). Let *N* be the number of teams/tools participating in the considered track and *L* be the total number of benchmarks provided by all teams. The maximal number of experiments for the track is *N* × *L*. That is, each team has the possibility to compete on a benchmark.

Then, for each tool $T_i$ ($1 \le i \le N$) w.r.t. each benchmark $B_j$ ($1 \le j \le L$), we assign three different scores:

- the correctness score $C_{i,j}$,

- the overhead score $O_{i,j}$, and

- the memory-utilization score $M_{i,j}$.

In case of online monitoring (Java and C tracks), let $E_j$ be the execution time of benchmark $B_j$ (without monitor). Note, in the following, to simplicity notation, we assume that all participants of a track want to compete on benchmark $B_j$. Participants can of course decide not to qualify on a benchmark of their track. In this case, the following score definitions can be adapted easily.

Several considerations influenced the scoring principles:

- Since several benchmarks are provided in each track, we wanted to provide participants with the possibility to
It was noted by Klaus Havelund that this QEA could be rewritten to more accurately reflect the assumption about commands starting and succeeding exactly once. As for the benchmark described in Sect. 4.2.23, a modified version of the property can be found in [52].

### 4.3.18 Resource lifecycle

This benchmark is provided by the QEA team.

As the benchmark in Sect. 4.3.16, this benchmark is related to resource management.

*Description of the log* The supplied trace file contains 1 million events in CSV format and violates the property. The violation occurs due to a resource not being cancelled when the trace finishes.

*Description of the property* In this case, the property concerns the lifecycle of a resource. Implicitly this is with respect to a single task, i.e., we assume the trace only contains events from a single tasks interaction. A variant of this property appears in [52] where the task is also quantified.

The steps of the lifecycle are as follows:

- A resource may be requested

- A requested resource may be denied or granted

- A granted resource may be rescinded or cancelled

- A resource may only be requested when not currently requested or granted

- A granted resource must eventually be cancelled

This is captured by the following QEA which quantifies over the resource *r* and captures the lifecycle in the automaton structure.

```
qea {
    Forall (r)
    accept next (free) {
        request(r) -> requested
    }
    accept next (requested) {
        deny(r) -> free
        grant(r) -> granted
    }
    accept next (granted) {
        cancel(r) -> free
        rescind(r) -> granted
    }
}
```

### 4.3.19 Respecting conflicts of resources

This benchmark is provided by the QEA team.

As the benchmark in Sect. 4.3.16, this benchmark is related to resource management.

*Description of the log* The supplied trace file contains 100 2954 events in CSV format and satisfies the property.

*Description of the property* This benchmark focuses on conflicts between resources. It is assumed that conflicts between resources are declared at the beginning of operation and that after this point resources that are in conflict with each other cannot be granted at the same time. It is assumed a resource cannot be put in conflict with itself.

A QEA for this property is given as follows. It quantifies over two resources *r1* and *r2* and detects a conflict declaration between these two resources. After this point, there is a mutual exclusion between the two resources.

```
qea {
    Forall (r1, r2)
    accept skip (start) {
        conflict(r1, r2) -> free
        conflict(r2, r1) -> free
    }
    accept skip (free) {
        grant(r1) -> granted1
        grant(r2) -> granted2
    }
    accept next (granted1) {
        cancel(r1) -> free
    }
    accept next (granted2) {
        cancel(r2) -> free
    }
}
```

## 5 Evaluation: calculating scores

In this section, we present in detail the algorithm to calculate the final score for each tool. Consider one of the three competition tracks (C, Java, and Offline). Let *N* be the number of teams/tools participating in the considered track and *L* be the total number of benchmarks provided by all teams. The maximal number of experiments for the track is *N* × *L*. That is, each team has the possibility to compete on a benchmark.

Then, for each tool $T_i$ ($1 \le i \le N$) w.r.t. each benchmark $B_j$ ($1 \le j \le L$), we assign three different scores:

- the correctness score $C_{i,j}$,

- the overhead score $O_{i,j}$, and

- the memory-utilization score $M_{i,j}$.

In case of online monitoring (Java and C tracks), let $E_j$ be the execution time of benchmark $B_j$ (without monitor). Note, in the following, to simplicity notation, we assume that all participants of a track want to compete on benchmark $B_j$. Participants can of course decide not to qualify on a benchmark of their track. In this case, the following score definitions can be adapted easily.

Several considerations influenced the scoring principles:

- Since several benchmarks are provided in each track, we wanted to provide participants with the possibility to
compete on a benchmark or not. We allocated a maximum number of points that could be gained on a benchmark. In our opinion, it limited the influence of the failure or success on a benchmark and rewarded the overall behavior of tools on the benchmarks in a track.

- We gave an important emphasis on the correctness of monitoring verdicts. As such, the scoring mechanism gives more priority to correctness of verdicts in that performance is evaluated on a benchmark only when a tool provides the correct verdict and negative points are assigned on a benchmark when a tool produces a false verdict or crashes.

- Within a benchmark, scores are assigned to participants/-tools based on how better they perform compared to each other. Moreover, the proportion of points in benchmark assigned to a tool depends on a performance ratio comparing to the average performance of other tools. The average performance of other tools is computed with the geometric mean (because we dealt with normalized numbers [49]).

## 5.1 Correctness score

The correctness score $C_{i,j}$ for a tool $T_i$ running a benchmark $B_j$ is (an integer) calculated as follows:

- $C_{i,j} = 0$, if the property associated with benchmark $B_j$ cannot be expressed in the specification language of $T_i$.

- $C_{i,j} = -10$, if, in case of online monitoring, the property can be expressed, but the monitored program crashes.

- $C_{i,j} = -5$, if, in case of online monitoring, the property can be expressed and no verdict is reported after $10 \times E_j$.

- $C_{i,j} = -5$, if, in case of offline monitoring, the property can be expressed, but the monitor crashes.

- $C_{i,j} = -5$, if the property can be expressed, the tool does not crash, and the verification verdict is incorrect.

- $C_{i,j} = 10$, if the tool does not crash, it allows to express the property of interest, and it provides the correct verification verdict.

Note that, in case of a negative correctness score, there is no evaluation w.r.t. the overhead and memory-utilization scores for the pair $(T_i, B_j)$.

## 5.2 Overhead score

The overhead score $O_{i,j}$, for a tool $T_i$ running benchmark $B_j$, is related to the timing performance of the tool for detecting the (unique) verdict. For all benchmarks, a fixed total number of points $O$ is allocated when evaluating the tools on a benchmark. Thus, the scoring method for overhead ensures that

$$ \sum_{i=1}^{N} \sum_{j=1}^{L} O_{i,j} = O. $$

The overhead score is calculated as follows. First, we compute the overhead index $o_{i,j}$, for tool $T_i$ running a benchmark $B_j$, where the larger the overhead index is, the better.

- In the case of offline monitoring, for the overhead, we consider the elapsed time till the property under scrutiny is either found to be satisfied or violated. If monitoring (with tool $T_i$) of the trace of benchmark $B_j$ executes in time $V_i$, then we define the overhead as

$$ o_{i,j} = \begin{cases} \frac{1}{V_i} & \text{if } C_{i,j} > 0, \\ 0 & \text{otherwise.} \end{cases} $$

- In the case of online monitoring (C or Java), the overhead associated with monitoring is a measure of how much longer a program takes to execute due to runtime monitoring. If the monitored program (with monitor from tool $T_i$) executes in $V_{i,j}$ time units, we define the overhead index as

$$ o_{i,j} = \begin{cases} \frac{\sqrt[N]{\prod_{l=1}^{N} V_{i,j}}}{V_{i,j}} & \text{if } C_{i,j} > 0, \\ 0 & \text{otherwise.} \end{cases} $$

In other words, the overhead index for tool $T_i$ evaluated on benchmark $B_j$ is the geometric mean of the overheads of the monitored programs with all tools over the overhead of the monitored program with tool $T_i$.

Then, the overhead score $O_{i,j}$ for a tool $T_i$ w.r.t. benchmark $B_j$ is defined as follows:

$$ O_{i,j} = O \times \frac{o_{i,j}}{\sum_{l=1}^{N} o_{l,j}}. $$

For each tool, the overhead score is a harmonization of the overhead index so that the sum of overhead scores is equal to $O$.

## 5.3 Memory-utilization score

The memory-utilization score $M_{i,j}$ is calculated similarly to the overhead score. For all benchmarks, a fixed total number of points $O$ is allocated when evaluating the tools on a benchmark. Thus, the scoring method for memory utilization ensures that:

$$ \sum_{i=1}^{N} \sum_{j=1}^{L} M_{i,j} = M. $$
compete on a benchmark or not. We allocated a maximum number of points that could be gained on a benchmark. In our opinion, it limited the influence of the failure or success on a benchmark and rewarded the overall behavior of tools on the benchmarks in a track.

- We gave an important emphasis on the correctness of monitoring verdicts. As such, the scoring mechanism gives more priority to correctness of verdicts in that performance is evaluated on a benchmark only when a tool provides the correct verdict and negative points are assigned on a benchmark when a tool produces a false verdict or crashes.

- Within a benchmark, scores are assigned to participants/-tools based on how better they perform compared to each other. Moreover, the proportion of points in benchmark assigned to a tool depends on a performance ratio comparing to the average performance of other tools. The average performance of other tools is computed with the geometric mean (because we dealt with normalized numbers [49]).

## 5.1 Correctness score

The correctness score $C_{i,j}$ for a tool $T_i$ running a benchmark $B_j$ is (an integer) calculated as follows:

- $C_{i,j} = 0$, if the property associated with benchmark $B_j$ cannot be expressed in the specification language of $T_i$.

- $C_{i,j} = -10$, if, in case of online monitoring, the property can be expressed, but the monitored program crashes.

- $C_{i,j} = -5$, if, in case of online monitoring, the property can be expressed and no verdict is reported after $10 \times E_j$.

- $C_{i,j} = -5$, if, in case of offline monitoring, the property can be expressed, but the monitor crashes.

- $C_{i,j} = -5$, if the property can be expressed, the tool does not crash, and the verification verdict is incorrect.

- $C_{i,j} = 10$, if the tool does not crash, it allows to express the property of interest, and it provides the correct verification verdict.

Note that, in case of a negative correctness score, there is no evaluation w.r.t. the overhead and memory-utilization scores for the pair $(T_i, B_j)$.

## 5.2 Overhead score

The overhead score $O_{i,j}$, for a tool $T_i$ running benchmark $B_j$, is related to the timing performance of the tool for detecting the (unique) verdict. For all benchmarks, a fixed total number of points $O$ is allocated when evaluating the tools on a benchmark. Thus, the scoring method for overhead ensures that

$$ \sum_{i=1}^{N} \sum_{j=1}^{L} O_{i,j} = O. $$

The overhead score is calculated as follows. First, we compute the overhead index $o_{i,j}$, for tool $T_i$ running a benchmark $B_j$, where the larger the overhead index is, the better.

- In the case of offline monitoring, for the overhead, we consider the elapsed time till the property under scrutiny is either found to be satisfied or violated. If monitoring (with tool $T_i$) of the trace of benchmark $B_j$ executes in time $V_i$, then we define the overhead as

$$ o_{i,j} = \begin{cases} \frac{1}{V_i} & \text{if } C_{i,j} > 0, \\ 0 & \text{otherwise.} \end{cases} $$

- In the case of online monitoring (C or Java), the overhead associated with monitoring is a measure of how much longer a program takes to execute due to runtime monitoring. If the monitored program (with monitor from tool $T_i$) executes in $V_{i,j}$ time units, we define the overhead index as

$$ o_{i,j} = \begin{cases} \frac{\sqrt[N]{\prod_{l=1}^{N} V_{i,j}}}{V_{i,j}} & \text{if } C_{i,j} > 0, \\ 0 & \text{otherwise.} \end{cases} $$

In other words, the overhead index for tool $T_i$ evaluated on benchmark $B_j$ is the geometric mean of the overheads of the monitored programs with all tools over the overhead of the monitored program with tool $T_i$.

Then, the overhead score $O_{i,j}$ for a tool $T_i$ w.r.t. benchmark $B_j$ is defined as follows:

$$ O_{i,j} = O \times \frac{o_{i,j}}{\sum_{l=1}^{N} o_{l,j}}. $$

For each tool, the overhead score is a harmonization of the overhead index so that the sum of overhead scores is equal to $O$.

## 5.3 Memory-utilization score

The memory-utilization score $M_{i,j}$ is calculated similarly to the overhead score. For all benchmarks, a fixed total number of points $O$ is allocated when evaluating the tools on a benchmark. Thus, the scoring method for memory utilization ensures that:

$$ \sum_{i=1}^{N} \sum_{j=1}^{L} M_{i,j} = M. $$
First, we measure the memory-utilization index $m_{i,j}$ for tool $T_i$ running a benchmark $B_j$, where the larger memory-utilization index, the better.

- In the case of offline monitoring, we consider the maximum memory allocated during the tool execution. If monitoring (with tool $T_i$) of the trace of benchmark $B_j$ uses a quantity of memory $D_i$, then we define the overhead as:

$$m_{i,j} = \begin{cases} \frac{1}{D_i} & \text{if } C_{i,j} > 0, \\ 0 & \text{otherwise,} \end{cases}$$

That is, the memory-utilization index for tool $T_i$ evaluated on benchmark $B_j$ is the geometric mean of the memory utilizations of the monitored programs with all tools over the memory utilization of the monitored program with tool $T_i$.

- In the case of online monitoring (C or Java tracks), memory utilization associated with monitoring is a measure of the extra memory the monitored program needs (due to runtime monitoring). If the monitored program uses $D_i$, we define the memory utilization as

$$m_{i,j} = \begin{cases} \frac{\sqrt[N]{\prod_{l=1}^{N} D_{i,j}}}{D_{i,j}} & \text{if } C_{i,j} > 0, \\ 0 & \text{otherwise.} \end{cases}$$

Then, the memory-utilization score $M_{i,j}$ for a tool $T_i$ w.r.t. a benchmark $B_j$ is defined as follows:

$$M_{i,j} = M \times \frac{m_{i,j}}{\sum_{l=1}^{N} m_{l,j}}.$$

## 5.4 Final score

The final score $F_i$ for tool $T_i$ is then computed as follows:

$$F_i = \sum_{j=1}^{L} S_{i,j}$$

where:

$$S_{i,j} = \begin{cases} C_{i,j} & \text{if } C_{i,j} \le 0, \\ C_{i,j} + O_{i,j} + M_{i,j} & \text{otherwise.} \end{cases}$$

For the results reported in the next section, we set $O = C = M = 10$, giving the same weight to the correctness, overhead, and memory-utilization scores.

## 6 Results

In this section, we report on the results of the participants.

The raw experimental data and the scripts submitted by participants can be obtained by cloning the repository available at:

https://gitlab.inria.fr/crv14/evaluation.

For each track, we present the scores obtained in each category and the final scores achieved by each team, as defined in Sect. 5. In the following tables, teams are ranked according to their total scores.

Let us recall that the experiments were conducted on DataMill [73]. The selected machine was **queen**, which has an Intel(R) Core(TM) i7-2600K CPU @ 3.40 GHZ (x86_64 architecture with 8 cores), 7.72 GB of DDR3, and is running on a Gentoo Linux distribution. We have considered the Wall-clock time for our measures. Using DataMill guarantees that each tool had the same execution environment, and it was the only running software during each experiment. Tools were allowed to leverage the eight available cores.

### 6.1 Scores for the C track

The detailed scores for the C track are presented in Table 6. The final scores of the C track are reported in Table 7 and can be visualized in Fig. 5. The final ranking of the teams is: first is RiTHM, second is E- ACSL, third is RTC.

As one can observe in Table 7, RiTHM made the difference over E- ACSL on the overhead score, whereas RiTHM and E- ACSL have approximately the same correctness and memory-utilization scores. Moreover, there is an important gap between the two first tools in this track (RiTHM and E- ACSL) and RTC. Possible explanations for this discrepancy are discussed in Sect. 7.

### 6.2 Scores for the Java track

The detailed scores for the Java track are presented in Table 8.

The final scores of the Java track are reported in Table 9 and can be visualized in Fig. 6.

As one can observe in Table 9, the scores between the two first highest scores are really close and we call it a draw between QEA and JAVA- MOP. Thus, the final ranking of the teams is: firsts are QEA and JAVA- MOP, second is JUNITRV, third is LARVA. While there is a draw between QEA and JAVA- MOP, one can notice that QEA did slightly better on the memory-utilization score, while JAVA- MOP did slightly better on the overhead score. While the scores of the tools do not differ much in terms of correctness, the rankings are due to first the overhead score and then the memory score.
First, we measure the memory-utilization index $m_{i,j}$ for tool $T_i$ running a benchmark $B_j$, where the larger memory-utilization index, the better.

- In the case of offline monitoring, we consider the maximum memory allocated during the tool execution. If monitoring (with tool $T_i$) of the trace of benchmark $B_j$ uses a quantity of memory $D_i$, then we define the overhead as:

$$m_{i,j} = \begin{cases} \frac{1}{D_i} & \text{if } C_{i,j} > 0, \\ 0 & \text{otherwise,} \end{cases}$$

That is, the memory-utilization index for tool $T_i$ evaluated on benchmark $B_j$ is the geometric mean of the memory utilizations of the monitored programs with all tools over the memory utilization of the monitored program with tool $T_i$.

- In the case of online monitoring (C or Java tracks), memory utilization associated with monitoring is a measure of the extra memory the monitored program needs (due to runtime monitoring). If the monitored program uses $D_i$, we define the memory utilization as

$$m_{i,j} = \begin{cases} \frac{\sqrt[N]{\prod_{l=1}^{N} D_{i,j}}}{D_{i,j}} & \text{if } C_{i,j} > 0, \\ 0 & \text{otherwise.} \end{cases}$$

Then, the memory-utilization score $M_{i,j}$ for a tool $T_i$ w.r.t. a benchmark $B_j$ is defined as follows:

$$M_{i,j} = M \times \frac{m_{i,j}}{\sum_{l=1}^{N} m_{l,j}}.$$

## 5.4 Final score

The final score $F_i$ for tool $T_i$ is then computed as follows:

$$F_i = \sum_{j=1}^{L} S_{i,j}$$

where:

$$S_{i,j} = \begin{cases} C_{i,j} & \text{if } C_{i,j} \le 0, \\ C_{i,j} + O_{i,j} + M_{i,j} & \text{otherwise.} \end{cases}$$

For the results reported in the next section, we set $O = C = M = 10$, giving the same weight to the correctness, overhead, and memory-utilization scores.

## 6 Results

In this section, we report on the results of the participants.

The raw experimental data and the scripts submitted by participants can be obtained by cloning the repository available at:

https://gitlab.inria.fr/crv14/evaluation.

For each track, we present the scores obtained in each category and the final scores achieved by each team, as defined in Sect. 5. In the following tables, teams are ranked according to their total scores.

Let us recall that the experiments were conducted on DataMill [73]. The selected machine was **queen**, which has an Intel(R) Core(TM) i7-2600K CPU @ 3.40 GHZ (x86_64 architecture with 8 cores), 7.72 GB of DDR3, and is running on a Gentoo Linux distribution. We have considered the Wall-clock time for our measures. Using DataMill guarantees that each tool had the same execution environment, and it was the only running software during each experiment. Tools were allowed to leverage the eight available cores.

### 6.1 Scores for the C track

The detailed scores for the C track are presented in Table 6. The final scores of the C track are reported in Table 7 and can be visualized in Fig. 5. The final ranking of the teams is: first is RiTHM, second is E- ACSL, third is RTC.

As one can observe in Table 7, RiTHM made the difference over E- ACSL on the overhead score, whereas RiTHM and E- ACSL have approximately the same correctness and memory-utilization scores. Moreover, there is an important gap between the two first tools in this track (RiTHM and E- ACSL) and RTC. Possible explanations for this discrepancy are discussed in Sect. 7.

### 6.2 Scores for the Java track

The detailed scores for the Java track are presented in Table 8.

The final scores of the Java track are reported in Table 9 and can be visualized in Fig. 6.

As one can observe in Table 9, the scores between the two first highest scores are really close and we call it a draw between QEA and JAVA- MOP. Thus, the final ranking of the teams is: firsts are QEA and JAVA- MOP, second is JUNITRV, third is LARVA. While there is a draw between QEA and JAVA- MOP, one can notice that QEA did slightly better on the memory-utilization score, while JAVA- MOP did slightly better on the overhead score. While the scores of the tools do not differ much in terms of correctness, the rankings are due to first the overhead score and then the memory score.
<table><caption>**Table 6** Detailed scores for the C track</caption><thead><tr><th rowspan="3">Reference to benchmark description</th><th colspan="3">RITHM</th><th colspan="3">E- ACSL</th><th colspan="3">RTC</th></tr><tr><th>Verdict</th><th>Mem (MB)</th><th>Ovhd (s)</th><th>Verdict</th><th>Mem (MB)</th><th>Ovhd (s)</th><th>Verdict</th><th>Mem (MB)</th><th>Ovhd (s)</th></tr><tr><th>v-score</th><th>m-score</th><th>o-score</th><th>v-score</th><th>m-score</th><th>o-score</th><th>v-score</th><th>m-score</th><th>o-score</th></tr></thead><tbody><tr><td>Section 4.1.1</td><td>F<br>10</td><td>1012756<br>10</td><td>0.68<br>10</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td></tr><tr><td>Section 4.1.2</td><td>F<br>10</td><td>1012756<br>10</td><td>0.68<br>10</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td></tr><tr><td>Section 4.1.3</td><td>F<br>10</td><td>614168<br>10</td><td>0.42<br>10</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td></tr><tr><td>Section 4.1.4</td><td>F<br>10</td><td>614168<br>10</td><td>0.42<br>10</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td></tr><tr><td>Section 4.1.5</td><td>F<br>10</td><td>647696<br>10</td><td>0.69<br>10</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td></tr><tr><td>Section 4.1.6</td><td>F<br>10</td><td>11916<br>4.46</td><td>0.01<br>9.59</td><td>F<br>10</td><td>12980<br>4.10</td><td>0.30<br>0.16</td><td>F<br>10</td><td>37040<br>1.44</td><td>0.19<br>0.14</td></tr><tr><td>Section 4.1.7</td><td>F<br>10</td><td>5388<br>3.18</td><td>0.001<br>9.09</td><td>F<br>10</td><td>4320<br>3.96</td><td>4.87<br>0</td><td>F<br>10</td><td>5984<br>2.86</td><td>0.01<br>0.29</td></tr><tr><td>Section 4.1.8</td><td>F<br>10</td><td>4236<br>3.79</td><td>0.01<br>9.52</td><td>F<br>10</td><td>4628<br>3.47</td><td>2.66<br>0.03</td><td>F<br>10</td><td>5856<br>2.74</td><td>0.19<br>0.27</td></tr><tr><td>Section 4.1.9</td><td>F<br>10</td><td>4212<br>3.70</td><td>N/A<br>0</td><td>F<br>10</td><td>4312<br>3.61</td><td>N/A<br>0</td><td>F<br>10</td><td>5792<br>2.69</td><td>0.01<br>10</td></tr><tr><td>Section 4.1.10</td><td>F<br>10</td><td>4212<br>2.42</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>F<br>10</td><td>1344<br>7.58</td><td>N/A<br>0</td></tr><tr><td>Section 4.1.11</td><td>F<br>10</td><td>4216<br>6.17</td><td>N/A<br>0</td><td>F<br>10</td><td>6804<br>3.83</td><td>N/A<br>0</td><td>F<br>10</td><td>N/A<br>0</td><td>0.23<br>10</td></tr></tbody></table>

<table><caption>**Table 7** Scores for the C track</caption><thead><tr><th>Rank name</th><th>Team score</th><th>Correctness score</th><th>Overhead score</th><th>Memory score</th><th>Total score</th></tr></thead><tbody><tr><td>1</td><td>RITHM-1</td><td>110</td><td>78.19</td><td>73.72</td><td>261.92</td></tr><tr><td>2</td><td>E- ACSL</td><td>100</td><td>50.19</td><td>68.97</td><td>219.16</td></tr><tr><td>3</td><td>RTC</td><td>70</td><td>20.70</td><td>17.31</td><td>108.01</td></tr></tbody></table>

<figure><img src="image_10.png" /><figcaption>**Fig. 5** Graphical representation of the scores for the C track</figcaption></figure>

## 6.3 Scores for the offline track

The detailed scores for the offline track are presented in Table 10.

The final scores of the offline track are reported in Table 11 and can be visualized in Fig. 7. The final ranking of the teams is: first is QEA, second is MONPOLY, third is RITHM, fourth is STEPR.

As one can observe in Table 11, there is not much difference in terms of correctness score between the three first tools. There is, however, a noticeable difference between each of the three first tools in terms of global score. One can also notice that the difference between QEA and MONPOLY was made on the overhead score.
<table><caption>**Table 6** Detailed scores for the C track</caption><thead><tr><th rowspan="3">Reference to benchmark description</th><th colspan="3">RITHM</th><th colspan="3">E- ACSL</th><th colspan="3">RTC</th></tr><tr><th>Verdict</th><th>Mem (MB)</th><th>Ovhd (s)</th><th>Verdict</th><th>Mem (MB)</th><th>Ovhd (s)</th><th>Verdict</th><th>Mem (MB)</th><th>Ovhd (s)</th></tr><tr><th>v-score</th><th>m-score</th><th>o-score</th><th>v-score</th><th>m-score</th><th>o-score</th><th>v-score</th><th>m-score</th><th>o-score</th></tr></thead><tbody><tr><td>Section 4.1.1</td><td>F<br>10</td><td>1012756<br>10</td><td>0.68<br>10</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td></tr><tr><td>Section 4.1.2</td><td>F<br>10</td><td>1012756<br>10</td><td>0.68<br>10</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td></tr><tr><td>Section 4.1.3</td><td>F<br>10</td><td>614168<br>10</td><td>0.42<br>10</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td></tr><tr><td>Section 4.1.4</td><td>F<br>10</td><td>614168<br>10</td><td>0.42<br>10</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td></tr><tr><td>Section 4.1.5</td><td>F<br>10</td><td>647696<br>10</td><td>0.69<br>10</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td></tr><tr><td>Section 4.1.6</td><td>F<br>10</td><td>11916<br>4.46</td><td>0.01<br>9.59</td><td>F<br>10</td><td>12980<br>4.10</td><td>0.30<br>0.16</td><td>F<br>10</td><td>37040<br>1.44</td><td>0.19<br>0.14</td></tr><tr><td>Section 4.1.7</td><td>F<br>10</td><td>5388<br>3.18</td><td>0.001<br>9.09</td><td>F<br>10</td><td>4320<br>3.96</td><td>4.87<br>0</td><td>F<br>10</td><td>5984<br>2.86</td><td>0.01<br>0.29</td></tr><tr><td>Section 4.1.8</td><td>F<br>10</td><td>4236<br>3.79</td><td>0.01<br>9.52</td><td>F<br>10</td><td>4628<br>3.47</td><td>2.66<br>0.03</td><td>F<br>10</td><td>5856<br>2.74</td><td>0.19<br>0.27</td></tr><tr><td>Section 4.1.9</td><td>F<br>10</td><td>4212<br>3.70</td><td>N/A<br>0</td><td>F<br>10</td><td>4312<br>3.61</td><td>N/A<br>0</td><td>F<br>10</td><td>5792<br>2.69</td><td>0.01<br>10</td></tr><tr><td>Section 4.1.10</td><td>F<br>10</td><td>4212<br>2.42</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>N/A<br>0</td><td>F<br>10</td><td>1344<br>7.58</td><td>N/A<br>0</td></tr><tr><td>Section 4.1.11</td><td>F<br>10</td><td>4216<br>6.17</td><td>N/A<br>0</td><td>F<br>10</td><td>6804<br>3.83</td><td>N/A<br>0</td><td>F<br>10</td><td>N/A<br>0</td><td>0.23<br>10</td></tr></tbody></table>

<table><caption>**Table 7** Scores for the C track</caption><thead><tr><th>Rank name</th><th>Team score</th><th>Correctness score</th><th>Overhead score</th><th>Memory score</th><th>Total score</th></tr></thead><tbody><tr><td>1</td><td>RITHM-1</td><td>110</td><td>78.19</td><td>73.72</td><td>261.92</td></tr><tr><td>2</td><td>E- ACSL</td><td>100</td><td>50.19</td><td>68.97</td><td>219.16</td></tr><tr><td>3</td><td>RTC</td><td>70</td><td>20.70</td><td>17.31</td><td>108.01</td></tr></tbody></table>

<figure><img src="image_9.png" /><figcaption>**Fig. 5** Graphical representation of the scores for the C track</figcaption></figure>

## 6.3 Scores for the offline track

The detailed scores for the offline track are presented in Table 10.

The final scores of the offline track are reported in Table 11 and can be visualized in Fig. 7. The final ranking of the teams is: first is QEA, second is MONPOLY, third is RITHM, fourth is STEPR.

As one can observe in Table 11, there is not much difference in terms of correctness score between the three first tools. There is, however, a noticeable difference between each of the three first tools in terms of global score. One can also notice that the difference between QEA and MONPOLY was made on the overhead score.

<figure><img src="image_10.png" /></figure>
<table><caption>**Table 8** Detailed scores for the Java track</caption><thead><tr><th rowspan="2">Reference to benchmark description</th><th colspan="3">LARVA</th><th colspan="3">JUnit<sup>RV</sup></th><th colspan="3">JAVAMOP</th><th colspan="3">QEA</th></tr><tr><th>Verdict v-score</th><th>Mem (MB) m-score</th><th>Ovhd (s) o-score</th><th>Verdict v-score</th><th>Mem (MB) m-score</th><th>Ovhd (s) o-score</th><th>Verdict v-score</th><th>Mem (MB) m-score</th><th>Ovhd (s) o-score</th><th>Verdict v-score</th><th>Mem (MB) m-score</th><th>Ovhd (s) o-score</th></tr></thead><tbody><tr><td>Section 4.2.1</td><td>F</td><td>0.55</td><td>1.54</td><td>F</td><td>1.92</td><td>6.08</td><td>F</td><td>1.94</td><td>0.17</td><td>F</td><td>2.65</td><td>0.20</td></tr><tr><td></td><td>10</td><td>1.95</td><td>2.66</td><td>10</td><td>2.70</td><td>0.14</td><td>10</td><td>2.68</td><td>4.96</td><td>10</td><td>1.96</td><td>4.35</td></tr><tr><td>Section 4.2.2</td><td>F</td><td>0.58</td><td>1.56</td><td>F</td><td>7.75</td><td>6.86</td><td>F</td><td>2.59</td><td>0.21</td><td>F</td><td>2.70</td><td>0.18</td></tr><tr><td></td><td>10</td><td>2.60</td><td>3.03</td><td>10</td><td>1.02</td><td>0.13</td><td>10</td><td>3.04</td><td>4.33</td><td>10</td><td>2.92</td><td>4.96</td></tr><tr><td>Section 4.2.3</td><td>F</td><td>0.66</td><td>1.56</td><td>F</td><td>1.92</td><td>3.74</td><td>F</td><td>9.03</td><td>0.22</td><td>F</td><td>5.24</td><td>0.24</td></tr><tr><td></td><td>10</td><td>4.54</td><td>2.11</td><td>10</td><td>4.99</td><td>0.28</td><td>10</td><td>1.06</td><td>4.66</td><td>10</td><td>1.83</td><td>4.40</td></tr><tr><td>Section 4.2.4</td><td>F</td><td>0.69</td><td>1.56</td><td>F</td><td>1.92</td><td>8.63</td><td>F</td><td>9.04</td><td>0.32</td><td>F</td><td>2.00</td><td>0.18</td></tr><tr><td></td><td>10</td><td>9.05</td><td>0.89</td><td>10</td><td>4.20</td><td>0.12</td><td>10</td><td>0.89</td><td>3.35</td><td>10</td><td>4.02</td><td>5.84</td></tr><tr><td>Section 4.2.5</td><td>F</td><td>0.95</td><td>1.57</td><td>F</td><td>1.92</td><td>8.57</td><td>F</td><td>9.69</td><td>0.73</td><td>F</td><td>2.64</td><td>0.22</td></tr><tr><td></td><td>10</td><td>10.97</td><td>0.83</td><td>10</td><td>4.76</td><td>0.17</td><td>10</td><td>0.94</td><td>2.05</td><td>10</td><td>3.46</td><td>6.83</td></tr><tr><td>Section 4.2.6</td><td>T</td><td>0.59</td><td>1.57</td><td>T</td><td>27.94</td><td>1.56</td><td>T</td><td>1.94</td><td>0.20</td><td>T</td><td>3.30</td><td>0.23</td></tr><tr><td></td><td>10</td><td>5.16</td><td>1.85</td><td>10</td><td>0.34</td><td>0.59</td><td>10</td><td>4.92</td><td>4.70</td><td>10</td><td>2.89</td><td>4.11</td></tr><tr><td>Section 4.2.7</td><td>T</td><td>0.65</td><td>1.58</td><td>T</td><td>308.67</td><td>22.93</td><td>T</td><td>1.94</td><td>0.20</td><td>T</td><td>2.65</td><td>0.25</td></tr><tr><td></td><td>10</td><td>7.10</td><td>1.36</td><td>10</td><td>0.03</td><td>0.04</td><td>10</td><td>4.97</td><td>5.19</td><td>10</td><td>3.64</td><td>4.12</td></tr><tr><td>Section 4.2.8</td><td>T</td><td>0.05</td><td>2173.26</td><td>T</td><td>244.27</td><td>49.94</td><td>T</td><td>32.24</td><td>26.27</td><td>T</td><td>5.85</td><td>25.99</td></tr><tr><td></td><td>10</td><td>162.39</td><td>0.29</td><td>10</td><td>0.19</td><td>2.06</td><td>10</td><td>1.46</td><td>3.92</td><td>10</td><td>8.06</td><td>3.97</td></tr><tr><td>Section 4.2.9</td><td>T</td><td>0.64</td><td>1.55</td><td>T</td><td>291.57</td><td>24.79</td><td>T</td><td>1.94</td><td>0.20</td><td>T</td><td>4.59</td><td>0.23</td></tr><tr><td></td><td>10</td><td>5.16</td><td>2.08</td><td>10</td><td>0.04</td><td>0.04</td><td>10</td><td>5.55</td><td>4.98</td><td>10</td><td>2.34</td><td>4.34</td></tr><tr><td>Section 4.2.10</td><td>T</td><td>1.13</td><td>1.56</td><td>T</td><td>680.19</td><td>100.57</td><td>T</td><td>2.58</td><td>0.24</td><td>T</td><td>110.33</td><td>1.26</td></tr><tr><td></td><td>10</td><td>7.76</td><td>2.45</td><td>10</td><td>0.03</td><td>0.02</td><td>10</td><td>7.35</td><td>7.45</td><td>10</td><td>0.17</td><td>1.40</td></tr><tr><td>Section 4.2.11</td><td>F</td><td>0.10</td><td>48.06</td><td>F</td><td>N/A</td><td>2.98</td><td>F</td><td>5.17</td><td>0.79</td><td>F</td><td>4.53</td><td>2.04</td></tr><tr><td></td><td>10</td><td>40.93</td><td>0.56</td><td>10</td><td>0</td><td>1.59</td><td>10</td><td>4.41</td><td>5.99</td><td>10</td><td>5.04</td><td>2.32</td></tr></tbody></table>
<table><caption>**Table 8** Detailed scores for the Java track</caption><thead><tr><th rowspan="2">Reference to benchmark description</th><th colspan="3">LARVA</th><th colspan="3">JUnit<sup>RV</sup></th><th colspan="3">JAVAMOP</th><th colspan="3">QEA</th></tr><tr><th>Verdict v-score</th><th>Mem (MB) m-score</th><th>Ovhd (s) o-score</th><th>Verdict v-score</th><th>Mem (MB) m-score</th><th>Ovhd (s) o-score</th><th>Verdict v-score</th><th>Mem (MB) m-score</th><th>Ovhd (s) o-score</th><th>Verdict v-score</th><th>Mem (MB) m-score</th><th>Ovhd (s) o-score</th></tr></thead><tbody><tr><td>Section 4.2.1</td><td>F</td><td>0.55</td><td>1.54</td><td>F</td><td>1.92</td><td>6.08</td><td>F</td><td>1.94</td><td>0.17</td><td>F</td><td>2.65</td><td>0.20</td></tr><tr><td></td><td>10</td><td>1.95</td><td>2.66</td><td>10</td><td>2.70</td><td>0.14</td><td>10</td><td>2.68</td><td>4.96</td><td>10</td><td>1.96</td><td>4.35</td></tr><tr><td>Section 4.2.2</td><td>F</td><td>0.58</td><td>1.56</td><td>F</td><td>7.75</td><td>6.86</td><td>F</td><td>2.59</td><td>0.21</td><td>F</td><td>2.70</td><td>0.18</td></tr><tr><td></td><td>10</td><td>2.60</td><td>3.03</td><td>10</td><td>1.02</td><td>0.13</td><td>10</td><td>3.04</td><td>4.33</td><td>10</td><td>2.92</td><td>4.96</td></tr><tr><td>Section 4.2.3</td><td>F</td><td>0.66</td><td>1.56</td><td>F</td><td>1.92</td><td>3.74</td><td>F</td><td>9.03</td><td>0.22</td><td>F</td><td>5.24</td><td>0.24</td></tr><tr><td></td><td>10</td><td>4.54</td><td>2.11</td><td>10</td><td>4.99</td><td>0.28</td><td>10</td><td>1.06</td><td>4.66</td><td>10</td><td>1.83</td><td>4.40</td></tr><tr><td>Section 4.2.4</td><td>F</td><td>0.69</td><td>1.56</td><td>F</td><td>1.92</td><td>8.63</td><td>F</td><td>9.04</td><td>0.32</td><td>F</td><td>2.00</td><td>0.18</td></tr><tr><td></td><td>10</td><td>9.05</td><td>0.89</td><td>10</td><td>4.20</td><td>0.12</td><td>10</td><td>0.89</td><td>3.35</td><td>10</td><td>4.02</td><td>5.84</td></tr><tr><td>Section 4.2.5</td><td>F</td><td>0.95</td><td>1.57</td><td>F</td><td>1.92</td><td>8.57</td><td>F</td><td>9.69</td><td>0.73</td><td>F</td><td>2.64</td><td>0.22</td></tr><tr><td></td><td>10</td><td>10.97</td><td>0.83</td><td>10</td><td>4.76</td><td>0.17</td><td>10</td><td>0.94</td><td>2.05</td><td>10</td><td>3.46</td><td>6.83</td></tr><tr><td>Section 4.2.6</td><td>T</td><td>0.59</td><td>1.57</td><td>T</td><td>27.94</td><td>1.56</td><td>T</td><td>1.94</td><td>0.20</td><td>T</td><td>3.30</td><td>0.23</td></tr><tr><td></td><td>10</td><td>5.16</td><td>1.85</td><td>10</td><td>0.34</td><td>0.59</td><td>10</td><td>4.92</td><td>4.70</td><td>10</td><td>2.89</td><td>4.11</td></tr><tr><td>Section 4.2.7</td><td>T</td><td>0.65</td><td>1.58</td><td>T</td><td>308.67</td><td>22.93</td><td>T</td><td>1.94</td><td>0.20</td><td>T</td><td>2.65</td><td>0.25</td></tr><tr><td></td><td>10</td><td>7.10</td><td>1.36</td><td>10</td><td>0.03</td><td>0.04</td><td>10</td><td>4.97</td><td>5.19</td><td>10</td><td>3.64</td><td>4.12</td></tr><tr><td>Section 4.2.8</td><td>T</td><td>0.05</td><td>2173.26</td><td>T</td><td>244.27</td><td>49.94</td><td>T</td><td>32.24</td><td>26.27</td><td>T</td><td>5.85</td><td>25.99</td></tr><tr><td></td><td>10</td><td>162.39</td><td>0.29</td><td>10</td><td>0.19</td><td>2.06</td><td>10</td><td>1.46</td><td>3.92</td><td>10</td><td>8.06</td><td>3.97</td></tr><tr><td>Section 4.2.9</td><td>T</td><td>0.64</td><td>1.55</td><td>T</td><td>291.57</td><td>24.79</td><td>T</td><td>1.94</td><td>0.20</td><td>T</td><td>4.59</td><td>0.23</td></tr><tr><td></td><td>10</td><td>5.16</td><td>2.08</td><td>10</td><td>0.04</td><td>0.04</td><td>10</td><td>5.55</td><td>4.98</td><td>10</td><td>2.34</td><td>4.34</td></tr><tr><td>Section 4.2.10</td><td>T</td><td>1.13</td><td>1.56</td><td>T</td><td>680.19</td><td>100.57</td><td>T</td><td>2.58</td><td>0.24</td><td>T</td><td>110.33</td><td>1.26</td></tr><tr><td></td><td>10</td><td>7.76</td><td>2.45</td><td>10</td><td>0.03</td><td>0.02</td><td>10</td><td>7.35</td><td>7.45</td><td>10</td><td>0.17</td><td>1.40</td></tr><tr><td>Section 4.2.11</td><td>F</td><td>0.10</td><td>48.06</td><td>F</td><td>N/A</td><td>2.98</td><td>F</td><td>5.17</td><td>0.79</td><td>F</td><td>4.53</td><td>2.04</td></tr><tr><td></td><td>10</td><td>40.93</td><td>0.56</td><td>10</td><td>0</td><td>1.59</td><td>10</td><td>4.41</td><td>5.99</td><td>10</td><td>5.04</td><td>2.32</td></tr></tbody></table>
<table><caption>**Table 8 continued**</caption><thead><tr><th rowspan="2">Reference to benchmark description</th><th colspan="3">LARVA</th><th colspan="3">jUnit<sup>RV</sup></th><th colspan="3">JAVAMOP</th><th colspan="3">QEA</th></tr><tr><th>Verdict v-score</th><th>Mem (MB) m-score</th><th>Ovhd (s) o-score</th><th>Verdict v-score</th><th>Mem (MB) m-score</th><th>Ovhd (s) o-score</th><th>Verdict v-score</th><th>Mem (MB) m-score</th><th>Ovhd (s) o-score</th><th>Verdict v-score</th><th>Mem (MB) m-score</th><th>Ovhd (s) o-score</th></tr></thead><tbody><tr><td>Section 4.2.12</td><td>N/A</td><td>N/A</td><td>N/A</td><td>F</td><td>N/A</td><td>0.51</td><td>F</td><td>5.81</td><td>2.23</td><td>F</td><td>8.41</td><td>3.24</td></tr><tr><td>Section 4.2.13</td><td>0</td><td>0</td><td>0</td><td>10</td><td>0</td><td>7.21</td><td>10</td><td>5.91</td><td>1.65</td><td>10</td><td>4.09</td><td>1.14</td></tr><tr><td>Section 4.2.14</td><td>F</td><td>0.10</td><td>35.78</td><td>F</td><td>N/A</td><td>0.36</td><td>F</td><td>7.10</td><td>25.22</td><td>F</td><td>5.20</td><td>25.33</td></tr><tr><td>Section 4.2.15</td><td>10</td><td>3.87</td><td>4.37</td><td>10</td><td>0</td><td>9.63</td><td>10</td><td>2.38</td><td>0.14</td><td>10</td><td>3.25</td><td>0.14</td></tr><tr><td>Section 4.2.16</td><td>10</td><td>2.58</td><td>3.57</td><td>10</td><td>0</td><td>0.55</td><td>10</td><td>3.57</td><td>4.94</td><td>10</td><td>2.86</td><td>3.95</td></tr><tr><td>Section 4.2.17</td><td>F</td><td>0.03</td><td>2606.58</td><td>F</td><td>N/A</td><td>7.58</td><td>F</td><td>647.19</td><td>87.00</td><td>F</td><td>837.29</td><td>190.89</td></tr><tr><td>Section 4.2.18</td><td>10</td><td>841.28</td><td>3.03</td><td>10</td><td>0</td><td>8.85</td><td>10</td><td>3.93</td><td>0.77</td><td>10</td><td>3.04</td><td>0.35</td></tr><tr><td>Section 4.2.19</td><td>10</td><td>0.06</td><td>15393.22</td><td>T</td><td>N/A</td><td>0</td><td>F</td><td>1001.69</td><td>164.00</td><td>F</td><td>829.59</td><td>217.27</td></tr><tr><td>Section 4.2.20</td><td>10</td><td>721.39</td><td>3.86</td><td>-5</td><td>0</td><td>0</td><td>10</td><td>2.78</td><td>5.66</td><td>10</td><td>3.36</td><td>4.28</td></tr><tr><td>Section 4.2.21</td><td>10</td><td>0</td><td>N/A</td><td>T</td><td>717.92</td><td>88.35</td><td>T</td><td>801.15</td><td>242.00</td><td>T</td><td>844.54</td><td>288.08</td></tr><tr><td>Section 4.2.22</td><td>10</td><td>0</td><td>N/A</td><td>T</td><td>3.64</td><td>5.98</td><td>10</td><td>3.26</td><td>2.18</td><td>10</td><td>3.10</td><td>1.83</td></tr><tr><td>Section 4.2.23</td><td>10</td><td>267.43</td><td>0</td><td>10</td><td>697.42</td><td>113.63</td><td>T</td><td>795.49</td><td>237.00</td><td>T</td><td>819.92</td><td>889.63</td></tr><tr><td>Section 4.2.24</td><td>10</td><td>160.62</td><td>2.18</td><td>10</td><td>4.06</td><td>6.22</td><td>10</td><td>3.21</td><td>2.98</td><td>10</td><td>3.12</td><td>0.79</td></tr><tr><td>Section 4.2.25</td><td>10</td><td>0</td><td>6882.58</td><td>T</td><td>300.2</td><td>49.9</td><td>T</td><td>309.00</td><td>94.00</td><td>F</td><td>820.52</td><td>170.31</td></tr><tr><td>Section 4.2.26</td><td>10</td><td>0</td><td>N/A</td><td>F</td><td>0.16</td><td>27.22</td><td>F</td><td>3.68</td><td>5.58</td><td>6.44</td><td>4.42</td><td>3.56</td></tr><tr><td>Section 4.2.27</td><td>10</td><td>135.98</td><td>1.08</td><td>10</td><td>0</td><td>1.22</td><td>10</td><td>2.53</td><td>1.42</td><td>10</td><td>6.39</td><td>7.20</td></tr><tr><td>Section 4.2.28</td><td>10</td><td>0.29</td><td>70.12</td><td>T</td><td>86.04</td><td>8.8</td><td>T</td><td>267.45</td><td>5.64</td><td>T</td><td>142.74</td><td>5.29</td></tr><tr><td>Section 4.2.29</td><td>10</td><td>0</td><td>2.24</td><td>10</td><td>2.00</td><td>0.55</td><td>10</td><td>1.31</td><td>3.59</td><td>10</td><td>2.45</td><td>3.82</td></tr><tr><td>Section 4.2.30</td><td>10</td><td>0</td><td>N/A</td><td>F</td><td>0</td><td>1.45</td><td>10</td><td>4.19</td><td>2.67</td><td>10</td><td>5.81</td><td>5.88</td></tr></tbody></table>

<figure><img src="image_11.png" /></figure>
<table><caption>**Table 8** continued</caption><thead><tr><th rowspan="2">Reference to benchmark description</th><th colspan="3">LARVA</th><th colspan="3">jUnit<sup>RV</sup></th><th colspan="3">JAVAMOP</th><th colspan="3">QEA</th></tr><tr><th>Verdict v-score</th><th>Mem (MB) m-score</th><th>Ovhd (s) o-score</th><th>Verdict v-score</th><th>Mem (MB) m-score</th><th>Ovhd (s) o-score</th><th>Verdict v-score</th><th>Mem (MB) m-score</th><th>Ovhd (s) o-score</th><th>Verdict v-score</th><th>Mem (MB) m-score</th><th>Ovhd (s) o-score</th></tr></thead><tbody><tr><td>Section 4.2.12</td><td>N/A</td><td>N/A</td><td>N/A</td><td>F</td><td>N/A</td><td>0.51</td><td>F</td><td>5.81</td><td>2.23</td><td>F</td><td>8.41</td><td>3.24</td></tr><tr><td>Section 4.2.13</td><td>0</td><td>0</td><td>0</td><td>10</td><td>0</td><td>7.21</td><td>10</td><td>5.91</td><td>1.65</td><td>10</td><td>4.09</td><td>1.14</td></tr><tr><td>Section 4.2.14</td><td>F</td><td>0.10</td><td>35.78</td><td>F</td><td>N/A</td><td>0.36</td><td>F</td><td>7.10</td><td>25.22</td><td>F</td><td>5.20</td><td>25.33</td></tr><tr><td>Section 4.2.15</td><td>10</td><td>3.87</td><td>4.37</td><td>10</td><td>0</td><td>9.63</td><td>10</td><td>2.38</td><td>0.14</td><td>10</td><td>3.25</td><td>0.14</td></tr><tr><td>Section 4.2.16</td><td>10</td><td>2.58</td><td>3.57</td><td>10</td><td>0</td><td>0.55</td><td>10</td><td>3.57</td><td>4.94</td><td>10</td><td>2.86</td><td>3.95</td></tr><tr><td>Section 4.2.17</td><td>F</td><td>0.03</td><td>2606.58</td><td>F</td><td>N/A</td><td>7.58</td><td>F</td><td>647.19</td><td>87.00</td><td>F</td><td>837.29</td><td>190.89</td></tr><tr><td>Section 4.2.18</td><td>10</td><td>841.28</td><td>3.03</td><td>10</td><td>0</td><td>8.85</td><td>10</td><td>3.93</td><td>0.77</td><td>10</td><td>3.04</td><td>0.35</td></tr><tr><td>Section 4.2.19</td><td>10</td><td>0.06</td><td>15393.22</td><td>T</td><td>N/A</td><td>0</td><td>F</td><td>1001.69</td><td>164.00</td><td>F</td><td>829.59</td><td>217.27</td></tr><tr><td>Section 4.2.20</td><td>T/O</td><td>721.39</td><td>3.86</td><td>-5</td><td>0</td><td>0</td><td>10</td><td>2.78</td><td>5.66</td><td>10</td><td>3.36</td><td>4.28</td></tr><tr><td>Section 4.2.21</td><td>-5</td><td>N/A</td><td>N/A</td><td>T</td><td>717.92</td><td>88.35</td><td>T</td><td>801.15</td><td>242.00</td><td>T</td><td>844.54</td><td>288.08</td></tr><tr><td>Section 4.2.22</td><td>T/O</td><td>0</td><td>N/A</td><td>T</td><td>697.42</td><td>5.98</td><td>10</td><td>3.26</td><td>2.18</td><td>10</td><td>3.10</td><td>1.83</td></tr><tr><td>Section 4.2.23</td><td>T</td><td>0</td><td>N/A</td><td>T</td><td>697.42</td><td>113.63</td><td>T</td><td>795.49</td><td>237.00</td><td>T</td><td>819.92</td><td>889.63</td></tr><tr><td>Section 4.2.24</td><td>10</td><td>160.62</td><td>2.18</td><td>10</td><td>4.06</td><td>6.22</td><td>10</td><td>3.21</td><td>2.98</td><td>10</td><td>3.12</td><td>0.79</td></tr><tr><td>Section 4.2.25</td><td>10</td><td>267.43</td><td>2.24</td><td>10</td><td>2.00</td><td>0</td><td>N/A</td><td>649.83</td><td>94.00</td><td>F</td><td>820.52</td><td>170.31</td></tr><tr><td>Section 4.2.26</td><td>N/A</td><td>N/A</td><td>N/A</td><td>T</td><td>N/A</td><td>-5</td><td>0</td><td>0</td><td>6.44</td><td>10</td><td>4.42</td><td>3.56</td></tr><tr><td>Section 4.2.27</td><td>F</td><td>0.16</td><td>27.22</td><td>F</td><td>N/A</td><td>3.68</td><td>F</td><td>58.27</td><td>3.16</td><td>F</td><td>23.07</td><td>0.62</td></tr><tr><td>Section 4.2.28</td><td>10</td><td>135.98</td><td>1.08</td><td>10</td><td>0</td><td>1.22</td><td>10</td><td>2.53</td><td>1.42</td><td>10</td><td>6.39</td><td>7.20</td></tr><tr><td>Section 4.2.29</td><td>T</td><td>0.29</td><td>70.12</td><td>T</td><td>86.04</td><td>8.8</td><td>T</td><td>267.45</td><td>5.64</td><td>T</td><td>142.74</td><td>5.29</td></tr><tr><td>Section 4.2.30</td><td>10</td><td>160.62</td><td>2.18</td><td>10</td><td>4.06</td><td>2.30</td><td>10</td><td>1.31</td><td>3.59</td><td>10</td><td>2.45</td><td>3.82</td></tr><tr><td>Section 4.2.31</td><td>T</td><td>0</td><td>6882.58</td><td>T</td><td>300.2</td><td>49.9</td><td>T</td><td>309.00</td><td>6.08</td><td>T</td><td>156.66</td><td>5.59</td></tr><tr><td>Section 4.2.32</td><td>10</td><td>267.43</td><td>2.24</td><td>10</td><td>2.00</td><td>0.55</td><td>10</td><td>1.94</td><td>4.53</td><td>10</td><td>3.82</td><td>4.92</td></tr><tr><td>Section 4.2.33</td><td>0</td><td>0</td><td>0</td><td>10</td><td>0</td><td>1.45</td><td>10</td><td>4.19</td><td>2.67</td><td>10</td><td>5.81</td><td>5.88</td></tr></tbody></table>

<figure><img src="image_11.png" /></figure>
<table><caption>**Table 9** Scores for the Java track</caption><thead><tr><th>Rank</th><th>Team name</th><th>Correctness score</th><th>Overhead score</th><th>Memory score</th><th>Total score</th></tr></thead><tbody><tr><td>1</td><td>QEA</td><td>230</td><td>84.50</td><td>82.01</td><td>396.51</td></tr><tr><td>1</td><td>JAVAMOP</td><td>230</td><td>88.56</td><td>77.89</td><td>396.45</td></tr><tr><td>2</td><td>JUNIT<sup>RV</sup></td><td>200</td><td>49.15</td><td>31.67</td><td>280.82</td></tr><tr><td>3</td><td>LARVA</td><td>165</td><td>7.79</td><td>38.43</td><td>211.22</td></tr></tbody></table>

<figure><img src="image_12.png" /><figcaption>**Fig. 6** Graphical representation of the scores for the Java track</figcaption></figure>

## 7 Lessons learned and discussion

*Comparison with other competitions* Over the past fifteen years, the arise of several software tool competitions [2,21,54,55,59,84] has deeply contributed to advance the state of the art in the computer-aided verification technology. The international SAT solver competition [59] is a pioneer example with a long track record of editions starting from 2002. The aim of this competition is to determine as quickly as possible whether a boolean formula expressed in conjunctive normal form (CNF) is satisfiable or not. If the formula is satisfiable, the tool should return also a correct assignment. If the returned assignment is incorrect, the tool is disqualified. The organisers provide three different categories of benchmarks: industrial, crafted and random benchmarks. The performance is evaluated by measuring the CPU time necessary for each tool to return an answer. In the recent editions, the organisers provide also a wall-clock time within which a tool can use all the available resources (for example multiple cores) to provide the correct answer. In SAT competition, the jury is the responsible of choosing the final benchmarks. This is different in CRV where each team can provide up to five benchmarks to challenge the other teams, highlighting the bottlenecks of the other teams' tools. Furthermore, during the CRV training phase each team has the possibility to improve the development of their tools using new benchmarks that were not considered before.

The success of the SAT competitions has inspired other initiatives such as the Satisfiability Modulo Theories Competitions (SMT-COMP) [2] started in 2005. The challenge of

SMT-COMP is to efficiently check the satisfiability of first-order formula modulo a background theory. In this case, the chosen theory strictly depends on the nature of the problem to consider (i.e., arrays, bit-vectors, uninterpreted functions, etc.). A major challenge for the SMT community has been to devise a common input language for their tools that could accommodate different theories and to express their syntax and semantics. This goal was achieved in 2004 with the release of SMT-LIB a standard input language that is now used as common format for the selected benchmarks in SMT-COMP.

One important difference of CRV with SMT-COMP and the SAT competition is the lack of a common input language for the participating tools. In CRV, a benchmark unit includes a program or a trace and a property to be monitored. Properties can be expressed using different formal specification languages more or less expressive and computationally complex to be monitored. The interplay between the allowed expressiveness and the monitoring complexity plays an important role in CRV competition. Some tools may result extremely efficient in detecting simple temporal behaviors, but then they may lack the necessary support to detect more complex properties and vice versa. One of the open challenges for CRV remains the possibility to have a common formal specification language that is general enough to express all the other common formal specification languages used in the RV community.

In the area of software verification, there are three related competitions that have been recently introduced: SV-COMP [21], VerifyThis [55] and RERS Challenge [54]. SV-COMP initiated in 2011 within TACAS [1] community with the aim to compare tools for software model checking. Benchmarks are provided as C programs, while the requirements to check are provided in terms of linear temporal logic formulas. SV-COMP targets tools for the exhaustive exploration of all program behaviors. On the contrary, CRV is dedicated to monitoring tools analyzing only a single program's execution using runtime and offline verification techniques. In SV-COMP the memory utilization is not taken in consideration and the time needed to verify a property does not affect the program execution itself since the verification process is separated from the program execution. The runtime verification tools competing in CRV introduce instead an overhead for the monitored program and they consume memory resources that could affect the execution of the program
<table><caption>**Table 9** Scores for the Java track</caption><thead><tr><th>Rank</th><th>Team name</th><th>Correctness score</th><th>Overhead score</th><th>Memory score</th><th>Total score</th></tr></thead><tbody><tr><td>1</td><td>QEA</td><td>230</td><td>84.50</td><td>82.01</td><td>396.51</td></tr><tr><td>1</td><td>JAVAMOP</td><td>230</td><td>88.56</td><td>77.89</td><td>396.45</td></tr><tr><td>2</td><td>JUNIT<sup>RV</sup></td><td>200</td><td>49.15</td><td>31.67</td><td>280.82</td></tr><tr><td>3</td><td>LARVA</td><td>165</td><td>7.79</td><td>38.43</td><td>211.22</td></tr></tbody></table>

<figure><img src="image_12.png" /><figcaption>**Fig. 6** Graphical representation of the scores for the Java track</figcaption></figure>

## 7 Lessons learned and discussion

*Comparison with other competitions* Over the past fifteen years, the arise of several software tool competitions [2,21,54,55,59,84] has deeply contributed to advance the state of the art in the computer-aided verification technology. The international SAT solver competition [59] is a pioneer example with a long track record of editions starting from 2002. The aim of this competition is to determine as quickly as possible whether a boolean formula expressed in conjunctive normal form (CNF) is satisfiable or not. If the formula is satisfiable, the tool should return also a correct assignment. If the returned assignment is incorrect, the tool is disqualified. The organisers provide three different categories of benchmarks: industrial, crafted and random benchmarks. The performance is evaluated by measuring the CPU time necessary for each tool to return an answer. In the recent editions, the organisers provide also a wall-clock time within which a tool can use all the available resources (for example multiple cores) to provide the correct answer. In SAT competition, the jury is the responsible of choosing the final benchmarks. This is different in CRV where each team can provide up to five benchmarks to challenge the other teams, highlighting the bottlenecks of the other teams' tools. Furthermore, during the CRV training phase each team has the possibility to improve the development of their tools using new benchmarks that were not considered before.

The success of the SAT competitions has inspired other initiatives such as the Satisfiability Modulo Theories Competitions (SMT-COMP) [2] started in 2005. The challenge of

SMT-COMP is to efficiently check the satisfiability of first-order formula modulo a background theory. In this case, the chosen theory strictly depends on the nature of the problem to consider (i.e., arrays, bit-vectors, uninterpreted functions, etc.). A major challenge for the SMT community has been to devise a common input language for their tools that could accommodate different theories and to express their syntax and semantics. This goal was achieved in 2004 with the release of SMT-LIB a standard input language that is now used as common format for the selected benchmarks in SMT-COMP.

One important difference of CRV with SMT-COMP and the SAT competition is the lack of a common input language for the participating tools. In CRV, a benchmark unit includes a program or a trace and a property to be monitored. Properties can be expressed using different formal specification languages more or less expressive and computationally complex to be monitored. The interplay between the allowed expressiveness and the monitoring complexity plays an important role in CRV competition. Some tools may result extremely efficient in detecting simple temporal behaviors, but then they may lack the necessary support to detect more complex properties and vice versa. One of the open challenges for CRV remains the possibility to have a common formal specification language that is general enough to express all the other common formal specification languages used in the RV community.

In the area of software verification, there are three related competitions that have been recently introduced: SV-COMP [21], VerifyThis [55] and RERS Challenge [54]. SV-COMP initiated in 2011 within TACAS [1] community with the aim to compare tools for software model checking. Benchmarks are provided as C programs, while the requirements to check are provided in terms of linear temporal logic formulas. SV-COMP targets tools for the exhaustive exploration of all program behaviors. On the contrary, CRV is dedicated to monitoring tools analyzing only a single program's execution using runtime and offline verification techniques. In SV-COMP the memory utilization is not taken in consideration and the time needed to verify a property does not affect the program execution itself since the verification process is separated from the program execution. The runtime verification tools competing in CRV introduce instead an overhead for the monitored program and they consume memory resources that could affect the execution of the program
<table><caption>**Table 10** Detailed scores for the offline track</caption><thead><tr><th rowspan="3">Reference to benchmark description</th><th colspan="2">RITHM</th><th colspan="2">MonPoly</th><th colspan="2">STEPR</th><th colspan="4">QEA</th></tr><tr><th>Verdict v-score</th><th>Mem (MB) m-score</th><th>Ovhd (s) o-score</th><th>Verdict v-score</th><th>Mem (MB) m-score</th><th>Ovhd (s) o-score</th><th>Verdict v-score</th><th>Mem (MB) m-score</th><th>Ovhd (s) o-score</th><th>Verdict v-score</th><th>Mem (MB) m-score</th><th>Ovhd (s) o-score</th></tr></thead><tbody><tr><td>Section 4.3.1</td><td>F</td><td>993</td><td>0.60</td><td>F</td><td>13</td><td>0.13</td><td>F</td><td>29.53</td><td>0.90</td><td>F</td><td>4.535</td><td>0.24</td></tr><tr><td>Section 4.3.2</td><td>F</td><td>993</td><td>1.12</td><td>10</td><td>2.31</td><td>5.32</td><td>10</td><td>1.02</td><td>0.75</td><td>10</td><td>6.64</td><td>2.81</td></tr><tr><td>Section 4.3.3</td><td>F</td><td>614</td><td>7.67</td><td>10</td><td>1228</td><td>8.40</td><td>F</td><td>645.17</td><td>8.87</td><td>F</td><td>33.30</td><td>3.58</td></tr><tr><td>Section 4.3.4</td><td>F</td><td>614</td><td>0.63</td><td>10</td><td>2.32</td><td>5.41</td><td>10</td><td>0.97</td><td>0.68</td><td>10</td><td>6.66</td><td>3.28</td></tr><tr><td>Section 4.3.5</td><td>F</td><td>614</td><td>0.98</td><td>F</td><td>1696</td><td>15.80</td><td>F</td><td>622.30</td><td>21.10</td><td>F</td><td>517.07</td><td>12.22</td></tr><tr><td>Section 4.3.6</td><td>F</td><td>628</td><td>0.99</td><td>F</td><td>544</td><td>5.09</td><td>F</td><td>274.29</td><td>7.77</td><td>F</td><td>32.94</td><td>3.71</td></tr><tr><td>Section 4.3.7</td><td>N/A</td><td>0.43</td><td>6.29</td><td>10</td><td>0.49</td><td>1.24</td><td>10</td><td>0.97</td><td>0.80</td><td>10</td><td>8.11</td><td>1.68</td></tr><tr><td>Section 4.3.8</td><td>N/A</td><td>0</td><td>N/A</td><td>10</td><td>1.25</td><td>0.41</td><td>10</td><td>0.07</td><td>0.06</td><td>10</td><td>8.68</td><td>0.26</td></tr><tr><td>Section 4.3.9</td><td>N/A</td><td>0</td><td>N/A</td><td>10</td><td>20</td><td>1.33</td><td>F</td><td>255.48</td><td>96.00</td><td>F</td><td>4.53</td><td>9.53</td></tr><tr><td>Section 4.3.10</td><td>N/A</td><td>0</td><td>N/A</td><td>10</td><td>1.82</td><td>1.56</td><td>10</td><td>0.14</td><td>0.02</td><td>10</td><td>8.04</td><td>8.42</td></tr><tr><td>Section 4.3.11</td><td>T</td><td>14.27</td><td>5.40</td><td>T</td><td>370</td><td>33.51</td><td>F</td><td>706.26</td><td>21.41</td><td>F</td><td>7.75</td><td>0.29</td></tr><tr><td>Section 4.3.12</td><td>F</td><td>14.27</td><td>2.65</td><td>10</td><td>4.92</td><td>2.84</td><td>10</td><td>0.10</td><td>1.32</td><td>10</td><td>0.50</td><td>3.18</td></tr><tr><td>Section 4.3.13</td><td>F</td><td>14.27</td><td>7.20</td><td>F</td><td>13.00</td><td>0.80</td><td>F</td><td>333.01</td><td>2.93</td><td>F</td><td>30.33</td><td>0.80</td></tr><tr><td>Section 4.3.14</td><td>F</td><td>14.28</td><td>3.86</td><td>10</td><td>4.24</td><td>1.04</td><td>F</td><td>501.91</td><td>3.20</td><td>F</td><td>30.86</td><td>1.05</td></tr><tr><td>Section 4.3.15</td><td>T</td><td>3.77</td><td>1.46</td><td>10</td><td>4.14</td><td>1.75</td><td>10</td><td>0.31</td><td>1.20</td><td>10</td><td>1.78</td><td>5.59</td></tr><tr><td>Section 4.3.16</td><td>F</td><td>75.00</td><td>3.97</td><td>9.15</td><td>3.50</td><td>0</td><td>10</td><td>0.53</td><td>0.18</td><td>10</td><td>2.00</td><td>0.67</td></tr></tbody><tfoot><tr><td></td><td></td><td>10</td><td>1.39</td><td>0.38</td><td>10</td><td>8.03</td><td>0.036</td><td>10</td><td>0.17</td><td>1.85</td><td>0.42</td><td>7.73</td></tr></tfoot></table>

<figure><img src="image_13.png" /></figure>
<table><caption>**Table 10** Detailed scores for the offline track</caption><thead><tr><th rowspan="3">Reference to benchmark description</th><th colspan="3">RITHM</th><th colspan="3">MonPoly</th><th colspan="3">STEPR</th><th colspan="3">QEA</th></tr><tr><th colspan="2">Verdict</th><th rowspan="2">Mem (MB)<br/>m-score</th><th rowspan="2">Ovhd (s)<br/>o-score</th><th colspan="2">Verdict</th><th rowspan="2">Mem (MB)<br/>m-score</th><th rowspan="2">Ovhd (s)<br/>o-score</th><th colspan="2">Verdict</th><th rowspan="2">Mem (MB)<br/>m-score</th><th rowspan="2">Ovhd (s)<br/>o-score</th></tr><tr><th>v-score</th><th>v-score</th><th>v-score</th><th>v-score</th><th>v-score</th><th>v-score</th><th>v-score</th></tr></thead><tbody><tr><td>Section 4.3.1</td><td>F</td><td>993</td><td>0.60</td><td>F</td><td>13</td><td>0.13</td><td>F</td><td>29.53</td><td>0.90</td><td>F</td><td>4.535</td><td>0.24</td></tr><tr><td>Section 4.3.2</td><td>F</td><td>0.03</td><td>1.12</td><td>10</td><td>2.31</td><td>5.32</td><td>10</td><td>1.02</td><td>0.75</td><td>10</td><td>6.64</td><td>2.81</td></tr><tr><td>Section 4.3.3</td><td>F</td><td>0.30</td><td>7.67</td><td>10</td><td>1228</td><td>8.40</td><td>F</td><td>645.17</td><td>8.87</td><td>F</td><td>33.30</td><td>3.58</td></tr><tr><td>Section 4.3.4</td><td>F</td><td>0.05</td><td>0.63</td><td>10</td><td>2.32</td><td>5.41</td><td>10</td><td>0.97</td><td>0.68</td><td>10</td><td>6.66</td><td>3.28</td></tr><tr><td>Section 4.3.5</td><td>F</td><td>10</td><td>2.83</td><td>8.41</td><td>10</td><td>1.02</td><td>10</td><td>2.79</td><td>0.39</td><td>10</td><td>3.36</td><td>0.68</td></tr><tr><td>Section 4.3.6</td><td>F</td><td>0.43</td><td>6.29</td><td>10</td><td>544</td><td>5.09</td><td>F</td><td>274.29</td><td>7.77</td><td>F</td><td>32.94</td><td>3.71</td></tr><tr><td>Section 4.3.7</td><td>N/A</td><td>0</td><td>N/A</td><td>0</td><td>10</td><td>1.25</td><td>0.41</td><td>10</td><td>0.07</td><td>10</td><td>5.19</td><td>0.26</td></tr><tr><td>Section 4.3.8</td><td>N/A</td><td>0</td><td>N/A</td><td>0</td><td>20</td><td>1.33</td><td>F</td><td>255.48</td><td>96.00</td><td>F</td><td>4.53</td><td>9.53</td></tr><tr><td>Section 4.3.9</td><td>N/A</td><td>0</td><td>N/A</td><td>0</td><td>370</td><td>1.82</td><td>1.56</td><td>10</td><td>0.14</td><td>10</td><td>8.04</td><td>8.42</td></tr><tr><td>Section 4.3.10</td><td>N/A</td><td>0</td><td>N/A</td><td>0</td><td>10</td><td>0.20</td><td>0.08</td><td>10</td><td>0.11</td><td>10</td><td>7.75</td><td>9.79</td></tr><tr><td>Section 4.3.11</td><td>T</td><td>14.27</td><td>5.40</td><td>T</td><td>13.00</td><td>9.76</td><td>6.39</td><td>10</td><td>0.22</td><td>10</td><td>127.62</td><td>4.51</td></tr><tr><td>Section 4.3.12</td><td>F</td><td>4.48</td><td>2.65</td><td>10</td><td>4.92</td><td>4.20</td><td>3.17</td><td>10</td><td>0.16</td><td>10</td><td>30.33</td><td>3.18</td></tr><tr><td>Section 4.3.13</td><td>F</td><td>14.27</td><td>7.20</td><td>F</td><td>13.00</td><td>1.04</td><td>F</td><td>501.91</td><td>3.20</td><td>F</td><td>30.86</td><td>1.05</td></tr><tr><td>Section 4.3.14</td><td>F</td><td>3.86</td><td>0.59</td><td>10</td><td>4.24</td><td>4.08</td><td>10</td><td>0.11</td><td>1.32</td><td>10</td><td>1.79</td><td>4.01</td></tr><tr><td>Section 4.3.15</td><td>T</td><td>3.77</td><td>1.46</td><td>10</td><td>4.14</td><td>1.75</td><td>10</td><td>0.31</td><td>1.20</td><td>10</td><td>1.78</td><td>5.59</td></tr><tr><td>Section 4.3.16</td><td>F</td><td>75.00</td><td>3.97</td><td>9.15</td><td>3.50</td><td>0</td><td>10</td><td>0.53</td><td>0.18</td><td>10</td><td>2.00</td><td>0.67</td></tr><tr><td></td><td>F</td><td>1.39</td><td>0.38</td><td>10</td><td>8.03</td><td>0.036</td><td>10</td><td>0.17</td><td>1.85</td><td>10</td><td>250.30</td><td>2.03</td></tr></tbody></table>

<figure><img src="image_13.png" /></figure>
<table><caption>Table 10 continued</caption><thead><tr><th rowspan="3">Reference to benchmark description</th><th colspan="3">RITHM</th><th colspan="3">MonPoly</th><th colspan="3">STEPR</th><th colspan="3">QEA</th></tr><tr><th colspan="2">Verdict</th><th rowspan="2">Mem (MB)<br>m-score</th><th rowspan="2">Ovhd (s)<br>o-score</th><th colspan="2">Verdict</th><th rowspan="2">Mem (MB)<br>m-score</th><th rowspan="2">Ovhd (s)<br>o-score</th><th colspan="2">Verdict</th><th rowspan="2">Mem (MB)<br>m-score</th><th rowspan="2">Ovhd (s)<br>o-score</th></tr><tr><th>v-score</th><th>v-score</th><th>v-score</th><th>v-score</th><th>v-score</th><th>v-score</th><th>v-score</th></tr></thead><tbody><tr><td>Section 4.3.17</td><td>F</td><td>14.04</td><td>0.16</td><td>F</td><td>24.00</td><td>3.06</td><td>F</td><td>36.01</td><td>1.19</td><td>F</td><td>295.52</td><td>1.36</td></tr><tr><td></td><td>10</td><td>4.94</td><td>7.67</td><td>10</td><td>2.89</td><td>0.40</td><td>10</td><td>1.93</td><td>1.03</td><td>10</td><td>0.23</td><td>0.90</td></tr><tr><td>Section 4.3.18</td><td>F</td><td>39.79</td><td>5.18</td><td>F</td><td>2675.00</td><td>3405.00</td><td>F</td><td>622.66</td><td>9.96</td><td>F</td><td>234.78</td><td>2.04</td></tr><tr><td></td><td>10</td><td>8.01</td><td>2.47</td><td>10</td><td>0.12</td><td>0.375</td><td>10</td><td>0.51</td><td>1.28</td><td>10</td><td>1.36</td><td>6.25</td></tr><tr><td>Section 4.3.19</td><td>T</td><td>14.00</td><td>5.14</td><td>T</td><td>13.00</td><td>26.21</td><td>T</td><td>494.39</td><td>9.17</td><td>T</td><td>239.60</td><td>3.54</td></tr><tr><td></td><td>10</td><td>4.62</td><td>3.12</td><td>10</td><td>4.98</td><td>0.61</td><td>10</td><td>0.13</td><td>1.75</td><td>10</td><td>0.27</td><td>4.53</td></tr></tbody></table>
<table><caption>**Table 10** continued</caption><thead><tr><th rowspan="3">Reference to<br>benchmark<br>description</th><th colspan="3">RITHM</th><th colspan="3">MonPoly</th><th colspan="3">STEPR</th><th colspan="3">QEA</th></tr><tr><th colspan="2">Verdict</th><th rowspan="2">Mem (MB)<br>m-score</th><th rowspan="2">Ovhd (s)<br>o-score</th><th colspan="2">Verdict</th><th rowspan="2">Mem (MB)<br>m-score</th><th rowspan="2">Ovhd (s)<br>o-score</th><th colspan="2">Verdict</th><th rowspan="2">Mem (MB)<br>m-score</th><th rowspan="2">Ovhd (s)<br>o-score</th></tr><tr><th>v-score</th><th>v-score</th><th>v-score</th><th>v-score</th><th>v-score</th><th>v-score</th><th>v-score</th></tr></thead><tbody><tr><td>Section 4.3.17</td><td>F</td><td>14.04</td><td>0.16</td><td>F</td><td>24.00</td><td>3.06</td><td>F</td><td>36.01</td><td>1.19</td><td>F</td><td>295.52</td><td>1.36</td></tr><tr><td></td><td>10</td><td>4.94</td><td>7.67</td><td>10</td><td>2.89</td><td>0.40</td><td>10</td><td>1.93</td><td>1.03</td><td>10</td><td>0.23</td><td>0.90</td></tr><tr><td>Section 4.3.18</td><td>F</td><td>39.79</td><td>5.18</td><td>F</td><td>2675.00</td><td>3405.00</td><td>F</td><td>622.66</td><td>9.96</td><td>F</td><td>234.78</td><td>2.04</td></tr><tr><td></td><td>10</td><td>8.01</td><td>2.47</td><td>10</td><td>0.12</td><td>0.375</td><td>10</td><td>0.51</td><td>1.28</td><td>10</td><td>1.36</td><td>6.25</td></tr><tr><td>Section 4.3.19</td><td>T</td><td>14.00</td><td>5.14</td><td>T</td><td>13.00</td><td>26.21</td><td>T</td><td>494.39</td><td>9.17</td><td>T</td><td>239.60</td><td>3.54</td></tr><tr><td></td><td>10</td><td>4.62</td><td>3.12</td><td>10</td><td>4.98</td><td>0.61</td><td>10</td><td>0.13</td><td>1.75</td><td>10</td><td>0.27</td><td>4.53</td></tr></tbody></table>
<table><caption>**Table 11** Scores for the offline track</caption><thead><tr><td>Rank</td><td>Team name</td><td>Correctness score</td><td>Overhead score</td><td>Memory score</td><td>Total score</td></tr></thead><tbody><tr><td>1</td><td>QEA</td><td>190</td><td>77.79</td><td>71.36</td><td>339.15</td></tr><tr><td>2</td><td>MONPOLY</td><td>190</td><td>39.35</td><td>64.19</td><td>293.54</td></tr><tr><td>3</td><td>RITHM-2</td><td>140</td><td>54.40</td><td>42.52</td><td>236.91</td></tr><tr><td>4</td><td>STEPR</td><td>190</td><td>18.46</td><td>11.93</td><td>220.40</td></tr></tbody></table>

<figure><img src="image_14.png" /><figcaption>**Fig. 7** Graphical representation of the scores for the offline track</figcaption></figure>

itself. This is the reason why CRV assigns a score to both the overhead and the memory utilization.

VerifyThis [55] is another series of competitions dedicated to program verification and initiated in 2011. In VerifyThis, the organisers provide to the participants algorithms in a pseudo-code with an informal specification written in natural language. The challenge for each team is to formalize the requirements, implement a prototype and verify whether the implementation is correct w.r.t. the given requirements. The available time to accomplish this goal is quite short ranging between 45 and 90 minutes. The format of VerifyThis competition differs with CRV format because is problem-centred and focuses more on the skills of the team in formalizing and solving the problem rather than on the tool characteristics and performance. For this reason, it is even possible for two different teams to participate with the same tool to the competition.

The *Rigorous Examination of Reactive Systems (RERS)* challenge [54] follows a similar problem-centred approach of VerifyThis in contrast to a more tool-centred approach followed in CRV. The goal of the RERS challenge is to evaluate the effectiveness of various verification and validation approaches on reactive systems (RS), focusing on the analysis of a particular class of RS called *event-condition-action* (ECA) systems. These systems have transitions for input events that are guarded by conditions, operates on the internal state and produce outputs. The RERS challenge consists in verifying a set of properties on ECA systems: properties can be reachability properties or Linear Temporal Logic (LTL)

properties. The teams are free to choose the tool and the method they prefer, and they can also combine different tools in a toolchain in order to solve the challenge. Another difference with CRV is the selection of the benchmarks: in CRV the benchmarks are provided by the participating teams, while in RERS the benchmarks are automatically generated with a procedure discussed in [78].

*Positive points* Several positive aspects are to be noted regarding the first edition of CRV competition.

- The competition featured 8 distinct teams participating in the 3 tracks resulting in 11 participating teams in the tracks.

- The organisers have designed a sensible evaluation method. This method has been peer-reviewed and validated by the participating teams before the beginning of the competition. The method has been built upon the research efforts made in the runtime verification community when evaluating runtime verification prototypes.

- Choices needed to be made regarding the classification criteria of tracks. Moreover, different tracks could have been possible: domain of the monitored system, programming language of the monitor, categories of specifications, a track on elegance of the specification. The organisers have arranged the tracks of the competition according to the monitored system: either its programming language in case of monitoring software or traces. This reflects the fact of inline monitoring has been so far the most popular RV setting when monitoring software.

*Negative points* Several negative aspects are to be noted regarding the first edition of CRV competition.

- Significant delays were observed regarding benchmark submission. These delays were due to the substantial efforts required to convey the exact semantics of the specifications submitted. Indeed, as can be expected, some of the specifications could be interpreted differently by different participants. Moreover, as the participating teams mainly provided specifications in the input language of their tools, participants had also to formalize them in the specification language of their own tool.

<figure><img src="image_15.png" /></figure>
<table><caption>**Table 11** Scores for the offline track</caption><thead><tr><td>Rank</td><td>Team name</td><td>Correctness score</td><td>Overhead score</td><td>Memory score</td><td>Total score</td></tr></thead><tbody><tr><td>1</td><td>QEA</td><td>190</td><td>77.79</td><td>71.36</td><td>339.15</td></tr><tr><td>2</td><td>MONPOLY</td><td>190</td><td>39.35</td><td>64.19</td><td>293.54</td></tr><tr><td>3</td><td>RITHM-2</td><td>140</td><td>54.40</td><td>42.52</td><td>236.91</td></tr><tr><td>4</td><td>STEPR</td><td>190</td><td>18.46</td><td>11.93</td><td>220.40</td></tr></tbody></table>

<figure><img src="image_14.png" /><figcaption>**Fig. 7** Graphical representation of the scores for the offline track</figcaption></figure>

itself. This is the reason why CRV assigns a score to both the overhead and the memory utilization.

VerifyThis [55] is another series of competitions dedicated to program verification and initiated in 2011. In VerifyThis, the organisers provide to the participants algorithms in a pseudo-code with an informal specification written in natural language. The challenge for each team is to formalize the requirements, implement a prototype and verify whether the implementation is correct w.r.t. the given requirements. The available time to accomplish this goal is quite short ranging between 45 and 90 minutes. The format of VerifyThis competition differs with CRV format because is problem-centred and focuses more on the skills of the team in formalizing and solving the problem rather than on the tool characteristics and performance. For this reason, it is even possible for two different teams to participate with the same tool to the competition.

The *Rigorous Examination of Reactive Systems (RERS)* challenge [54] follows a similar problem-centred approach of VerifyThis in contrast to a more tool-centred approach followed in CRV. The goal of the RERS challenge is to evaluate the effectiveness of various verification and validation approaches on reactive systems (RS), focusing on the analysis of a particular class of RS called *event-condition-action* (ECA) systems. These systems have transitions for input events that are guarded by conditions, operates on the internal state and produce outputs. The RERS challenge consists in verifying a set of properties on ECA systems: properties can be reachability properties or Linear Temporal Logic (LTL)

properties. The teams are free to choose the tool and the method they prefer, and they can also combine different tools in a toolchain in order to solve the challenge. Another difference with CRV is the selection of the benchmarks: in CRV the benchmarks are provided by the participating teams, while in RERS the benchmarks are automatically generated with a procedure discussed in [78].

*Positive points* Several positive aspects are to be noted regarding the first edition of CRV competition.

- The competition featured 8 distinct teams participating in the 3 tracks resulting in 11 participating teams in the tracks.

- The organisers have designed a sensible evaluation method. This method has been peer-reviewed and validated by the participating teams before the beginning of the competition. The method has been built upon the research efforts made in the runtime verification community when evaluating runtime verification prototypes.

- Choices needed to be made regarding the classification criteria of tracks. Moreover, different tracks could have been possible: domain of the monitored system, programming language of the monitor, categories of specifications, a track on elegance of the specification. The organisers have arranged the tracks of the competition according to the monitored system: either its programming language in case of monitoring software or traces. This reflects the fact of inline monitoring has been so far the most popular RV setting when monitoring software.

*Negative points* Several negative aspects are to be noted regarding the first edition of CRV competition.

- Significant delays were observed regarding benchmark submission. These delays were due to the substantial efforts required to convey the exact semantics of the specifications submitted. Indeed, as can be expected, some of the specifications could be interpreted differently by different participants. Moreover, as the participating teams mainly provided specifications in the input language of their tools, participants had also to formalize them in the specification language of their own tool.

<figure><img src="image_15.png" /></figure>
- Delays were also observed during the phases where the organizers had to prepare the next phases. For instance, after the benchmark submission phase, a sanity check had to be performed regarding the submissions of some participants. Several iterations were needed to unify the submissions in spite of the provided provided, which was consequently not constraining enough or ambiguous on some aspects. We note that building on this observation, the next edition of the competition learned from this and for instance defined standard formats for traces [47].

Memory measurement in Java It was not entirely clear how to measure memory usage for the Java benchmarks. It was decided that memory used by the JVM should be excluded and the participants were asked to suggest methods for recording memory usage. The first proposal was to use Java Management eXtensions (JMX) to create a separate Java program that attached to the running benchmark and queried its memory usage. For completeness, we include an example Java program utilizing this method:

```java
public class JMXExample {
    private static final String
        CONNECTOR_ADDRESS =
            "com.sun.management.jmxremote." +
            "localConnectorAddress";

    public static void main
        (String[] args)
    throws Exception {
        // attach to target VM
        VirtualMachineDescriptor vmd =
            VirtualMachine.list().get(0);
        VirtualMachine vm = VirtualMachine.
            attach(vmd);
        JMXConnector jmxc
            = getLocalConnection vm;
        MBeanServerConnection mbsc =
            jmxc.getMBeanServerConnection();

        MemoryMXBean memory
            = ManagementFactory.
                getPlatformMXBean(mbsc,
                MemoryMXBean.class);
        List/MemoryPoolMXBean> pools =
            ManagementFactory.
                getPlatformMXBeans(mbsc,
                MemoryPoolMXBean.class);

        while (true) {
            System.out.println("Used Heap: " +
                (memory.getHeapMemoryUsage().
                    getUsed() /
                    1000000f) + "mb");
            for (MemoryPoolMXBean pool :
                pools) {
                System.out.println("Used "
                    + poolOSEName() +
                    ": " + (pool.getPeakUsage().
                        getUsed() /
```

```java
                    1000000f) + "mb");
                }
                System.out.println();
                Thread.sleep(100);
            }
        }
        private static JMXConnector
            getLocalConnection
                (VirtualMachinevm)
                throws Exception
        {
            Properties props
                = vm.getAgentProperties();
            String connectorAddress =
                props.getProperty
                    (CONNECTOR_ADDRESS);
            if (connectorAddress == null) {
                props = vm.getSystemProperties();
                String home = props.getProperty
                    ("java.home");
                String agent = home +
                    Filesepahar + "lib" +
                    Filesepahar
                        + "management-agent.jar";
                vm.loadAgentagent);
                props = vm.getAgentProperties();
                connectorAddress =
                    props Property
                    (CONNECTOR_ADDRESS);
            }
            JMXServiceURL url =
                new JMXServiceURL
                    (connectorAddress);
            return JMXConnectorFactory.connect
                (url);
        }
```

However, this approach required a separate JVM to be started to run this program. As some benchmarks are very short-lived, this led to the benchmark program terminating before this method could begin measuring memory utilization. An alternative method using the jstat tool (standing for Java Virtual Machine Statistics Monitoring Tool) was proposed. This method sampled memory usage every 10ms and dumped the output into a file, which was then parsed after the benchmark had run to compute memory utilization. The script for running a program and recording its memory utilization is given below:

```bash
#!/bin/bash

java -cp "lib/*:bin" $1 &> out.log &
pid=$!
jstat -gc $pid 10ms &> memory.log

echo "Peak memory was " >> out.log
tail -n +2 memory.log | while read
line; do
    count=0
    sum=0.0
    for entry in $line; do
```
- Delays were also observed during the phases where the organizers had to prepare the next phases. For instance, after the benchmark submission phase, a sanity check had to be performed regarding the submissions of some participants. Several iterations were needed to unify the submissions in spite of the provided provided, which was consequently not constraining enough or ambiguous on some aspects. We note that building on this observation, the next edition of the competition learned from this and for instance defined standard formats for traces [47].

Memory measurement in Java It was not entirely clear how to measure memory usage for the Java benchmarks. It was decided that memory used by the JVM should be excluded and the participants were asked to suggest methods for recording memory usage. The first proposal was to use Java Management eXtensions (JMX) to create a separate Java program that attached to the running benchmark and queried its memory usage. For completeness, we include an example Java program utilizing this method:

```java
public class JMXExample {
    private static final String
        CONNECTOR_ADDRESS =
            "com.sun management.jmxremote." +
            "localConnectorAddress";

    public static void main
        (String[] args)
    throws Exception {
        // attach to target VM
        VirtualMachineDescriptor vmd =
            VirtualMachine. list().get(0);
        VirtualMachine vm = VirtualMachine.
            attach(vmd);
        JMXConnector jmxc
            = getLocalConnection vm;
        MBeanServerConnection mbsc =
            jmxc. getMBeanServerConnection();

        MemoryMXBean memory
            = ManagementFactory.
                getPlatformMXBean(mbsc,
                MemoryMXBean. class);
        List<MemoryPoolMXBean> pools =
            ManagementFactory.
                getPlatformMXBeans(mbsc,
                MemoryPoolMXBean. class);

        while (true) {
            System.out. println("Used Heap: " +
                (memory. getHeapMemoryUsage()).
                getUsed() /
                1000000f) + "mb");
            for (MemoryPoolMXBean pool :
                pools) {
                System.out. println("Used "
                    + pool. getName() +
                    ": " + (pool. getPeakUsage()).
                getUsed() /
```

```java
                    1000000f) + "mb");
                }
                System.out. println();
                Thread.sleep(100);
            }
        }
        private static JMXConnector
            getLocalConnection
                (VirtualMachinevm)
                throws Exception
        {
            Properties props
                = vm. getAgentProperties();
            String connectorAddress =
                props. getProperty
                    (CONNECTOR_ADDRESS);
            if (connectorAddress == null) {
                props = vm.SystemProperties();
                String home = props. getProperty
                    ("java. home");
                String agent = home +
                    File. separator + "lib" +
                    File. separator
                        + "management-agent.jar";
                vm. loadAgent (agent);
                props = vm. getAgentProperties();
                connectorAddress =
                    props. getProperty
                        (CONNECTOR_ADDRESS);
            }
            JMXServiceURL url =
                new JMXServiceURL
                    (connectorAddress);
            return JMXConnectorFactory. connect
                (url);
        }
```

However, this approach required a separate JVM to be started to run this program. As some benchmarks are very short-lived, this led to the benchmark program terminating before this method could begin measuring memory utilization. An alternative method using the `jstat` tool (standing for Java Virtual Machine Statistics Monitoring Tool) was proposed. This method sampled memory usage every 10ms and dumped the output into a file, which was then parsed after the benchmark had run to compute memory utilization. The script for running a program and recording its memory utilization is given below:

```bash
#!/bin/bash

java -cp "lib/*:bin" $1 &> out.log &
pid=$!
jstat -gc $pid 10ms &> memory.log

echo "Peak memory was " >> out.log
tail -n +2 memory.log | while read
line; do
    count=0
    sum=0.0
    for entry in $line; do
```
```c
if [[ count -eq 2 || count -eq 3 ||
     count -eq 5 || count -eq 7 ]]]
then
  sum=$(bc -l <<< "$entry + $sum")
fi
count=$( (count+1))
done
int_sum=$( echo $sum | awk
  '{ print int($1) }')
if [[ $int_sum -gt $max ]] then
  max=$int_sum
  echo "$max"
fi
echo $max
done | tail -1 >> out.log
```

The time taken to parse the memory.log file was non-negligible. Therefore, it was necessary to perform separate runs to measure time overhead and memory utilization. Both approaches make use of the same underlying technology so should produce similar results. Ideally, a single method would have been used, but both approaches were used by different teams in the competition.

**Monitoring hardware** In the last decade, the increasing complexity of the circuit design has been making their verification and validation more convenient to perform using hardware emulation instead of the classical simulation, a task becoming very time consuming and expensive for the industry [57,72].

Hardware emulation has opened new interesting challenges such as how to verify at runtime real-time temporal properties specified in assertion languages and how to synthesize resource efficient monitoring hardware checking these properties. FoCs [35] developed by IBM and MBAC [25–27] developed by Zilic and Boulé are important examples of tools for generating synthesizable hardware monitors from Property Specification Language (PSL). In [48], Finkbeiner et al. present a technique to synthesize monitor circuits from LTL formulas with bounded and unbounded future operators. More recently, Reinbacher et. al. introduce in [76,77] synthesizable hardware monitors from different fragments of Metric Temporal Logic (MTL) and Jaksic et al. in [57,58,72,79] propose several practical techniques for generating Field-Programmable Gate Array (FPGA) hardware monitors for Signal Temporal Logic (STL), an extension of MTL handling predicates over the real-values.

The first edition of the CRV competition was entirely dedicated to software runtime verification tools. We are currently exploring the possibility to add a special track for hardware monitoring tools. However, the problem of comparing performances of hardware monitors opens new challenges. In particular, all the aforementioned approaches use not only different specification languages for the property to monitor, but also different hardware and dedicated third-party software for the hardware synthesis, making extremely hard to assess the real merit of the tools for the automatic monitors generation.

**Toward a general specification language (for the competition)**

- every tool is defined in its own logic that is mathematically defined but have different semantics

- There is no unified specification that the organizers could use to provide specifications

- Even if such a specification language existed some tools would handle only a fragment of such logic, one would have to provide specs in each fragment in such a way that the competition is fair.

**On the challenges of monitoring C programs** In spite of its maturity and robust industry support, the C programming language remains a challenging frontier for runtime verification practitioners. As a close-to-the-metal, performance-driven language, C offers flexible and fine-grained control over memory, and avoids the use of burdensome safety features; the programmer is entrusted with the utmost power and responsibility. As a consequence, however, there is little that can be asserted about the behavior of a C program other than that which requires deep, potentially expensive analysis. However, because the language has long since passed the threshold of immortality, it is imperative that more scalable and sophisticated tools and techniques be developed to meet the needs of the C programming community. However, this requires that several key challenges be properly addressed.

First, it is necessary to achieve good coverage of the language's features and constructs, and this can a very time-consuming process. Even if one has a highly efficient analysis, insufficient coverage can severely limit the effectiveness of a tool at more than a few handful of 1000 lines of code in size. On the one hand, given the maturity of the language, legacy support becomes a concern. The libraries participating in a mature C project may be staggered chronologically, and when delving into the depths, it is not uncommon to encounter rarely used built-in functions like `setjmp`, keyworded modifiers such as `register`, and even the use of the `goto` statement. To its credit, the C language strives to be parsimonious in its extensions, but this also means that it is not uncommon to find highly tailored and difficult to analyze features such as custom-defined memory allocators. Furthermore, many dialects of C, such as those intended for use in embedded environments, often extend the language with compiler-specific and/or platform-dependent constructs. What is desired is a standard way of monitoring C programs, but it is difficult to conceive of a comprehensive solution. As such, tool developers with novel ideas must either build their work on top of an existing analysis framework or expend considerable time and energy accruing the necessary technological capital. In short, bringing innovative analyses to market can require significant investment.
```c
if [[ count -eq 2 || count -eq 3 ||
        count -eq 5 || count -eq 7 ]]]
then
  sum=$(bc -l <<< "$entry + $sum")
fi
count=$( (count+1))
done
int_sum=$( echo $sum | awk
           '{ print int($1) }')
if [[ $int_sum -gt $max ]] then
  max=$int_sum
  echo "$max"
fi
echo $max
done | tail -1 >> out.log
```

The time taken to parse the memory.log file was non-negligible. Therefore, it was necessary to perform separate runs to measure time overhead and memory utilization. Both approaches make use of the same underlying technology so should produce similar results. Ideally, a single method would have been used, but both approaches were used by different teams in the competition.

**Monitoring hardware** In the last decade, the increasing complexity of the circuit design has been making their verification and validation more convenient to perform using hardware emulation instead of the classical simulation, a task becoming very time consuming and expensive for the industry [57,72].

Hardware emulation has opened new interesting challenges such as how to verify at runtime real-time temporal properties specified in assertion languages and how to synthesize resource efficient monitoring hardware checking these properties. FoCs [35] developed by IBM and MBAC [25–27] developed by Zilic and Boulé are important examples of tools for generating synthesizable hardware monitors from Property Specification Language (PSL). In [48], Finkbeiner et al. present a technique to synthesize monitor circuits from LTL formulas with bounded and unbounded future operators. More recently, Reinbacher et. al. introduce in [76,77] synthesizable hardware monitors from different fragments of Metric Temporal Logic (MTL) and Jaksic et al. in [57,58,72,79] propose several practical techniques for generating Field-Programmable Gate Array (FPGA) hardware monitors for Signal Temporal Logic (STL), an extension of MTL handling predicates over the real-values.

The first edition of the CRV competition was entirely dedicated to software runtime verification tools. We are currently exploring the possibility to add a special track for hardware monitoring tools. However, the problem of comparing performances of hardware monitors opens new challenges. In particular, all the aforementioned approaches use not only different specification languages for the property to monitor, but also different hardware and dedicated third-party software for the hardware synthesis, making extremely hard to assess the real merit of the tools for the automatic monitors generation.

**Toward a general specification language (for the competition)**

- every tool is defined in its own logic that is mathematically defined but have different semantics

- There is no unified specification that the organizers could use to provide specifications

- Even if such a specification language existed some tools would handle only a fragment of such logic, one would have to provide specs in each fragment in such a way that the competition is fair.

**On the challenges of monitoring C programs** In spite of its maturity and robust industry support, the C programming language remains a challenging frontier for runtime verification practitioners. As a close-to-the-metal, performance-driven language, C offers flexible and fine-grained control over memory, and avoids the use of burdensome safety features; the programmer is entrusted with the utmost power and responsibility. As a consequence, however, there is little that can be asserted about the behavior of a C program other than that which requires deep, potentially expensive analysis. However, because the language has long since passed the threshold of immortality, it is imperative that more scalable and sophisticated tools and techniques be developed to meet the needs of the C programming community. However, this requires that several key challenges be properly addressed.

First, it is necessary to achieve good coverage of the language's features and constructs, and this can a very time-consuming process. Even if one has a highly efficient analysis, insufficient coverage can severely limit the effectiveness of a tool at more than a few handful of 1000 lines of code in size. On the one hand, given the maturity of the language, legacy support becomes a concern. The libraries participating in a mature C project may be staggered chronologically, and when delving into the depths, it is not uncommon to encounter rarely used built-in functions like `setjmp`, keyworded modifiers such as `register`, and even the use of the `goto` statement. To its credit, the C language strives to be parsimonious in its extensions, but this also means that it is not uncommon to find highly tailored and difficult to analyze features such as custom-defined memory allocators. Furthermore, many dialects of C, such as those intended for use in embedded environments, often extend the language with compiler-specific and/or platform-dependent constructs. What is desired is a standard way of monitoring C programs, but it is difficult to conceive of a comprehensive solution. As such, tool developers with novel ideas must either build their work on top of an existing analysis framework or expend considerable time and energy accruing the necessary technological capital. In short, bringing innovative analyses to market can require significant investment.

<figure><img src="image_16.png" /></figure>
Second, portability is becoming an increasingly important issue. In years past, it was enough that a tool could function in just two or three environments, but these days we are seeing a proliferation of different kinds of computing environments, including consumer electronics such as smartphones and sophisticated embedded environments such as control systems for avionics and healthcare. In all of these environments, C is either used directly or provides libraries for other languages including Java, Perl, and Python. A common feature of these new environments is a limited tolerance for runtime overhead, which is challenging from a verification standpoint. One possible way of reducing that overhead includes exposing runtime monitoring code in a way that allows for compiler optimizations, but because not all C compilers are available in all environments, many cost-saving measures can actually exacerbate the portability issue. Another way of controlling the runtime overhead of monitoring C program is to utilize various parallel algorithms on back-ends such as graphics processing unit (GPU), field-programmable gate array (FPGA), etc. A use of such back-ends requires profiling the monitors for obtaining an optimal performance. Such profiling effort can be prohibitive for scalable runtime verification because runtime verification techniques are expected to automate monitor generation, and a need of manual intervention during the profiling effort goes against the principle of automation. Designing a monitoring framework that is portable, robust in its safety guarantees, and minimally expensive remains an open problem.

## 8 Conclusions

This paper presents the final results of the first international Competition on Runtime Verification. A preliminary presentation of the results has been reported during the RV 2014 conference in Toronto, Canada. This paper provides a comprehensive overview of the teams and their tools, the submitted programs, traces, and specifications, the method used to compute the scores, and the final results for each of the tracks. We expect this report to help the runtime verification community in several ways. First, this report shall assist the future organizers of the competition to build on the efforts made to organize CRV 2014. Second, the report can also be seen as an entry point to several benchmarks containing non-trivial programs and properties. This shall help developers of tools to assess and experiment with their tools.

**Acknowledgements** Open access funding provided by TU Wien (TUW). The competition organizers, E. Bartocci, B. Bonakdarpour, and Y. Falcone, are grateful to many people. The competition organizers would like to warmly thank all participants for their hard work, the members of the runtime verification community who encouraged them to initiate this work, the Laboratoire d'Informatique de Grenoble and its IT team for its support, Inria and its GitLab framework, and finally the

DataMill team for providing us with such a nice experimentation platform to run all benchmarks. All the authors acknowledge the support of the ICT COST Action IC1402 Runtime Verification beyond Monitoring (ARVI). Ezio Bartocci acknowledges also the partial support of the Austrian FFG project HARMONIA (No. 845631) and the Austrian National Research Network (No. S 11405-N23) SHINE funded by the Austrian Science Fund (FWF). The research performed by Klaus Havelund was carried out at Jet Propulsion Laboratory, California Institute of Technology, under a contract with the National Aeronautics and Space Administration. The authors are grateful to the insightful reviewers who helped improving the quality of this paper.

**Open Access** This article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.

## References

1. Abdulla, P.A., Rustan, K., Leino, M. (eds.): Proceedings of TACAS 2011: The 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Volume 6605 of LNCS. Springer, Berlin (2011)

2. Barrett, C., Deters, M., de Moura, L., Oliveras, Ade, Stump, A.: 6 years of SMT-COMP. J. Autom. Reason. 50(3), 243–277 (2013)

3. Barringer, H., Falcone, Y., Havelund, K., Reger, G., Rydeheard, D.E.: Quantified event automata: towards expressive and efficient runtime monitors. In: Proceedings of FM 2012: The 18th International Symposium on Formal Methods, Volume 7436 of LNCS, pp. 68–84. Springer, Berlin (2012)

4. Bartocci, E., Bonakdarpour, B., Falcone, Y.: First international competition on software for runtime verification. In: Bonakdarpour and Smolka [24], pp. 1–9

5. Bartocci, E., Bortolussi, L., Nenzi, L.: A temporal logic approach to modular design of synthetic biological circuits. In: Proceedings of CMSB 2013: The 11th International Conference on Computational Methods in Systems Biology, Volume 8130 of LNCS, pp. 164–177. Springer, Berlin (2013)

6. Bartocci, E., Bortolussi, L., Sanguinetti, G.: Data-driven statistical learning of temporal logic properties. In: Proceedings of FORMATS 2014: The 12th International Conference on Formal Modeling and Analysis of Timed Systems, Volume 8711 of LNCS, pp. 23–37 (2014)

7. Bartocci, E., Falcone, Y.: Runtime verification and enforcement, the (industrial) application perspective (track introduction). In: Proceedings of ISOLLA 2016: The 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications, Part II, Volume 9953 of LNCS, pp. 333–338 (2016)

8. Bartocci, E., Grosu, R., Karmarkar, A., Smolka, S.A., Stoller, S.D., Zadok, E., Seyster, J.: Adaptive runtime verification. In: Proceedings of RV 2012: The 3rd International Conference on Runtime Verification, Volume 7687 of LNCS, pp. 168–182. Springer, Berlin (2012)

9. Bartocci, E., Liò, P.: Computational modeling, formal analysis, and tools for systems biology. PLoS Comput. Biol. 12(1), e1004591 (2016)

10. Basin, D., Harvan, M., Klaedtke, F., Zălinescu, E.: MONPOLY: Monitoring usage-control policies. In: Proceedings of RV 2011: The 2nd International Conference on Runtime Verification, Volume 7186 of LNCS, pp. 360–364. Springer, Berlin (2012)
Second, portability is becoming an increasingly important issue. In years past, it was enough that a tool could function in just two or three environments, but these days we are seeing a proliferation of different kinds of computing environments, including consumer electronics such as smartphones and sophisticated embedded environments such as control systems for avionics and healthcare. In all of these environments, C is either used directly or provides libraries for other languages including Java, Perl, and Python. A common feature of these new environments is a limited tolerance for runtime overhead, which is challenging from a verification standpoint. One possible way of reducing that overhead includes exposing runtime monitoring code in a way that allows for compiler optimizations, but because not all C compilers are available in all environments, many cost-saving measures can actually exacerbate the portability issue. Another way of controlling the runtime overhead of monitoring C program is to utilize various parallel algorithms on back-ends such as graphics processing unit (GPU), field-programmable gate array (FPGA), etc. A use of such back-ends requires profiling the monitors for obtaining an optimal performance. Such profiling effort can be prohibitive for scalable runtime verification because runtime verification techniques are expected to automate monitor generation, and a need of manual intervention during the profiling effort goes against the principle of automation. Designing a monitoring framework that is portable, robust in its safety guarantees, and minimally expensive remains an open problem.

## 8 Conclusions

This paper presents the final results of the first international Competition on Runtime Verification. A preliminary presentation of the results has been reported during the RV 2014 conference in Toronto, Canada. This paper provides a comprehensive overview of the teams and their tools, the submitted programs, traces, and specifications, the method used to compute the scores, and the final results for each of the tracks. We expect this report to help the runtime verification community in several ways. First, this report shall assist the future organizers of the competition to build on the efforts made to organize CRV 2014. Second, the report can also be seen as an entry point to several benchmarks containing non-trivial programs and properties. This shall help developers of tools to assess and experiment with their tools.

**Acknowledgements** Open access funding provided by TU Wien (TUW). The competition organizers, E. Bartocci, B. Bonakdarpour, and Y. Falcone, are grateful to many people. The competition organizers would like to warmly thank all participants for their hard work, the members of the runtime verification community who encouraged them to initiate this work, the Laboratoire d'Informatique de Grenoble and its IT team for its support, Inria and its GitLab framework, and finally the

DataMill team for providing us with such a nice experimentation platform to run all benchmarks. All the authors acknowledge the support of the ICT COST Action IC1402 Runtime Verification beyond Monitoring (ARVI). Ezio Bartocci acknowledges also the partial support of the Austrian FFG project HARMONIA (No. 845631) and the Austrian National Research Network (No. S 11405-N23) SHINE funded by the Austrian Science Fund (FWF). The research performed by Klaus Havelund was carried out at Jet Propulsion Laboratory, California Institute of Technology, under a contract with the National Aeronautics and Space Administration. The authors are grateful to the insightful reviewers who helped improving the quality of this paper.

**Open Access** This article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.

## References

1. Abdulla, P.A., Rustan, K., Leino, M. (eds.): Proceedings of TACAS 2011: The 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Volume 6605 of LNCS. Springer, Berlin (2011)

2. Barrett, C., Deters, M., de Moura, L., Oliveras, Ade, Stump, A.: 6 years of SMT-COMP. J. Autom. Reason. 50(3), 243–277 (2013)

3. Barringer, H., Falcone, Y., Havelund, K., Reger, G., Rydeheard, D.E.: Quantified event automata: towards expressive and efficient runtime monitors. In: Proceedings of FM 2012: The 18th International Symposium on Formal Methods, Volume 7436 of LNCS, pp. 68–84. Springer, Berlin (2012)

4. Bartocci, E., Bonakdarpour, B., Falcone, Y.: First international competition on software for runtime verification. In: Bonakdarpour and Smolka [24], pp. 1–9

5. Bartocci, E., Bortolussi, L., Nenzi, L.: A temporal logic approach to modular design of synthetic biological circuits. In: Proceedings of CMSB 2013: The 11th International Conference on Computational Methods in Systems Biology, Volume 8130 of LNCS, pp. 164–177. Springer, Berlin (2013)

6. Bartocci, E., Bortolussi, L., Sanguinetti, G.: Data-driven statistical learning of temporal logic properties. In: Proceedings of FORMATS 2014: The 12th International Conference on Formal Modeling and Analysis of Timed Systems, Volume 8711 of LNCS, pp. 23–37 (2014)

7. Bartocci, E., Falcone, Y.: Runtime verification and enforcement, the (industrial) application perspective (track introduction). In: Proceedings of ISOLLA 2016: The 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications, Part II, Volume 9953 of LNCS, pp. 333–338 (2016)

8. Bartocci, E., Grosu, R., Karmarkar, A., Smolka, S.A., Stoller, S.D., Zadok, E., Seyster, J.: Adaptive runtime verification. In: Proceedings of RV 2012: The 3rd International Conference on Runtime Verification, Volume 7687 of LNCS, pp. 168–182. Springer, Berlin (2012)

9. Bartocci, E., Liò, P.: Computational modeling, formal analysis, and tools for systems biology. PLoS Comput. Biol. 12(1), e1004591 (2016)

10. Basin, D., Harvan, M., Klaedtke, F., Zălinescu, E.: MONPOLY: Monitoring usage-control policies. In: Proceedings of RV 2011: The 2nd International Conference on Runtime Verification, Volume 7186 of LNCS, pp. 360–364. Springer, Berlin (2012)
11. Basin, D., Harvan, M., Klaedtke, F., Zălinescu, E.: Monitoring data usage in distributed systems. IEEE Trans. Softw. Eng. 39(10), 1403–1426 (2013)

12. Basin, D., Klaedtke, F., Müller, S., Zălinescu, E.: Monitoring metric first-order temporal properties. J. ACM 62(2), 15:1–15:45 (2015)

13. Basin, D., Klaedtke, F., Zălinescu, E.: Greedily computing associative aggregations on sliding windows. Inf. Process. Lett. 115(2), 186–192 (2015)

14. Basin, D.A., Caronni, G., Ereth, S., Harvan, M., Klaedtke, F., ManTEL, H.: Scalable offline monitoring. Form. Methods Syst. Des. 49(1–2), 75–108 (2016)

15. Basin, D.A., Klaedtke, F., Marinovic, S., Zălinescu, E.: Monitoring of temporal first-order properties with aggregations. Form. Methods Syst. Des. 46(3), 262–285 (2015)

16. Baudin, P., Filliâtre, J.-C., Marché, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C Specification Language. Version 1.8, March 2014

17. Benameur, A., Evans, N.S., Elder, M.C.: MINESTRONE: testing the SOUP. In: Kanich, C., Sherr, M. (eds.) In: 6th Workshop on Cyber Security Experimentation and Test, CSET ’13, Washington, DC, USA, August 12, 2013. USENIX Association (2013)

18. Berkovich, S., Bonakdarpour, B., Fischmeister, S.: GPU-based runtime verification. In: 27th IEEE International Symposium on Parallel and Distributed Processing, IPDPS 2013, Cambridge, MA, USA, May 20–24, 2013, pp. 1025–1036 (2013)

19. Beyer, D.: Competition on software verification—(SV-COMP). In: Proceedings of TACAS 2012: The 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems—18th International Conference, Volume 7214 of LNCS, pp. 504–524. Springer, Berlin (2012)

20. Beyer, D.: Status report on software verification—(competition summary SV-COMP 2014). In: Ábrahám, E., Havelund, K. (eds.) Tools and Algorithms for the Construction and Analysis of Systems—20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5–13, 2014. Proceedings, Volume 8413 of Lecture Notes in Computer Science, pp. 373–388. Springer, Berlin (2014)

21. Beyer, D.: Software verification and verifiable witnesses—(report on SV-COMP 2015). In: Proceedings of TACAS 2015: The 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, vol. 9035, pp. 401–416. Springer, Berlin (2015)

22. Blackburn, S.M., Garner, R., Hoffmann, C., Khan, A.M., McKinley, K.S., Bentzur, R., Diwan, A., Feinberg, D., Frampton, D., Guyer, S.Z., Hirzel, M., Hosking, A.L., Jump, M., Lee, H.B., Eliot, J., Moss, B., Phansalkar, A., Stefanovic, D., VanDrunen, T., von Dincklage, D., Wiedermann, B.: The DaCapo benchmarks: Java benchmarking development and analysis. In: Tarr, P.L., Cook, W.R. (eds.) Proceedings of the 21st Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2006, October 22–26, 2006, Portland, Oregon, USA, pp. 169–190. ACM (2006)

23. Boland, T., Black, P.E.: Juliet 1.1 C/C++ and Java test suite. Computer 45(10), 88–90 (2012)

24. Bonakdarpour, B., Smolka, S.A. (eds.): Runtime Verification—5th International Conference, RV 2014, Toronto, ON, Canada, September 22–25, 2014. Proceedings, Volume 8734 of Lecture Notes in Computer Science. Springer, Berlin (2014)

25. Boulé, M., Zilic, Z.: Incorporating efficient assertion checkers into hardware emulation. In: Proceedings of ICCD, pp. 221–228. IEEE Computer Society Press (2005)

26. Boulé, M., Zilic, Z.: Efficient automata-based assertion-checker synthesis of PSL properties. In: Proceedings of HLDVT, pp. 69–76. IEEE (2006)

27. Boulé, M., Zilic, Z.: Automata-based assertion-checker synthesis of PSL properties. ACM Trans. Des. Autom. Electron. Syst. 13(1), 4:1–4:21

28. Bufo, S., Bartocci, E., Sanguinetti, G., Borelli, M., Lucangelo, U., Bortolussi, L.: Temporal logic based monitoring of assisted ventilation in intensive care patients. In: Steffen, B., Margaria, T. (eds.) Proceedings of ISoLA 2014: 6th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Volume 8803 of LNCS, pp. 391–403 (2014)

29. Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Inf. Process. Lett. 40(5), 269–276 (1991)

30. Chen, F., Meredith, P., Jin, D., Rosu, G.: Efficient formalism-independent monitoring of parametric properties. In: IEEE/ACM International Conference on Automated Software Engineering (ASE’09), pp. 383–394 (2009)

31. Colombo, C., Pace, G., Abela, P.: Safer asynchronous runtime monitoring using compensations. Form. Methods Syst. Des. 41(3), 269–294 (2012)

32. Colombo, C., Pace, G.J.: Fast-forward runtime monitoring—an industrial case study. In: Runtime Verification, Third International Conference, RV 2012, Volume 7687 of Lecture Notes in Computer Science, pp. 214–228. Springer, Berlin (2012)

33. Colombo, C., Pace, G.J., Schneider, G.: Dynamic event-based runtime monitoring of real-time and contextual properties. In: Formal Methods for Industrial Critical Systems (FMICS), Volume 5596 of Lecture Notes in Computer Science, pp. 135–149. Springer, Berlin (2008)

34. Colombo, C., Pace, G.J., Schneider, G.: Larva—safer monitoring of real-time java programs (tool paper). In: Proceedings of the 2009 Seventh IEEE International Conference on Software Engineering and Formal Methods, SEFM ’09, pp. 33–37. IEEE Computer Society, Washington, DC (2009)

35. Dahan, A., Geist, D., Gluhovsky, L., Pidan, D., Shapir, G., Wolfsthal, Y., Benalycherif, L., Kamidem, R., Lahbib, Y.: Combining system level modeling with assertion based verification. In: Proceedings of ISQED 2005: Sixth International Symposium on Quality of Electronic Design, pp. 310–315. IEEE (2005)

36. D'Angelo, B., Sankaranarayanan, S., Sanchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: LOLA: runtime monitoring of synchronous systems. In: Proceedings of TIME 2005: The 12th International Symposium on Temporal Representation and Reasoning, pp. 166–174 (2005)

37. de Moura, L.M., Bjørner, Nikolaj.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29–April 6, 2008. Proceedings, Volume 4963 of Lecture Notes in Computer Science, pp. 337–340. Springer, Berlin (2008)

38. Decker, N., Leucker, M., Thoma, D.: jUnitRV—adding runtime verification to jUnit. In Brat, G., Rungta, N., Venet, A. (eds.) NASA Formal Methods, 5th International Symposium, NFM 2013, Mofett Field, CA, USA, May 14–16, 2013. Proceedings, Volume 7871 of Lecture Notes in Computer Science, pp. 459–464. Springer, Berlin (2013)

39. Decker, N., Leucker, M., Thoma, D.: Monitoring modulo theories. In: Ábrahám, E., Havelund, K. (eds.) Tools and Algorithms for the Construction and Analysis of Systems—20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5–13, 2014. Proceedings, Volume 8413 of Lecture Notes in Computer Science, pp. 341–356. Springer, Berlin (2014)

40. Decker, N., Leucker, M., Thoma, D.: Monitoring modulo theories. Int. J. Softw. Tools Technol. Transf. 18(2), 205–225 (2016)
11. Basin, D., Harvan, M., Klaedtke, F., Zălinescu, E.: Monitoring data usage in distributed systems. IEEE Trans. Softw. Eng. 39(10), 1403–1426 (2013)

12. Basin, D., Klaedtke, F., Müller, S., Zălinescu, E.: Monitoring metric first-order temporal properties. J. ACM 62(2), 15:1–15:45 (2015)

13. Basin, D., Klaedtke, F., Zălinescu, E.: Greedily computing associative aggregations on sliding windows. Inf. Process. Lett. 115(2), 186–192 (2015)

14. Basin, D.A., Caronni, G., Ereth, S., Harvan, M., Klaedtke, F., ManTEL, H.: Scalable offline monitoring. Form. Methods Syst. Des. 49(1–2), 75–108 (2016)

15. Basin, D.A., Klaedtke, F., Marinovic, S., Zălinescu, E.: Monitoring of temporal first-order properties with aggregations. Form. Methods Syst. Des. 46(3), 262–285 (2015)

16. Baudin, P., Filliâtre, J.-C., Marché, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C Specification Language. Version 1.8, March 2014

17. Benameur, A., Evans, N.S., Elder, M.C.: MINESTRONE: testing the SOUP. In: Kanich, C., Sherr, M. (eds.) In: 6th Workshop on Cyber Security Experimentation and Test, CSET ’13, Washington, DC, USA, August 12, 2013. USENIX Association (2013)

18. Berkovich, S., Bonakdarpour, B., Fischmeister, S.: GPU-based runtime verification. In: 27th IEEE International Symposium on Parallel and Distributed Processing, IPDPS 2013, Cambridge, MA, USA, May 20–24, 2013, pp. 1025–1036 (2013)

19. Beyer, D.: Competition on software verification—(SV-COMP). In: Proceedings of TACAS 2012: The 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems—18th International Conference, Volume 7214 of LNCS, pp. 504–524. Springer, Berlin (2012)

20. Beyer, D.: Status report on software verification—(competition summary SV-COMP 2014). In: Ábrahám, E., Havelund, K. (eds.) Tools and Algorithms for the Construction and Analysis of Systems—20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5–13, 2014. Proceedings, Volume 8413 of Lecture Notes in Computer Science, pp. 373–388. Springer, Berlin (2014)

21. Beyer, D.: Software verification and verifiable witnesses—(report on SV-COMP 2015). In: Proceedings of TACAS 2015: The 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, vol. 9035, pp. 401–416. Springer, Berlin (2015)

22. Blackburn, S.M., Garner, R., Hoffmann, C., Khan, A.M., McKinley, K.S., Bentzur, R., Diwan, A., Feinberg, D., Frampton, D., Guyer, S.Z., Hirzel, M., Hosking, A.L., Jump, M., Lee, H.B., Eliot, J., Moss, B., Phansalkar, A., Stefanovic, D., VanDrunen, T., von Dincklage, D., Wiedermann, B.: The DaCapo benchmarks: Java benchmarking development and analysis. In: Tarr, P.L., Cook, W.R. (eds.) Proceedings of the 21st Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2006, October 22–26, 2006, Portland, Oregon, USA, pp. 169–190. ACM (2006)

23. Boland, T., Black, P.E.: Juliet 1.1 C/C++ and Java test suite. Computer 45(10), 88–90 (2012)

24. Bonakdarpour, B., Smolka, S.A. (eds.): Runtime Verification—5th International Conference, RV 2014, Toronto, ON, Canada, September 22–25, 2014. Proceedings, Volume 8734 of Lecture Notes in Computer Science. Springer, Berlin (2014)

25. Boulé, M., Zilic, Z.: Incorporating efficient assertion checkers into hardware emulation. In: Proceedings of ICCD, pp. 221–228. IEEE Computer Society Press (2005)

26. Boulé, M., Zilic, Z.: Efficient automata-based assertion-checker synthesis of PSL properties. In: Proceedings of HLDVT, pp. 69–76. IEEE (2006)

27. Boulé, M., Zilic, Z.: Automata-based assertion-checker synthesis of PSL properties. ACM Trans. Des. Autom. Electron. Syst. 13(1), 4:1–4:21

28. Bufo, S., Bartocci, E., Sanguinetti, G., Borelli, M., Lucangelo, U., Bortolussi, L.: Temporal logic based monitoring of assisted ventilation in intensive care patients. In: Steffen, B., Margaria, T. (eds.) Proceedings of ISoLA 2014: 6th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Volume 8803 of LNCS, pp. 391–403 (2014)

29. Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Inf. Process. Lett. 40(5), 269–276 (1991)

30. Chen, F., Meredith, P., Jin, D., Rosu, G.: Efficient formalism-independent monitoring of parametric properties. In: IEEE/ACM International Conference on Automated Software Engineering (ASE’09), pp. 383–394 (2009)

31. Colombo, C., Pace, G., Abela, P.: Safer asynchronous runtime monitoring using compensations. Form. Methods Syst. Des. 41(3), 269–294 (2012)

32. Colombo, C., Pace, G.J.: Fast-forward runtime monitoring—an industrial case study. In: Runtime Verification, Third International Conference, RV 2012, Volume 7687 of Lecture Notes in Computer Science, pp. 214–228. Springer, Berlin (2012)

33. Colombo, C., Pace, G.J., Schneider, G.: Dynamic event-based runtime monitoring of real-time and contextual properties. In: Formal Methods for Industrial Critical Systems (FMICS), Volume 5596 of Lecture Notes in Computer Science, pp. 135–149. Springer, Berlin (2008)

34. Colombo, C., Pace, G.J., Schneider, G.: Larva—safer monitoring of real-time java programs (tool paper). In: Proceedings of the 2009 Seventh IEEE International Conference on Software Engineering and Formal Methods, SEFM ’09, pp. 33–37. IEEE Computer Society, Washington, DC (2009)

35. Dahan, A., Geist, D., Gluhovsky, L., Pidan, D., Shapir, G., Wolfsthal, Y., Benalycherif, L., Kamidem, R., Lahbib, Y.: Combining system level modeling with assertion based verification. In: Proceedings of ISQED 2005: Sixth International Symposium on Quality of Electronic Design, pp. 310–315. IEEE (2005)

36. D'Angelo, B., Sankaranarayanan, S., Sanchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: LOLA: runtime monitoring of synchronous systems. In: Proceedings of TIME 2005: The 12th International Symposium on Temporal Representation and Reasoning, pp. 166–174 (2005)

37. de Moura, L.M., Bjørner, Nikolaj.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29–April 6, 2008. Proceedings, Volume 4963 of Lecture Notes in Computer Science, pp. 337–340. Springer, Berlin (2008)

38. Decker, N., Leucker, M., Thoma, D.: jUnitRV—adding runtime verification to jUnit. In Brat, G., Rungta, N., Venet, A. (eds.) NASA Formal Methods, 5th International Symposium, NFM 2013, Mofett Field, CA, USA, May 14–16, 2013. Proceedings, Volume 7871 of Lecture Notes in Computer Science, pp. 459–464. Springer, Berlin (2013)

39. Decker, N., Leucker, M., Thoma, D.: Monitoring modulo theories. In: Ábrahám, E., Havelund, K. (eds.) Tools and Algorithms for the Construction and Analysis of Systems—20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5–13, 2014. Proceedings, Volume 8413 of Lecture Notes in Computer Science, pp. 341–356. Springer, Berlin (2014)

40. Decker, N., Leucker, M., Thoma, D.: Monitoring modulo theories. Int. J. Softw. Tools Technol. Transf. 18(2), 205–225 (2016)
41. Delahaye, M., Kosmatov, N., Signoles, J.: Common specification language for static and dynamic analysis of C programs. In: Proceedings of SAC ’13: The 28th Annual ACM Symposium on Applied Computing, pp. 1230–1235. ACM (2013)

42. Donzé, A., Maler, O., Bartocci, E., Nickovic, D., Grosu, R., Smolka, S.A.: On Temporal Logic and Signal Processing. In: Chakraborty, S., Mukund, M. (eds.) Proceedings of ATVA 2012: 10th International Symposium on Automated Technology for Verification and Analysis, Thiruvananthapuram, India, October 3–6, Volume 7561 of Lecture Notes in Computer Science, pp. 92–106. Springer, Berlin (2012)

43. Drago, I., Mellia, M., Munafò, M.M., Sperotto, A., Sadre, R., Pras, A.: Inside Dropbox: Understanding personal cloud storage services. In: Proceedings of the 12th ACM SIGCOMM Conference on Internet Measurement, IMC’12, pp. 481–494 (2012)

44. Falcone, Y.: You should better enforce than verify. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G.J., Rosu, G., Sokolsky, O., Tillmann, N. (eds.) Proceedings of the 1st International Conference on Runtime Verification (RV 2010), Volume 6418 of Lecture Notes in Computer Science, pp. 89–105. Springer, Berlin (2010)

45. Falcone, Y., Fernandez, J.-C., Mounier, L.: Runtime verification of safety-progress properties. In: 9th International Workshop on Runtime Verification. Selected Papers, vol. 5779, pp. 40–59 (2009)

46. Falcone, Y., Havelund, K., Reger, G.: A tutorial on runtime verification. In: Broy, M., Peled, D., Kalus, G. (eds.) Engineering Dependable Software Systems, Volume 34 of NATO Science for Peace and Security Series, D: Information and Communication Security, pp. 141–175. IOS Press, Amsterdam (2013)

47. Falcone, Y., Nickovic, D., Reger, G., Thoma, D.: Second international competition on runtime verification—crv 15. In: Runtime Verification—15th International Conference, RV 2015, Vienna, Austria, 2015. Proceedings, vol. 9333, pp. 365–382 (2015)

48. Finkbeiner, B., Kuhtz, L.: Monitor circuits for ltl with bounded and unbounded future. In: Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Volume 5779 of LNCS, pp. 60–75 (2009)

49. Fleming, P.J., Wallace, J.J.: How not to lie with statistics: the correct way to summarize benchmark results. Commun. ACM 29(3), 218–221 (1986)

50. Gol, E.A., Bartocci, E., Belta, C.: A formal methods approach to pattern synthesis in reaction diffusion systems. In: 53rd IEEE Conference on Decision and Control, CDC 2014, Los Angeles, CA, USA, December 15–17, 2014, pp. 108–113. IEEE (2014)

51. Havelund, K., Goldberg, A.: Verify your runs. In: Meyer, B., Woodcock, J. (eds.) Verified Software: Theories, Tools, Experiments, First IFIP TC 2/WG 2.3 Conference, VSTTE 2005, Zurich, Switzerland, October 10–13, 2005, Revised Selected Papers and Discussions, Volume 4171 of Lecture Notes in Computer Science, pp. 374–383. Springer, Berlin (2005)

52. Havelund, K., Reger, G.: Specification of parametric monitors—quantified event automata versus rule systems. In: Drechsler, R., Kühne, U. (eds.) Formal Modeling and Verification of Cyber-Physical Systems. Springer, Fachmedien Wiesbaden (2015)

53. Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D.: The RERS grey-box challenge 2012: analysis of event-condition-action systems. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change—5th International Symposium, ISOLA 2012, Heraklion, Crete, Greece, October 15–18, 2012, Proceedings, Part I, Volume 7609 of Lecture Notes in Computer Science, pp. 608–614. Springer, Berlin (2012)

54. Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D., Pasareanu, C.S.: Rigorous examination of reactive systems—the RERS challenges 2012 and 2013. STTT 16(5), 457–464 (2014)

55. Huisman, M., Klebanov, V., Monahan, R.: Verifythis 2012—a program verification competition. STTT 17(6), 647–657 (2015)

56. Jakobsson, A., Kosmatov, N., Signoles, J.: Fast as a shadow, expressive as a tree: hybrid memory monitoring for C. In: Wainwright, R.L., Corchado, J.M., Bechini, A., Hong, J. (eds.) Proceedings of the 30th Annual ACM Symposium on Applied Computing, Salamanca, Spain, April 13–17, 2015, pp. 1765–1772. ACM (2015)

57. Jaksic, S., Bartocci, E., Grosu, R., Kloibhofer, R., Nguyen, T., Ničković, D.: From signal temporal logic to FPGA monitors. In: Proceedings of MEMOCODE 2015: The ACM/IEEE International Conference on Formal Methods and Models for Codesign, pp. 218–227. IEEE (2015)

58. Jaksic, S., Bartocci, E., Grosu, R., Ničković, D.: Quantitative monitoring of STL with edit distance. In Proceedings of RV 2016: The 7th International Conference on Runtime Verification, LNCS, page to appear (2016)

59. Järvisalo, M., Berre, D.L., Roussel, O., Simon, L.: The international SAT solver competitions. AI Mag. 33(1), 89–94 (2012)

60. Jin, D., Meredith, P.O., Lee, C., Roșu, G.: JavaMOP: efficient parametric runtime monitoring framework. In: Proceedings of ICSE 2012: The 34th International Conference on Software Engineering, Zurich, Switzerland, June 2–9, pp. 1427–1430. IEEE Press (2012)

61. Jin, D., Meredith, P.O.N, Griffith, D., Roșu, G.: Garbage collection for monitoring parametric properties. In: Programming Language Design and Implementation (PLDI’11), pp. 415–424. ACM (2011)

62. Kalajdzic, K., Bartocci, E., Smolka, S.A., Stoller, S., Grosu, G.: Runtime verification with particle filtering. In: Proceedings of RV 2013, The fourth International Conference on Runtime Verification, INRIA Rennes, France, 24–27 September, 2013, Volume 8174 of Lecture Notes in Computer Science, pp. 149–166. Springer, Berlin (2013)

63. Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Form. Asp. Comput. 27(3), 573–609 (2015)

64. Kosmatov, N., Petiot, G., Signoles, J.: An optimized memory monitoring for runtime assertion checking of C programs. In: International Conference on Runtime Verification (RV’13), Volume 8174 of LNCS, pp. 167–182. Springer, Berlin (2013)

65. Laurila, J.L., Gatica-Perez, D., Aad, I., Blom, J., Bornet, O., Do, T.M.T., Dousse, O., Eberle, J., Miettinen, M.: From big smartphone data to worldwide research: the mobile data challenge. Pervasive Mob. Comput. 9(6), 752–771 (2013)

66. Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Log. Algebr. Program. 78(5), 293–303 (2009)

67. Luo, Q., Zhang, Y., Lee, C., Jin, D., Meredith, P.O.N, Serbanuta, T.-F., Rosu, G.: Rv-monitor: efficient parametric runtime verification with simultaneous properties. In: Bonakdarpour and Smolka [24], pp. 285–300 (2014)

68. Medhat, R., Joshi, Y., Bonakdarpour, B., Fischmeister, S.: Accelerated runtime verification of LTL specifications with counting semantics. CoRR abs/1411.2239 (2014)

69. Meredith, P.O.N., Jin, D., Griffith, D., Chen, F., Rosu, G.: An overview of the MOP runtime verification framework. STTT 14(3), 249–289 (2012)

70. Milewicz, R., Vanka, R., Tuck, J., Quinlan, D., Pirkelbauer, P.: Runtime checking c programs. In: Proceedings of the 30th Annual ACM Symposium on Applied Computing, pp. 2107–2114. ACM (2015)

71. Navabpour, S., Joshi, Y., Wu, C.W.W., Berkovich, S., Medhat, R., Bonakdarpour, B., Fischmeister, S.: RiTHM: a tool for enabling time-triggered runtime verification for C programs. In: ACM Symposium on the Foundations of Software Engineering (FSE), pp. 603–606 (2013)

72. Nguyen, T., Bartocci, E., Ničković, D., Grosu, R., Jaksic, S., Selyunin, K.: The HARMONIA project: hardware monitoring for
41. Delahaye, M., Kosmatov, N., Signoles, J.: Common specification language for static and dynamic analysis of C programs. In: Proceedings of SAC ’13: The 28th Annual ACM Symposium on Applied Computing, pp. 1230–1235. ACM (2013)

42. Donzé, A., Maler, O., Bartocci, E., Nickovic, D., Grosu, R., Smolka, S.A.: On Temporal Logic and Signal Processing. In: Chakraborty, S., Mukund, M. (eds.) Proceedings of ATVA 2012: 10th International Symposium on Automated Technology for Verification and Analysis, Thiruvananthapuram, India, October 3–6, Volume 7561 of Lecture Notes in Computer Science, pp. 92–106. Springer, Berlin (2012)

43. Drago, I., Mellia, M., Munafò, M.M., Sperotto, A., Sadre, R., Pras, A.: Inside Dropbox: Understanding personal cloud storage services. In: Proceedings of the 12th ACM SIGCOMM Conference on Internet Measurement, IMC’12, pp. 481–494 (2012)

44. Falcone, Y.: You should better enforce than verify. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G.J., Rosu, G., Sokolsky, O., Tillmann, N. (eds.) Proceedings of the 1st International Conference on Runtime Verification (RV 2010), Volume 6418 of Lecture Notes in Computer Science, pp. 89–105. Springer, Berlin (2010)

45. Falcone, Y., Fernandez, J.-C., Mounier, L.: Runtime verification of safety-progress properties. In: 9th International Workshop on Runtime Verification. Selected Papers, vol. 5779, pp. 40–59 (2009)

46. Falcone, Y., Havelund, K., Reger, G.: A tutorial on runtime verification. In: Broy, M., Peled, D., Kalus, G. (eds.) Engineering Dependable Software Systems, Volume 34 of NATO Science for Peace and Security Series, D: Information and Communication Security, pp. 141–175. IOS Press, Amsterdam (2013)

47. Falcone, Y., Nickovic, D., Reger, G., Thoma, D.: Second international competition on runtime verification—crv 15. In: Runtime Verification—15th International Conference, RV 2015, Vienna, Austria, 2015. Proceedings, vol. 9333, pp. 365–382 (2015)

48. Finkbeiner, B., Kuhtz, L.: Monitor circuits for ltl with bounded and unbounded future. In: Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Volume 5779 of LNCS, pp. 60–75 (2009)

49. Fleming, P.J., Wallace, J.J.: How not to lie with statistics: the correct way to summarize benchmark results. Commun. ACM 29(3), 218–221 (1986)

50. Gol, E.A., Bartocci, E., Belta, C.: A formal methods approach to pattern synthesis in reaction diffusion systems. In: 53rd IEEE Conference on Decision and Control, CDC 2014, Los Angeles, CA, USA, December 15–17, 2014, pp. 108–113. IEEE (2014)

51. Havelund, K., Goldberg, A.: Verify your runs. In: Meyer, B., Woodcock, J. (eds.) Verified Software: Theories, Tools, Experiments, First IFIP TC 2/WG 2.3 Conference, VSTTE 2005, Zurich, Switzerland, October 10–13, 2005, Revised Selected Papers and Discussions, Volume 4171 of Lecture Notes in Computer Science, pp. 374–383. Springer, Berlin (2005)

52. Havelund, K., Reger, G.: Specification of parametric monitors—quantified event automata versus rule systems. In: Drechsler, R., Kühne, U. (eds.) Formal Modeling and Verification of Cyber-Physical Systems. Springer, Fachmedien Wiesbaden (2015)

53. Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D.: The RERS grey-box challenge 2012: analysis of event-condition-action systems. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change—5th International Symposium, ISOLA 2012, Heraklion, Crete, Greece, October 15–18, 2012, Proceedings, Part I, Volume 7609 of Lecture Notes in Computer Science, pp. 608–614. Springer, Berlin (2012)

54. Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D., Pasareanu, C.S.: Rigorous examination of reactive systems—the RERS challenges 2012 and 2013. STTT 16(5), 457–464 (2014)

55. Huisman, M., Klebanov, V., Monahan, R.: Verifythis 2012—a program verification competition. STTT 17(6), 647–657 (2015)

56. Jakobsson, A., Kosmatov, N., Signoles, J.: Fast as a shadow, expressive as a tree: hybrid memory monitoring for C. In: Wainwright, R.L., Corchado, J.M., Bechini, A., Hong, J. (eds.) Proceedings of the 30th Annual ACM Symposium on Applied Computing, Salamanca, Spain, April 13–17, 2015, pp. 1765–1772. ACM (2015)

57. Jaksic, S., Bartocci, E., Grosu, R., Kloibhofer, R., Nguyen, T., Ničković, D.: From signal temporal logic to FPGA monitors. In: Proceedings of MEMOCODE 2015: The ACM/IEEE International Conference on Formal Methods and Models for Codesign, pp. 218–227. IEEE (2015)

58. Jaksic, S., Bartocci, E., Grosu, R., Ničković, D.: Quantitative monitoring of STL with edit distance. In Proceedings of RV 2016: The 7th International Conference on Runtime Verification, LNCS, page to appear (2016)

59. Järvisalo, M., Berre, D.L., Roussel, O., Simon, L.: The international SAT solver competitions. AI Mag. 33(1), 89–94 (2012)

60. Jin, D., Meredith, P.O., Lee, C., Roșu, G.: JavaMOP: efficient parametric runtime monitoring framework. In: Proceedings of ICSE 2012: The 34th International Conference on Software Engineering, Zurich, Switzerland, June 2–9, pp. 1427–1430. IEEE Press (2012)

61. Jin, D., Meredith, P.O.N, Griffith, D., Roșu, G.: Garbage collection for monitoring parametric properties. In: Programming Language Design and Implementation (PLDI’11), pp. 415–424. ACM (2011)

62. Kalajdzic, K., Bartocci, E., Smolka, S.A., Stoller, S., Grosu, G.: Runtime verification with particle filtering. In: Proceedings of RV 2013, The fourth International Conference on Runtime Verification, INRIA Rennes, France, 24–27 September, 2013, Volume 8174 of Lecture Notes in Computer Science, pp. 149–166. Springer, Berlin (2013)

63. Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Form. Asp. Comput. 27(3), 573–609 (2015)

64. Kosmatov, N., Petiot, G., Signoles, J.: An optimized memory monitoring for runtime assertion checking of C programs. In: International Conference on Runtime Verification (RV’13), Volume 8174 of LNCS, pp. 167–182. Springer, Berlin (2013)

65. Laurila, J.L., Gatica-Perez, D., Aad, I., Blom, J., Bornet, O., Do, T.M.T., Dousse, O., Eberle, J., Miettinen, M.: From big smartphone data to worldwide research: the mobile data challenge. Pervasive Mob. Comput. 9(6), 752–771 (2013)

66. Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Log. Algebr. Program. 78(5), 293–303 (2009)

67. Luo, Q., Zhang, Y., Lee, C., Jin, D., Meredith, P.O.N, Serbanuta, T.-F., Rosu, G.: Rv-monitor: efficient parametric runtime verification with simultaneous properties. In: Bonakdarpour and Smolka [24], pp. 285–300 (2014)

68. Medhat, R., Joshi, Y., Bonakdarpour, B., Fischmeister, S.: Accelerated runtime verification of LTL specifications with counting semantics. CoRR abs/1411.2239 (2014)

69. Meredith, P.O.N., Jin, D., Griffith, D., Chen, F., Rosu, G.: An overview of the MOP runtime verification framework. STTT 14(3), 249–289 (2012)

70. Milewicz, R., Vanka, R., Tuck, J., Quinlan, D., Pirkelbauer, P.: Runtime checking c programs. In: Proceedings of the 30th Annual ACM Symposium on Applied Computing, pp. 2107–2114. ACM (2015)

71. Navabpour, S., Joshi, Y., Wu, C.W.W., Berkovich, S., Medhat, R., Bonakdarpour, B., Fischmeister, S.: RiTHM: a tool for enabling time-triggered runtime verification for C programs. In: ACM Symposium on the Foundations of Software Engineering (FSE), pp. 603–606 (2013)

72. Nguyen, T., Bartocci, E., Ničković, D., Grosu, R., Jaksic, S., Selyunin, K.: The HARMONIA project: hardware monitoring for
automotive systems-of-systems. In: Steffen, B., Margaria, T. (eds.) Proceedings of ISoLA 2016: 7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Volume 9953 of LNCS, pp. 371–379. Springer, Berlin (2016)

73. Oliveira, A., Petkovich, J.-C., Reidemeister, T., Fischmeister, S.: DataMill: Rigorous performance evaluation made easy. In: Proceedings of ICPE 2013: The 4th ACM/SPEC International Conference on Performance Engineering, pp. 137–149. ACM (2013)

74. Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006: Formal Methods, 14th International Symposium on Formal Methods, Hamilton, Canada, August 21–27, 2006, Proceedings, Volume 4085 of Lecture Notes in Computer Science, pp. 573–586. Springer, Berlin (2006)

75. Reger, G., Cruz, H.C., Rydeheard, D.: MarQ: monitoring at runtime with QEA. In: Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’15) (2015)

76. Reinbacher, T., Függer, M., Brauer, J.: Runtime verification of embedded real-time systems. Form. Methods Syst. Des. 44(3), 230–239 (2014)

77. Reinbacher, T., Rozier, K.Y., Schuman, J.: Temporal-logic based runtime observer pairs for system health management of real-time systems. In: Proceedings of TACAS 2014, Volume 8413 of LNCS, pp. 357–372. Springer, Berlin (2014)

78. Schordan, M., Prantl, A.: Combining static analysis and state transition graphs for verification of event-condition-action systems in the RERS 2012 and 2013 challenges. STTT 16(5), 493–505 (2014)

79. Selyunin, K., Nguyen, T., Bartocci, E., Ničković, D., Grosu, R.: Monitoring of MTL specifications With IBM’s spiking-neuron model. In: Proceedings of DATE 2016: The 19th Design, Automation and Test in Europe Conference and Exhibition, pp. 924–929. IEEE (2016)

80. Signoles, J.: E-ACSL: Executable ANSI/ISO C Specification Language, Version 1.5-4, March 2014. http://frama-c.com/download/e-acsl/e-acsl.pdf

81. Signoles, J.: E-ACSL User Manual, March 2014. http://frama-c.com/download/e-acsl/e-acsl-manual.pdf

82. Sokolsky, O., Havelund, K., Lee, I.: Introduction to the special section on runtime verification. STTT 14(3), 243–247 (2012)

83. Stoller, S.D., Bartocci, E., Seyster, J., Grosu, R., Havelund, K., Smolka, S.A., Zadok, E.: Runtime verification with state estimation. In: Proceedings of RV 2011. The Second International Conference on Runtime verification, San Francisco, CA, USA, Volume 7186 of Lecture Notes in Computer Science, pp. 193–207. Springer, Berlin (2011)

84. Sutcliffe, G.: The 5th IJCAR automated theorem proving system competition—CASC-J5. AI Commun. 24(1), 75–89 (2011)

85. Zink, M., Kyoungwon, S., Gu, Y., Kurose, J.: Characteristics of youtube network traffic at a campus network—measurements, models, and implications. Comput. Netw. 53(4), 501–514 (2009)
automotive systems-of-systems. In: Steffen, B., Margaria, T. (eds.) Proceedings of ISoLA 2016: 7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Volume 9953 of LNCS, pp. 371–379. Springer, Berlin (2016)

73. Oliveira, A., Petkovich, J.-C., Reidemeister, T., Fischmeister, S.: DataMill: Rigorous performance evaluation made easy. In: Proceedings of ICPE 2013: The 4th ACM/SPEC International Conference on Performance Engineering, pp. 137–149. ACM (2013)

74. Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006: Formal Methods, 14th International Symposium on Formal Methods, Hamilton, Canada, August 21–27, 2006, Proceedings, Volume 4085 of Lecture Notes in Computer Science, pp. 573–586. Springer, Berlin (2006)

75. Reger, G., Cruz, H.C., Rydeheard, D.: MarQ: monitoring at runtime with QEA. In: Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’15) (2015)

76. Reinbacher, T., Függer, M., Brauer, J.: Runtime verification of embedded real-time systems. Form. Methods Syst. Des. 44(3), 230–239 (2014)

77. Reinbacher, T., Rozier, K.Y., Schuman, J.: Temporal-logic based runtime observer pairs for system health management of real-time systems. In: Proceedings of TACAS 2014, Volume 8413 of LNCS, pp. 357–372. Springer, Berlin (2014)

78. Schordan, M., Prantl, A.: Combining static analysis and state transition graphs for verification of event-condition-action systems in the RERS 2012 and 2013 challenges. STTT 16(5), 493–505 (2014)

79. Selyunin, K., Nguyen, T., Bartocci, E., Ničković, D., Grosu, R.: Monitoring of MTL specifications With IBM’s spiking-neuron model. In: Proceedings of DATE 2016: The 19th Design, Automation and Test in Europe Conference and Exhibition, pp. 924–929. IEEE (2016)

80. Signoles, J.: E-ACSL: Executable ANSI/ISO C Specification Language, Version 1.5-4, March 2014. http://frama-c.com/download/e-acsl/e-acsl.pdf

81. Signoles, J.: E-ACSL User Manual, March 2014. http://frama-c.com/download/e-acsl/e-acsl-manual.pdf

82. Sokolsky, O., Havelund, K., Lee, I.: Introduction to the special section on runtime verification. STTT 14(3), 243–247 (2012)

83. Stoller, S.D., Bartocci, E., Seyster, J., Grosu, R., Havelund, K., Smolka, S.A., Zadok, E.: Runtime verification with state estimation. In: Proceedings of RV 2011. The Second International Conference on Runtime verification, San Francisco, CA, USA, Volume 7186 of Lecture Notes in Computer Science, pp. 193–207. Springer, Berlin (2011)

84. Sutcliffe, G.: The 5th IJCAR automated theorem proving system competition—CASC-J5. AI Commun. 24(1), 75–89 (2011)

85. Zink, M., Kyoungwon, S., Gu, Y., Kurose, J.: Characteristics of youtube network traffic at a campus network—measurements, models, and implications. Comput. Netw. 53(4), 501–514 (2009)