# First international Competition on Runtime Verification: rules, benchmarks, tools, and final results of CRV 2014

E. Bartocci, Y. Falcone, B. Bonakdarpour, C. Colombo, N. Decker, K.

Havelund, Y. Joshi, F. Klaedtke, R. Milewicz, G. Reger, et al.

## ► To cite this version:

E. Bartocci, Y. Falcone, B. Bonakdarpour, C. Colombo, N. Decker, et al. First international Competition on Runtime Verification: rules, benchmarks, tools, and final results of CRV 2014. International Journal on Software Tools for Technology Transfer, 2017, 21, pp.31-70. 10.1007/s10009-017-0454-5 . cea-01845191

HAL Id: cea-01845191

https://cea.hal.science/cea-01845191

Submitted on 20 Feb 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
# First international Competition on Runtime Verification: rules, benchmarks, tools, and final results of CRV 2014

E. Bartocci, Y. Falcone, B. Bonakdarpour, C. Colombo, N. Decker, K.

Havelund, Y. Joshi, F. Klaedtke, R. Milewicz, G. Reger, et al.

## ► To cite this version:

E. Bartocci, Y. Falcone, B. Bonakdarpour, C. Colombo, N. Decker, et al. First international Competition on Runtime Verification: rules, benchmarks, tools, and final results of CRV 2014. International Journal on Software Tools for Technology Transfer, 2017, 21, pp.31-70. 10.1007/s10009-017-0454-5 . cea-01845191

HAL Id: cea-01845191

https://cea.hal.science/cea-01845191v1

Submitted on 20 Feb 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
<figure><img src="image_2.png" /></figure>

# First international Competition on Runtime Verification: rules, benchmarks, tools, and final results of CRV 2014

Ezio Bartocci<fnref n="1" /> · Yliès Falcone<fnref n="2" />,<fnref n="3" /> · Borzoo Bonakdarpour<fnref n="4" /> · Christian Colombo<fnref n="5" /> ·
Normann Decker<fnref n="6" /> · Klaus Havelund<fnref n="7" /> · Yogi Joshi<fnref n="8" /> · Felix Klaedtke<fnref n="9" /> ·
Reed Milewicz<fnref n="10" /> · Giles Reger<fnref n="11" /> · Grigore Rosu<fnref n="3" /> · Julien Signoles<fnref n="12" /> ·
Daniel Thoma<fnref n="6" /> · Eugen Zalinescu<fnref n="13" /> · Yi Zhang<fnref n="3" />

Published online: 7 April 2017

© The Author(s) 2017. This article is an open access publication

**Abstract** The first international Competition on Runtime Verification (CRV) was held in September 2014, in Toronto, Canada, as a satellite event of the 14th international conference on Runtime Verification (RV’14). The event was organized in three tracks: (1) offline monitoring, (2) online monitoring of C programs, and (3) online monitoring of Java programs. In this paper, we report on the phases and rules, a description of the participating teams and their submitted benchmark, the (full) results, as well as the lessons learned from the competition.

**Keywords** Runtime Verification · Software competition · Monitoring · Benchmarks

<figure><img src="image_3.png" /></figure>

Ezio Bartocci
ezio.bartocci@tuwien.ac.at

## 1 Introduction

Runtime verification [6, 45, 46, 51, 66, 82],<fnref n="1" /> from here on referred to as RV, refers to a class of lightweight scalable techniques for analysis of execution traces. The core idea is to instrument a program to emit events during its execution, which are then processed by a monitor. This paper focuses specifically on *specification-based* trace analysis, where execution traces are verified against formal specifications written in formal logical systems. Other forms of RV, not treated in this paper, include for example *algorithm-based* trace analysis, such as detecting concurrency issues such as data races and deadlocks; *specification mining* from traces; and *trace visualization*.

Specification-based trace analysis is a topic of particular interest due to the many different logics and supporting tools that have been developed over the last decade, including the following to just mention a few [5, 6, 9, 10, 28, 34, 36, 38, 41, 42, 44, 50, 67, 70, 71, 74, 75]. Unlike proof-oriented techniques, such as theorem proving or model checking, that aim to verify exhaustively whether a property is satisfied for all the possible system executions, specification-based RV automatically checks only if a single execution trace is correct, and it therefore does not suffer from the classic manual labor and state-explosion problems, typically associated with theorem proving and model checking. The achieved scalability of course comes at the cost of less coverage.

As illustrated in Fig. 1, an RV process consists of three main steps: *monitor synthesis*, *system instrumentation*, and *monitoring*. In the first step, a monitor is synthesized from a requirement expressed in a formal specification language (e.g., regular expression, automaton, rule set, grammar, or temporal logic formula), or it is programmed directly in a

<footnote n="1">1 TU Wien, Vienna, Austria</footnote>

<footnote n="2">2 Inria, CNRS, Laboratoire d'Informatique de Grenoble, Univ. Grenoble-Alpes, 38000 Grenoble, France</footnote>

<footnote n="3">3 University of Illinois at Urbana-Champaign, Champaign, IL, USA</footnote>

<footnote n="4">4 McMaster University, Hamilton, Canada</footnote>

<footnote n="5">5 University of Malta, Msida, Malta</footnote>

<footnote n="6">6 Lübeck University, Lübeck, Germany</footnote>

<footnote n="7">7 Jet Propulsion Laboratory, NASA, Pasadena, CA, USA</footnote>

<footnote n="8">8 University of Waterloo, Waterloo, Canada</footnote>

<footnote n="9">9 NEC Laboratories Europe, Heidelberg, Germany</footnote>

<footnote n="10">10 University of Alabama at Birmingham, Birmingham, AL, USA</footnote>

<footnote n="11">11 University of Manchester, Manchester, UK</footnote>

<footnote n="12">12 CEA, LIST, Software Security Laboratory, PC 174, 91191 Gif-sur-Yvette, France</footnote>

<footnote n="13">13 ETH Zurich, Zurich, Switzerland</footnote>

<footnote n="1">¹ http://runtime-verification.org.</footnote>
<figure><img src="image_2.png" /></figure>

# First international Competition on Runtime Verification: rules, benchmarks, tools, and final results of CRV 2014

Ezio Bartocci<fnref n="1" /> · Yliès Falcone<fnref n="2" />,<fnref n="3" /> · Borzoo Bonakdarpour<fnref n="4" /> · Christian Colombo<fnref n="5" /> ·
Normann Decker<fnref n="6" /> · Klaus Havelund<fnref n="7" /> · Yogi Joshi<fnref n="8" /> · Felix Klaedtke<fnref n="9" /> ·
Reed Milewicz<fnref n="10" /> · Giles Reger<fnref n="11" /> · Grigore Rosu<fnref n="3" /> · Julien Signoles<fnref n="12" /> ·
Daniel Thoma<fnref n="6" /> · Eugen Zalinescu<fnref n="13" /> · Yi Zhang<fnref n="3" />

Published online: 7 April 2017

© The Author(s) 2017. This article is an open access publication

**Abstract** The first international Competition on Runtime Verification (CRV) was held in September 2014, in Toronto, Canada, as a satellite event of the 14th international conference on Runtime Verification (RV’14). The event was organized in three tracks: (1) offline monitoring, (2) online monitoring of C programs, and (3) online monitoring of Java programs. In this paper, we report on the phases and rules, a description of the participating teams and their submitted benchmark, the (full) results, as well as the lessons learned from the competition.

**Keywords** Runtime Verification · Software competition · Monitoring · Benchmarks

<figure><img src="image_3.png" /></figure>

Ezio Bartocci
ezio.bartocci@tuwien.ac.at

## 1 Introduction

Runtime verification [6, 45, 46, 51, 66, 82],<fnref n="1" /> from here on referred to as RV, refers to a class of lightweight scalable techniques for analysis of execution traces. The core idea is to instrument a program to emit events during its execution, which are then processed by a monitor. This paper focuses specifically on *specification-based* trace analysis, where execution traces are verified against formal specifications written in formal logical systems. Other forms of RV, not treated in this paper, include for example *algorithm-based* trace analysis, such as detecting concurrency issues such as data races and deadlocks; *specification mining* from traces; and *trace visualization*.

Specification-based trace analysis is a topic of particular interest due to the many different logics and supporting tools that have been developed over the last decade, including the following to just mention a few [5, 6, 9, 10, 28, 34, 36, 38, 41, 42, 44, 50, 67, 70, 71, 74, 75]. Unlike proof-oriented techniques, such as theorem proving or model checking, that aim to verify exhaustively whether a property is satisfied for all the possible system executions, specification-based RV automatically checks only if a single execution trace is correct, and it therefore does not suffer from the classic manual labor and state-explosion problems, typically associated with theorem proving and model checking. The achieved scalability of course comes at the cost of less coverage.

As illustrated in Fig. 1, an RV process consists of three main steps: *monitor synthesis*, *system instrumentation*, and *monitoring*. In the first step, a monitor is synthesized from a requirement expressed in a formal specification language (e.g., regular expression, automaton, rule set, grammar, or temporal logic formula), or it is programmed directly in a

<footnote n="1">1 TU Wien, Vienna, Austria</footnote>

<footnote n="2">2 Inria, CNRS, Laboratoire d'Informatique de Grenoble, Univ. Grenoble-Alpes, 38000 Grenoble, France</footnote>

<footnote n="3">3 University of Illinois at Urbana-Champaign, Champaign, IL, USA</footnote>

<footnote n="4">4 McMaster University, Hamilton, Canada</footnote>

<footnote n="5">5 University of Malta, Msida, Malta</footnote>

<footnote n="6">6 Lübeck University, Lübeck, Germany</footnote>

<footnote n="7">7 Jet Propulsion Laboratory, NASA, Pasadena, CA, USA</footnote>

<footnote n="8">8 University of Waterloo, Waterloo, Canada</footnote>

<footnote n="9">9 NEC Laboratories Europe, Heidelberg, Germany</footnote>

<footnote n="10">10 University of Alabama at Birmingham, Birmingham, AL, USA</footnote>

<footnote n="11">11 University of Manchester, Manchester, UK</footnote>

<footnote n="12">12 CEA, LIST, Software Security Laboratory, PC 174, 91191 Gif-sur-Yvette, France</footnote>

<footnote n="13">13 ETH Zurich, Zurich, Switzerland</footnote>

<footnote n="1">¹ http://runtime-verification.org.</footnote>
<figure><img src="image_4.png" /><figcaption>**Fig. 1** Runtime verification main phases</figcaption></figure>

general-purpose programming language [46,69]. A monitor is a program or a device that receives as input a sequence of events (observations) and emits verdicts regarding the satisfaction or violation of the requirement. In the second step, the system is instrumented using event information extracted from requirements. The instrumentation aims at ensuring that the relevant behavior of the system can be observed at runtime. In the third step, the program is executed with the instrumentation activated. In *online monitoring*, the monitor runs in parallel with (or is embedded into) the program, analyzing the event sequence as it is produced. In *offline monitoring*, the event sequence is written to persistent memory, for example a log file, which at a later point in time is analyzed by the monitor. In online monitoring, monitor verdicts can trigger fault protection code. In offline monitoring, verdicts can be summarized and visualized in reports, or trigger the execution of other programs. Instrumentation and monitoring generally increase the memory utilization and introduce a runtime overhead that may alter the timing-related behavior of the system under scrutiny. In real-time applications, overhead control strategies are generally necessary to mitigate the overhead by, for example, using static analysis to minimize instrumentation, or switching on and off the monitor [8, 62, 83].

During the last decade, many important tools and techniques have been developed. However, due to lack of standard benchmark suites as well as scientific evaluation methods to validate and test new techniques, we believe that the RV community is in pressing need to have an organized venue whose goal is to provide mechanisms for comparing different aspects of existing tools and techniques.

For these reasons, inspired by the success of similar events in other areas of computer-aided verification (e.g., SAT [59],

SV-COMP [20], SMT [2], RERS [53,54]), Ezio Bartocci, Borzoo Bonakdarpour, and Yliès Falcone organized the first international Competition on Runtime Verification (CRV 2014) with the aim to foster the process of comparison and evaluation of software runtime verification tools.

The objectives of CRV'14 were the following:

- To stimulate the development of new efficient and practical runtime verification tools and the maintenance of the already developed ones.

- To produce benchmark suites for runtime verification tools, by sharing case studies and programs that researchers and developers can use in the future to test and to validate their prototypes.

- To discuss the measures employed for comparing the tools.

- To compare different aspects of the tools running with different benchmarks and evaluating them using different criteria.

- To enhance the visibility of presented tools among different communities (verification, software engineering, distributed computing and cyber security) involved in software monitoring.

CRV'14 was held in September 2014, in Toronto, Canada, as a satellite event of the 14th international conference on Runtime Verification (RV'14). The event was organized in three tracks: (1) offline monitoring, (2) online monitoring of C programs, and (3) online monitoring of Java programs. This paper conveys the experience on the procedures, the rules, the participating teams, the benchmarks, the evaluation process and the results of CRV'14. This paper complements and significantly extends a preliminary report that was written before RV'14 [4].

*Paper organization* The rest of this paper is organized as follows: Section 2 gives an overview of the phases and the rules of the competition. Section 3 introduces the participating teams. Section 4 presents the benchmarks used in all the three tracks of the competition. Section 5 defines the method used to compute the score. Section 6 reports on the results. Section 7 discusses lessons learned. Finally, Sect. 8 concludes the paper.

## 2 Phases and rules of the competition

Taking inspiration from the software verification competition (SVCOMP) started in 2012 [19], we have arranged the overall process along three different phases for each track:

1. *collection of benchmarks* (Sect. 2.1),

2. *training and monitor submissions* (Sect. 2.2),

<figure><img src="image_5.png" /></figure>
<figure><img src="image_4.png" /><figcaption>**Fig. 1** Runtime verification main phases</figcaption></figure>

general-purpose programming language [46,69]. A monitor is a program or a device that receives as input a sequence of events (observations) and emits verdicts regarding the satisfaction or violation of the requirement. In the second step, the system is instrumented using event information extracted from requirements. The instrumentation aims at ensuring that the relevant behavior of the system can be observed at runtime. In the third step, the program is executed with the instrumentation activated. In *online monitoring*, the monitor runs in parallel with (or is embedded into) the program, analyzing the event sequence as it is produced. In *offline monitoring*, the event sequence is written to persistent memory, for example a log file, which at a later point in time is analyzed by the monitor. In online monitoring, monitor verdicts can trigger fault protection code. In offline monitoring, verdicts can be summarized and visualized in reports, or trigger the execution of other programs. Instrumentation and monitoring generally increase the memory utilization and introduce a runtime overhead that may alter the timing-related behavior of the system under scrutiny. In real-time applications, overhead control strategies are generally necessary to mitigate the overhead by, for example, using static analysis to minimize instrumentation, or switching on and off the monitor [8, 62, 83].

During the last decade, many important tools and techniques have been developed. However, due to lack of standard benchmark suites as well as scientific evaluation methods to validate and test new techniques, we believe that the RV community is in pressing need to have an organized venue whose goal is to provide mechanisms for comparing different aspects of existing tools and techniques.

For these reasons, inspired by the success of similar events in other areas of computer-aided verification (e.g., SAT [59],

SV-COMP [20], SMT [2], RERS [53,54]), Ezio Bartocci, Borzoo Bonakdarpour, and Yliès Falcone organized the first international Competition on Runtime Verification (CRV 2014) with the aim to foster the process of comparison and evaluation of software runtime verification tools.

The objectives of CRV’14 were the following:

- To stimulate the development of new efficient and practical runtime verification tools and the maintenance of the already developed ones.

- To produce benchmark suites for runtime verification tools, by sharing case studies and programs that researchers and developers can use in the future to test and to validate their prototypes.

- To discuss the measures employed for comparing the tools.

- To compare different aspects of the tools running with different benchmarks and evaluating them using different criteria.

- To enhance the visibility of presented tools among different communities (verification, software engineering, distributed computing and cyber security) involved in software monitoring.

CRV’14 was held in September 2014, in Toronto, Canada, as a satellite event of the 14th international conference on Runtime Verification (RV’14). The event was organized in three tracks: (1) offline monitoring, (2) online monitoring of C programs, and (3) online monitoring of Java programs. This paper conveys the experience on the procedures, the rules, the participating teams, the benchmarks, the evaluation process and the results of CRV’14. This paper complements and significantly extends a preliminary report that was written before RV’14 [4].

*Paper organization* The rest of this paper is organized as follows: Section 2 gives an overview of the phases and the rules of the competition. Section 3 introduces the participating teams. Section 4 presents the benchmarks used in all the three tracks of the competition. Section 5 defines the method used to compute the score. Section 6 reports on the results. Section 7 discusses lessons learned. Finally, Sect. 8 concludes the paper.

## 2 Phases and rules of the competition

Taking inspiration from the software verification competition (SVCOMP) started in 2012 [19], we have arranged the overall process along three different phases for each track:

1. *collection of benchmarks* (Sect. 2.1),

2. *training and monitor submissions* (Sect. 2.2),

<figure><img src="image_5.png" /></figure>
an_event_name, a_field_name = a_value, a_field_name = a_value
an_event_name, a_field_name = a_value, a_field_name = a_value

<caption>**Fig. 2** Example of trace in CSV format</caption>

### 3. evaluation (Sect. 2.3).

The first phase (Dec. 15, 2013–March 1, 2014) aims to stimulate each team to develop at most five benchmarks per track that may challenge the tools of the other teams. In the second phase (March 2, 2014–May 30, 2014), the teams have the possibility to further develop and improve their tools using the benchmarks of the adversary teams. This cross-fertilizes new ideas between the teams, since each team is exposed to the same problems and challenges previously faced by the other teams. The goal of the last phase (June 1, 2014–Sept. 23, 2014) is to provide a framework for a fair and automatic evaluation of the participating tools. In the following, we describe the phases in more detail.

## 2.1 Collection of benchmarks

In the first phase, the teams participating in each track prepare and upload in a shared repository a set of benchmarks. We now provide a description of the requirements of a benchmark for the online and offline monitoring tracks.

*Online monitoring of C and Java programs tracks* In the case of C and Java tracks, each benchmark contribution is required to contain the following:

- A *program package* containing the program source code (the program to be monitored), a script to compile it, a script to run the executable, and an English description of the functionality of the program.

- A *specification package* containing a collection of files, each describing a property: an English description of the property, a formal representation of it in the logical system supported by the team, instrumentation information, and the expected verdict (the evaluation of the property on the program execution).

The instrumentation information describes of a mapping from concrete events in the program (for example method calls) to the abstract events referred to in the specification.

For instance, if one considers the *HasNext* property on Java iterators (that a call of the method *next* on an iterator should always be preceded by a call of the method *hasNext* that returns true), the mapping should indicate that the *hasNext* event in the property refers to a call to the *hasNext()* method on an *Iterator* object, and similarly for the *next* event. Several concrete events can be mapped to the same abstract event.

*Offline monitoring track.* In the case of offline track, each benchmark contribution is required to contain the following:

- A *trace*, in either CSV, custom, or XML format, and a description of the event kinds contained in the trace. The three trace formats are illustrated in Fig. 2, 3, and 4.

- A *specification package* containing a collection of files describing a property: an English description of the property, a formal representation of it in the logical system supported by the team, and the expected verdict (the evaluation of the property on the trace).

an_event_name
a_field_name = a_value
a_field_name = a_value

an_event_name
a_field_name = a_value
a_field_name = a_value

<caption>**Fig. 3** Example of trace in custom format</caption>

<log>
  <event>
    <name>an_event_name</name>
    <field>
      <name>a_field_name</name>
      <value>a_value</value>
    </field>
    <field>
      <name>a_field_name</name>
      <value>a_value</value>
    </field>
  </event>
  <event>
    <name>an_event_name</name>
    <field>
      <name>a_field_name</name>
      <value>a_value</value>
    </field>
    <field>
      <name>a_field_name</name>
      <value>a_value</value>
    </field>
  </event>
</log>

<caption>**Fig. 4** Example of trace in XML format</caption>
an_event_name, a_field_name = a_value, a_field_name = a_value
an_event_name, a_field_name = a_value, a_field_name = a_value

<caption>**Fig. 2** Example of trace in CSV format</caption>

### 3. evaluation (Sect. 2.3).

The first phase (Dec. 15, 2013–March 1, 2014) aims to stimulate each team to develop at most five benchmarks per track that may challenge the tools of the other teams. In the second phase (March 2, 2014–May 30, 2014), the teams have the possibility to further develop and improve their tools using the benchmarks of the adversary teams. This cross-fertilizes new ideas between the teams, since each team is exposed to the same problems and challenges previously faced by the other teams. The goal of the last phase (June 1, 2014–Sept. 23, 2014) is to provide a framework for a fair and automatic evaluation of the participating tools. In the following, we describe the phases in more detail.

## 2.1 Collection of benchmarks

In the first phase, the teams participating in each track prepare and upload in a shared repository a set of benchmarks. We now provide a description of the requirements of a benchmark for the online and offline monitoring tracks.

*Online monitoring of C and Java programs tracks* In the case of C and Java tracks, each benchmark contribution is required to contain the following:

- A *program package* containing the program source code (the program to be monitored), a script to compile it, a script to run the executable, and an English description of the functionality of the program.

- A *specification package* containing a collection of files, each describing a property: an English description of the property, a formal representation of it in the logical system supported by the team, instrumentation information, and the expected verdict (the evaluation of the property on the program execution).

The instrumentation information describes of a mapping from concrete events in the program (for example method calls) to the abstract events referred to in the specification.

For instance, if one considers the *HasNext* property on Java iterators (that a call of the method *next* on an iterator should always be preceded by a call of the method *hasNext* that returns true), the mapping should indicate that the *hasNext* event in the property refers to a call to the *hasNext()* method on an *Iterator* object, and similarly for the *next* event. Several concrete events can be mapped to the same abstract event.

*Offline monitoring track.* In the case of offline track, each benchmark contribution is required to contain the following:

- A *trace*, in either CSV, custom, or XML format, and a description of the event kinds contained in the trace. The three trace formats are illustrated in Fig. 2, 3, and 4.

- A *specification package* containing a collection of files describing a property: an English description of the property, a formal representation of it in the logical system supported by the team, and the expected verdict (the evaluation of the property on the trace).

an_event_name
a_field_name = a_value
a_field_name = a_value

an_event_name
a_field_name = a_value
a_field_name = a_value

<caption>**Fig. 3** Example of trace in custom format</caption>

<log>
  <event>
    <name>an_event_name</name>
    <field>
      <name>a_field_name</name>
      <value>a_value</value>
    </field>
    <field>
      <name>a_field_name</name>
      <value>a_value</value>
    </field>
  </event>
  <event>
    <name>an_event_name</name>
    <field>
      <name>a_field_name</name>
      <value>a_value</value>
    </field>
    <field>
      <name>a_field_name</name>
      <value>a_value</value>
    </field>
  </event>
</log>

<caption>**Fig. 4** Example of trace in XML format</caption>
## 2.2 Training phase and monitor collection phase

During this phase, all participants can apply their tools to all the available benchmarks in the repository, and possibly modify their tools to improve their performance. At the phase end, they submit their contributions as monitors for the benchmarks. A contribution is related one of the benchmarks uploaded in the first phase and contains a monitor for the property in the benchmark together with two scripts, one for building and one for running the monitor.

## 2.3 Benchmark evaluation phase

The evaluation of the teams' contributions is performed on DataMill,<fnref n="2" /> [73] a distributed infrastructure for computer performance experimentation targeted at scientists that are interested in performance evaluation. DataMill aims to allow the user to easily produce robust and reproducible results at low cost. DataMill executes experiments multiple times, obtaining average values, and generally deploys results from research on how to set up such experiments. Each participant has the possibility to set up and try their tool using DataMill. The final evaluation is performed by the competition organizers.

# 3 Participating teams and tools

In this section, we provide a description of participating teams and tools.

## 3.1 C track

Table 1 summarizes the teams and tools participating in the track of online monitoring of C programs. The tools are described in the rest of this subsection.

### 3.1.1 RITHM

RITHM (Runtime Time-triggered Heterogeneous Monitoring) [71] is a tool for runtime verification of C programs. RITHM is developed at the Real-time Embedded Software Group at University of Waterloo, Canada.

RITHM takes a C program and a set of properties expressed in a fragment of first-order LTL as input. RITHM instruments the C program with respect to the definition of predicates supplied along with LTL properties, and it synthesizes an LTL monitor. The program then can be monitored at runtime by the synthesized monitor, where the instrumented program sends events in its execution trace to the monitor.

<table><caption>**Table 1** Tools participating in online monitoring of C programs track</caption><thead><tr><td>Tool</td><td>References</td><td>Contact person</td><td>Affiliation</td></tr></thead><tbody><tr><td>RITHM</td><td>[71]</td><td>B. Bonakdarpour</td><td>McMaster Univ. and U. Waterloo, Canada</td></tr><tr><td>E- ACSL</td><td>[41]</td><td>J. Signoles</td><td>CEA LIST, France</td></tr><tr><td>RTC</td><td>[70]</td><td>R. Milewicz</td><td>University of Alabama at Birmingham, USA</td></tr></tbody></table>

Further, RITHM monitors a fragment of first-order LTL specifications as described in [68]. RITHM monitor can be run on Graphics Processing Units or multicore Central Processing Units [68] for accelerating the verification of an execution trace [18].

### 3.1.2 E-ACSL

E- ACSL [41] (Executable ANSI/ISO C Specification Language) is both a formal specification language and a monitoring tool which are designed and developed at CEA LIST, Software Security Labs. They are integrated to the Frama-C platform [63], which is an extensible and collaborative platform dedicated to source-code analysis of C software.

The formal specification language is a large subset of the ACSL specification language [16] and is designed in a way that each annotation can be verified at runtime [80]. It is a behavioral first-order typed specification language which supports, in particular, function contracts, assertions, user-defined predicates and built-in predicates (such as $\ \ \ \ \ valid(p)$ which indicates that the pointer $p$ points to a memory location that the program can write and read).

The plug-in E- ACSL [81] automatically converts a C program $p_1$ specified with E- ACSL annotations to another C program $p_2$ which monitors each annotation of $p_1$ at runtime. More precisely, for each annotation $a$, $p_2$ computes the truth value of $a$ and passes it as an argument to the C function `e_acslenk assert`. By default, this function stops the program execution with a precise error message if $a$ is 0 (i.e., false) and just continues the execution otherwise. The generated code is linked against a dedicated memory library which can efficiently compute the validity of complex memory-related properties (e.g., use-after-free or initialization of variables) [56,64].

### 3.1.3 RTC

RTC [70] (Runtime checking for C programs) is a runtime monitoring tool that instruments unsafe code and monitors

<footnote n="2">² http://datamill.uwaterloo.ca.</footnote>
## 2.2 Training phase and monitor collection phase

During this phase, all participants can apply their tools to all the available benchmarks in the repository, and possibly modify their tools to improve their performance. At the phase end, they submit their contributions as monitors for the benchmarks. A contribution is related one of the benchmarks uploaded in the first phase and contains a monitor for the property in the benchmark together with two scripts, one for building and one for running the monitor.

## 2.3 Benchmark evaluation phase

The evaluation of the teams' contributions is performed on DataMill,<fnref n="2" /> [73] a distributed infrastructure for computer performance experimentation targeted at scientists that are interested in performance evaluation. DataMill aims to allow the user to easily produce robust and reproducible results at low cost. DataMill executes experiments multiple times, obtaining average values, and generally deploys results from research on how to set up such experiments. Each participant has the possibility to set up and try their tool using DataMill. The final evaluation is performed by the competition organizers.

# 3 Participating teams and tools

In this section, we provide a description of participating teams and tools.

## 3.1 C track

Table 1 summarizes the teams and tools participating in the track of online monitoring of C programs. The tools are described in the rest of this subsection.

### 3.1.1 RITHM

RITHM (Runtime Time-triggered Heterogeneous Monitoring) [71] is a tool for runtime verification of C programs. RITHM is developed at the Real-time Embedded Software Group at University of Waterloo, Canada.

RITHM takes a C program and a set of properties expressed in a fragment of first-order LTL as input. RITHM instruments the C program with respect to the definition of predicates supplied along with LTL properties, and it synthesizes an LTL monitor. The program then can be monitored at runtime by the synthesized monitor, where the instrumented program sends events in its execution trace to the monitor.

<table><caption>Table 1 Tools participating in online monitoring of C programs track</caption><thead><tr><td>Tool</td><td>References</td><td>Contact person</td><td>Affiliation</td></tr></thead><tbody><tr><td>RITHM</td><td>[71]</td><td>B. Bonakdarpour</td><td>McMaster Univ. and U. Waterloo, Canada</td></tr><tr><td>E- ACSL</td><td>[41]</td><td>J. Signoles</td><td>CEA LIST, France</td></tr><tr><td>RTC</td><td>[70]</td><td>R. Milewicz</td><td>University of Alabama at Birmingham, USA</td></tr></tbody></table>

Further, RITHM monitors a fragment of first-order LTL specifications as described in [68]. RITHM monitor can be run on Graphics Processing Units or multicore Central Processing Units [68] for accelerating the verification of an execution trace [18].

### 3.1.2 E-ACSL

E- ACSL [41] (Executable ANSI/ISO C Specification Language) is both a formal specification language and a monitoring tool which are designed and developed at CEA LIST, Software Security Labs. They are integrated to the Frama-C platform [63], which is an extensible and collaborative platform dedicated to source-code analysis of C software.

The formal specification language is a large subset of the ACSL specification language [16] and is designed in a way that each annotation can be verified at runtime [80]. It is a behavioral first-order typed specification language which supports, in particular, function contracts, assertions, user-defined predicates and built-in predicates (such as $\text{valid}(p)$ which indicates that the pointer $p$ points to a memory location that the program can write and read).

The plug-in E- ACSL [81] automatically converts a C program $p_1$ specified with E- ACSL annotations to another C program $p_2$ which monitors each annotation of $p_1$ at runtime. More precisely, for each annotation $a$, $p_2$ computes the truth value of $a$ and passes it as an argument to the C function `e_acslenkert`. By default, this function stops the program execution with a precise error message if $a$ is 0 (i.e., false) and just continues the execution otherwise. The generated code is linked against a dedicated memory library which can efficiently compute the validity of complex memory-related properties (e.g., use-after-free or initialization of variables) [56,64].

### 3.1.3 RTC

RTC [70] (Runtime checking for C programs) is a runtime monitoring tool that instruments unsafe code and monitors

<footnote n="2">² http://datamill.uwaterloo.ca.</footnote>
<table><caption>**Table 2** Tools participating in online monitoring of Java programs track</caption><thead><tr><td>Tool</td><td>References</td><td>Contact person</td><td>Affiliation</td></tr></thead><tbody><tr><td>LARVA</td><td>[34]</td><td>C. Colombo</td><td>University of Malta, Malta</td></tr><tr><td>JUNIT<sup>RV</sup></td><td>[38,39]</td><td>D. Thoma</td><td>ISP, University of Lübeck, Germany</td></tr><tr><td>JAVAMOP</td><td>[60]</td><td>G. Roşu</td><td>U. of Illinois at Urbana Champaign, USA</td></tr><tr><td>QEA, MARQ</td><td>[3]</td><td>G. Reger</td><td>University of Manchester, UK</td></tr></tbody></table>

the program execution. RTC is built on top of the ROSE compiler infrastructure. RTC finds memory bugs, arithmetic overflows and under-flows, and runtime type violations. Most of the instrumentations are directly added to the source file and only require a minimal runtime system. As a result, the instrumented code remains portable. The team behind RTC consists of researchers from the University of Alabama at Birmingham, North Carolina State University, Lawrence Livermore National Laboratory, and Matlab.

## 3.2 Java track

Table 2 summarizes the teams and tools participating in the track of online monitoring of Java programs. The tools are described in the rest of this subsection.

### 3.2.1 Larva

Larva [34] is a Java and AspectJ-based RV tool whose specification language (DATEs [33]) is a flavour of automata enriched with stopwatches. The automata are symbolic in that they allow the use of local state in terms of Java variables and data structures. Furthermore, Larva allows the full use of Java for the specification of conditions which decide when transitions trigger. Similarly, for each transition, an action can be specified so that when it triggers, the local state can be updated, possibly also carrying out actions on the monitored system, e.g., to handle a detected problem.

The tool design and development has been inspired by case studies in the financial industry [32] where there are frequent soft real-time constraints such as limits on the amount of money spent within a particular period and entity life-cycles such as limiting the kind of operations users are allowed to perform while suspended.

Over the years, a set of tools have been built to support and augment Larva including conversion from other specification languages (such as duration calculus [29]) to Larva specification language, and extensions to support event extraction from databases as well as saving the monitor state to a database when it is not feasible to keep it in memory [31].

### 3.2.2 JUnitRV

JUnitRV [38] is a tool extending the unit testing framework JUnit with runtime verification capabilities. Roughly, JUnitRV

provides a new annotation @Monitors listing monitors that are synthesized from temporal specifications. The monitors check whether the currently executed tests satisfy the correctness properties underlying the monitors. As such, JUnit's concept of plain assert-based verification limited to checking properties of single states of a program is extended significantly toward checking properties of complete execution paths.

To support specifications beyond propositional properties, JUnitRV uses a generic approach to enhance traditional runtime verification techniques toward first-order theories in order to reason about data. This allows especially for the verification of multi-threaded, object-oriented systems. The framework lifts the monitor synthesis for propositional temporal logics to a temporal logic over structures within some first-order theory. To evaluate such temporal properties, SMT (Satisfiability Modulo Theory) solving and classical monitoring of propositional temporal properties is combined. JUnitRV implements this framework for linear-time temporal logic based on the Z3 SMT solver [37]. The framework is described in detail in [39,40].

### 3.2.3 JAVAMOP

JAVAMOP, with its core component RV-Monitor [67], is a formalism-independent RV tool designed to effectively monitor multiple parametric properties simultaneously. It is developed both by University of Illinois at Urbana Champaign and Runtime Verification, Inc.<fnref n="3" />

JAVAMOP specifications support a variety of formalisms such as finite state machine, linear temporal logic, string rewriting systems, etc., which gives users a lot of freedom to express different kinds of properties. At the same time, several optimizations [30,61,67] were proposed to make monitors creation, garbage collection, and internal data structure access more efficient. Besides, JAVAMOP can generate a single Java agent out of multiple specifications. The Java agent can be easily attached to the Java virtual machine to run with Java programs. All these efforts make JAVAMOP capable of monitoring multiple properties simultaneously on large Java applications.

<footnote n="3">³ https://www runtimeverification.com.</footnote>
<table><caption>**Table 2** Tools participating in online monitoring of Java programs track</caption><thead><tr><td>Tool</td><td>References</td><td>Contact person</td><td>Affiliation</td></tr></thead><tbody><tr><td>LARVA</td><td>[34]</td><td>C. Colombo</td><td>University of Malta, Malta</td></tr><tr><td>JUNIT<sup>RV</sup></td><td>[38,39]</td><td>D. Thoma</td><td>ISP, University of Lübeck, Germany</td></tr><tr><td>JAVAMOP</td><td>[60]</td><td>G. Roşu</td><td>U. of Illinois at Urbana Champaign, USA</td></tr><tr><td>QEA, MARQ</td><td>[3]</td><td>G. Reger</td><td>University of Manchester, UK</td></tr></tbody></table>

the program execution. RTC is built on top of the ROSE compiler infrastructure. RTC finds memory bugs, arithmetic overflows and under-flows, and runtime type violations. Most of the instrumentations are directly added to the source file and only require a minimal runtime system. As a result, the instrumented code remains portable. The team behind RTC consists of researchers from the University of Alabama at Birmingham, North Carolina State University, Lawrence Livermore National Laboratory, and Matlab.

## 3.2 Java track

Table 2 summarizes the teams and tools participating in the track of online monitoring of Java programs. The tools are described in the rest of this subsection.

### 3.2.1 Larva

Larva [34] is a Java and AspectJ-based RV tool whose specification language (DATEs [33]) is a flavour of automata enriched with stopwatches. The automata are symbolic in that they allow the use of local state in terms of Java variables and data structures. Furthermore, Larva allows the full use of Java for the specification of conditions which decide when transitions trigger. Similarly, for each transition, an action can be specified so that when it triggers, the local state can be updated, possibly also carrying out actions on the monitored system, e.g., to handle a detected problem.

The tool design and development has been inspired by case studies in the financial industry [32] where there are frequent soft real-time constraints such as limits on the amount of money spent within a particular period and entity life-cycles such as limiting the kind of operations users are allowed to perform while suspended.

Over the years, a set of tools have been built to support and augment Larva including conversion from other specification languages (such as duration calculus [29]) to Larva specification language, and extensions to support event extraction from databases as well as saving the monitor state to a database when it is not feasible to keep it in memory [31].

### 3.2.2 JUnit<sup>RV</sup>

JUnitRV [38] is a tool extending the unit testing framework JUnit with runtime verification capabilities. Roughly, JUnitRV

provides a new annotation @Monitors listing monitors that are synthesized from temporal specifications. The monitors check whether the currently executed tests satisfy the correctness properties underlying the monitors. As such, JUnit's concept of plain assert-based verification limited to checking properties of single states of a program is extended significantly toward checking properties of complete execution paths.

To support specifications beyond propositional properties, JUnitRV uses a generic approach to enhance traditional runtime verification techniques toward first-order theories in order to reason about data. This allows especially for the verification of multi-threaded, object-oriented systems. The framework lifts the monitor synthesis for propositional temporal logics to a temporal logic over structures within some first-order theory. To evaluate such temporal properties, SMT (Satisfiability Modulo Theory) solving and classical monitoring of propositional temporal properties is combined. JUnitRV implements this framework for linear-time temporal logic based on the Z3 SMT solver [37]. The framework is described in detail in [39,40].

### 3.2.3 JAVAMOP

JAVAMOP, with its core component RV-Monitor [67], is a formalism-independent RV tool designed to effectively monitor multiple parametric properties simultaneously. It is developed both by University of Illinois at Urbana Champaign and Runtime Verification, Inc.<fnref n="3" />

JAVAMOP specifications support a variety of formalisms such as finite state machine, linear temporal logic, string rewriting systems, etc., which gives users a lot of freedom to express different kinds of properties. At the same time, several optimizations [30,61,67] were proposed to make monitors creation, garbage collection, and internal data structure access more efficient. Besides, JAVAMOP can generate a single Java agent out of multiple specifications. The Java agent can be easily attached to the Java virtual machine to run with Java programs. All these efforts make JAVAMOP capable of monitoring multiple properties simultaneously on large Java applications.

<footnote n="3">³ https://www run timeverification.com.</footnote>
<table><caption>**Table 3** Tools participating in the offline monitoring track</caption><thead><tr><td>Tool</td><td>References</td><td>Contact person</td><td>Affiliation</td></tr></thead><tbody><tr><td>RITHM2</td><td>[71]</td><td>B. Bonakdarpour</td><td>McMaster Univ. and U. Waterloo, Canada</td></tr><tr><td>MONPOLY</td><td>[10]</td><td>E. Zălinescu</td><td>ETH Zurich, Switzerland</td></tr><tr><td>STEPR</td><td></td><td>N. Decker</td><td>ISP, University of Lübeck, Germany</td></tr><tr><td>QEA, MARQ</td><td>[3]</td><td>G. Reger</td><td>University of Manchester, UK</td></tr></tbody></table>

### 3.2.4 Monitoring at runtime with QEA (MARQ)

The MARQ tool [75] monitors specifications written in the Quantified Event Automata (QEAs) [3] specification language. It has been developed at the University of Manchester by Giles Reger and Helena Cuenca Cruz with input from David Rydeheard.

QEAs combine a quantifier list with an extended finite state machine over parametric events. Trace acceptance is defined via the *trace slicing* approach, extended to allow existential quantification and a notion of free variables.

*Syntax of QEA* We give a brief explanation of the syntax used and will not repeat it below. A QEA consists of a quantifier list and a state machine. They can have multiple **Forall** or **Exists** quantifications with an optional **Where** constraint restricting the considered values. States can be **accept** states, indicating that a trace is accepted if *any* path reaches an **accept** state. There are two other state modifiers: **skip** indicates that missing transitions are self-looping; **next** indicates that missing transitions implicitly go to the **failure** state. The failure state is an implicit non-accept state with no outgoing transitions; once the failure state has been reached, success (for this binding) is not possible.

The MARQ tool implements an incremental monitoring algorithm for QEAs. A *structural specialization* module attempts to specialize the algorithm based on structural properties of the specification. Singly quantified specifications are directly indexed; otherwise, a general *symbol-based* indexing approach is used.

For monitoring Java programs, MARQ is designed to be used with AspectJ. It also implements mechanisms for dealing with garbage collection and can either use reference or semantic identity for monitored objects.

## 3.3 Offline track

Table 3 summarizes the tools teams and participating in the track of offline monitoring. The tools are described in the rest of this subsection.

### 3.3.1 RITHM-2

RITHM [71], as previously described, is a tool for runtime verification. In addition to *online* monitoring of C programs,

it can process execution traces for performing *offline* verification. Further, RITHM was extended to process execution traces in XML and CSV formats as per the schemas described in Sect. 2.1. RITHM is designed for monitoring specifications described using LTL or a first-order fragment of LTL [68].

### 3.3.2 MONPOLY

MONPOLY [10] is a monitoring tool for checking compliance of IT systems with respect to policies specifying normal or compulsory system behavior. The tool has been developed as part of several research projects on runtime monitoring and enforcement in the Information Security group at ETH Zurich. MONPOLY is open source, written in OCaml.

Policies are given as formulas of an expressive safety fragment of metric first-order temporal logic (MFOTL), including dedicated operators for expressing aggregations on data items. The first-order fragment is well suited for formalizing relations between data items, while the temporal operators are used to express quantitative temporal constraints on the occurrence or non-occurrence of events at different time points. An event streams can be input through a log file or a UNIX pipeline, which MONPOLY processes iteratively, either offline or online. The stream can be seen as a sequence of timestamped databases, each of them consisting of the events that have occurred in the system execution at a point in time. Each tuple in one of the databases' relations represents a system action together with the involved data. For a given event stream and a formula, MONPOLY outputs all the policy violations (Table 4).

Further details on MFOTL and the tool's underlying monitoring algorithm are given in [12, 13, 15]. MONPOLY has been used in real-world case studies, in collaboration with Nokia Research Lausanne [11] and with Google Zurich [14]. Further performance evaluation and comparison with alternative approaches can be found in [12] and [15].

### 3.3.3 STEPR

STEPR is a prototype log file analysis tool developed at the Institute for Software Engineering and Programming Languages, University of Lübeck, Germany.<fnref n="4" /> It is loosely based on the Lola stream processing verification language proposed by d'Angelo et al. [36]. The log file is considered as an input

<figure><img src="image_6.png" /></figure>

<footnote n="4">⁴ www.isp.uni-luebeck.de.</footnote>
<table><caption>**Table 3** Tools participating in the offline monitoring track</caption><thead><tr><td>Tool</td><td>References</td><td>Contact person</td><td>Affiliation</td></tr></thead><tbody><tr><td>RITHM2</td><td>[71]</td><td>B. Bonakdarpour</td><td>McMaster Univ. and U. Waterloo, Canada</td></tr><tr><td>MONPOLY</td><td>[10]</td><td>E. Zălinescu</td><td>ETH Zurich, Switzerland</td></tr><tr><td>STEPR</td><td></td><td>N. Decker</td><td>ISP, University of Lübeck, Germany</td></tr><tr><td>QEA, MARQ</td><td>[3]</td><td>G. Reger</td><td>University of Manchester, UK</td></tr></tbody></table>

### 3.2.4 Monitoring at runtime with QEA (MARQ)

The MARQ tool [75] monitors specifications written in the Quantified Event Automata (QEAs) [3] specification language. It has been developed at the University of Manchester by Giles Reger and Helena Cuenca Cruz with input from David Rydeheard.

QEAs combine a quantifier list with an extended finite state machine over parametric events. Trace acceptance is defined via the *trace slicing* approach, extended to allow existential quantification and a notion of free variables.

*Syntax of QEA* We give a brief explanation of the syntax used and will not repeat it below. A QEA consists of a quantifier list and a state machine. They can have multiple **Forall** or **Exists** quantifications with an optional **Where** constraint restricting the considered values. States can be **accept** states, indicating that a trace is accepted if *any* path reaches an **accept** state. There are two other state modifiers: **skip** indicates that missing transitions are self-looping; **next** indicates that missing transitions implicitly go to the **failure** state. The failure state is an implicit non-accept state with no outgoing transitions; once the failure state has been reached, success (for this binding) is not possible.

The MARQ tool implements an incremental monitoring algorithm for QEAs. A *structural specialization* module attempts to specialize the algorithm based on structural properties of the specification. Singly quantified specifications are directly indexed; otherwise, a general *symbol-based* indexing approach is used.

For monitoring Java programs, MARQ is designed to be used with AspectJ. It also implements mechanisms for dealing with garbage collection and can either use reference or semantic identity for monitored objects.

## 3.3 Offline track

Table 3 summarizes the tools teams and participating in the track of offline monitoring. The tools are described in the rest of this subsection.

### 3.3.1 RITHM-2

RITHM [71], as previously described, is a tool for runtime verification. In addition to *online* monitoring of C programs,

it can process execution traces for performing *offline* verification. Further, RITHM was extended to process execution traces in XML and CSV formats as per the schemas described in Sect. 2.1. RITHM is designed for monitoring specifications described using LTL or a first-order fragment of LTL [68].

### 3.3.2 MONPOLY

MONPOLY [10] is a monitoring tool for checking compliance of IT systems with respect to policies specifying normal or compulsory system behavior. The tool has been developed as part of several research projects on runtime monitoring and enforcement in the Information Security group at ETH Zurich. MONPOLY is open source, written in OCaml.

Policies are given as formulas of an expressive safety fragment of metric first-order temporal logic (MFOTL), including dedicated operators for expressing aggregations on data items. The first-order fragment is well suited for formalizing relations between data items, while the temporal operators are used to express quantitative temporal constraints on the occurrence or non-occurrence of events at different time points. An event streams can be input through a log file or a UNIX pipeline, which MONPOLY processes iteratively, either offline or online. The stream can be seen as a sequence of timestamped databases, each of them consisting of the events that have occurred in the system execution at a point in time. Each tuple in one of the databases' relations represents a system action together with the involved data. For a given event stream and a formula, MONPOLY outputs all the policy violations (Table 4).

Further details on MFOTL and the tool's underlying monitoring algorithm are given in [12, 13, 15]. MONPOLY has been used in real-world case studies, in collaboration with Nokia Research Lausanne [11] and with Google Zurich [14]. Further performance evaluation and comparison with alternative approaches can be found in [12] and [15].

### 3.3.3 STEPR

STEPR is a prototype log file analysis tool developed at the Institute for Software Engineering and Programming Languages, University of Lübeck, Germany.<fnref n="4" /> It is loosely based on the Lola stream processing verification language proposed by d'Angelo et al. [36]. The log file is considered as an input

<figure><img src="image_6.png" /></figure>

<footnote n="4">⁴ www.isp.uni-luebeck.de.</footnote>
<table><caption>**Table 4** URLs where it is possible to download the tools participating to the competition</caption><thead><tr><td>Tool</td><td>Available at (URL)</td></tr></thead><tbody><tr><td>E- ACSL (ver. 0.4.1)</td><td>http://frama-c.com/download/e-acsl/e-acsl-0.4.1.tar.gz</td></tr><tr><td>JAVAMOP (VER. 4.2)</td><td>http://fsl.cs.illinois.edu/index.php/JavaMOP4</td></tr><tr><td>JUNIT<sup>RV</sup></td><td>https://www.isp.uni-luebeck.de/junitrv</td></tr><tr><td>LARVA</td><td>http://www.cs.um.edu.mt/svrg/Tools/LARVA/</td></tr><tr><td>MONPOLY</td><td>http://sourceforge.net/projects/monpoly</td></tr><tr><td>QEA(MARQ)</td><td>https://github.com/selig/qea</td></tr><tr><td>RITHM/RITHM2</td><td>https://uwaterloo.ca/embedded-software-group/projects/rithm</td></tr><tr><td>RTC</td><td>https://github.com/rose-compiler/rose/tree/master/projects/RTC</td></tr><tr><td>STEPR</td><td>http://www.isp.uni-luebeck.de/stepr</td></tr></tbody></table>

stream of data, and the user can use stream operations to define new streams and combine them in an algebraic fashion. Assertions can be specified on such streams that, once violated, make the program report an error. Streams can further be declared as output streams that are written to report files in various formats and verbosity. They provide additional information on the exact position of the violation and error counts allowing for convenient analysis of the occurred deviations. STEPR is written in the Scala programming language<fnref n="5" /> and provides a Scala-internal domain-specific language for specifications. The full power of Scala can be used for specifying further stream operation if needed.

### 3.3.4 Monitoring at runtime with QEA (MARQ)

MARQ is described in Sect. 3.2.4 as a tool for monitoring Java programs. Here, we give details of how it can be used for offline monitoring.

MARQ can parse trace files in either CSV or XML formats (JSON traces are not supported). The CSV parser has been hand-written to optimize the translation of events into the internal representation. The XML parser makes use of standard Java library features. As a consequence, the XML parser is relatively inefficient compared to the CSV parser. Therefore, we prefer the CSV format and would normally first translate traces into this format.

One can use different events in the specification and the trace when monitoring with MARQ. For example, an abstract event in the specification can have a different name, arity, and parameter order as the corresponding event in the trace. Furthermore, multiple events in the trace can be mapped to an abstract event, and vice-versa. To handle this, MARQ requires the use of so-called *translators* that can translate event names as well as permuting or dropping event parameters. Additionally, translators can be used to *interpret* values, i.e., to parse strings into integer objects. Translators are required when a

parameter value should be treated as its interpreted value, as is the case with a counter.

## 3.4 Summary

Table 5 summarizes some of the features of the tools presented in this section. A checkmark sign (✓) indicates a supported feature. Four categories of features are presented. *Input requirement specification* The first category concerns the specification of the input requirement that a tool can monitor. The entry *user-enabled* in Table 5 is ticked when the corresponding tool allows the user to specify the requirement. In this case, the tool supports one or more specification languages that allow the user to write flexible requirements to be monitored. The entry *built-in* is ticked when the corresponding tool has a number of built-in specifications that can be checked at runtime without any specification effort by the user. Table 5 lists next some of the following common specification language features: *automata-based*, *regular-expressions-based*, and *logic-based*, supporting *logical-time* where only the relative ordering of events is important or *real-time* where the event occurrence times are also relevant. The language can support *propositional events* and/or *parametric events*, depending on whether runtime events cannot carry or, respectively, can carry data values. Generally, more expressive specification languages require more complex monitoring algorithms. The monitoring code can be generated from a high-level specification language or directly implemented in a programming language.

*Instrumentation* The entry *own instrumentation* indicates that the tool implements its own instrumentation phase of the RV process. The entry *relies on AspectJ* indicates that the tool uses AspectJ for instrumentation purposes. The entry *relies on another technique* indicates that the tool uses a third-party technique and/or tool different from AspectJ for instrumentation purposes.

*Monitored systems* The entries in this category have their expected meaning and indicate the kind of systems that the tool can monitor (C programs, Java programs, or traces).

<footnote n="5">⁵ www.scala-lang.org.</footnote>
<table><caption>**Table 4** URLs where it is possible to download the tools participating to the competition</caption><thead><tr><td>Tool</td><td>Available at (URL)</td></tr></thead><tbody><tr><td>E- ACSL (ver. 0.4.1)</td><td>http://frama-c.com/download/e-acsl/e-acsl-0.4.1.tar.gz</td></tr><tr><td>JAVAMOP (VER. 4.2)</td><td>http://fsl.cs.illinois.edu/index.php/JavaMOP4</td></tr><tr><td>JUNIT<sup>RV</sup></td><td>https://www.isp.uni-luebeck.de/junitrv</td></tr><tr><td>LARVA</td><td>http://www.cs.um.edu.mt/svrg/Tools/LARVA/</td></tr><tr><td>MONPOLY</td><td>http://sourceforge.net/projects/monpoly</td></tr><tr><td>QEA(MARQ)</td><td>https://github.com/selig/qea</td></tr><tr><td>RITHM/RITHM2</td><td>https://uwaterloo.ca/embedded-software-group/projects/rithm</td></tr><tr><td>RTC</td><td>https://github.com/rose-compiler/rose/tree/master/projects/RTC</td></tr><tr><td>STEPR</td><td>http://www.isp.uni-luebeck.de/stepr</td></tr></tbody></table>

stream of data, and the user can use stream operations to define new streams and combine them in an algebraic fashion. Assertions can be specified on such streams that, once violated, make the program report an error. Streams can further be declared as output streams that are written to report files in various formats and verbosity. They provide additional information on the exact position of the violation and error counts allowing for convenient analysis of the occurred deviations. STEPR is written in the Scala programming language<fnref n="5" /> and provides a Scala-internal domain-specific language for specifications. The full power of Scala can be used for specifying further stream operation if needed.

### 3.3.4 Monitoring at runtime with QEA (MARQ)

MARQ is described in Sect. 3.2.4 as a tool for monitoring Java programs. Here, we give details of how it can be used for offline monitoring.

MARQ can parse trace files in either CSV or XML formats (JSON traces are not supported). The CSV parser has been hand-written to optimize the translation of events into the internal representation. The XML parser makes use of standard Java library features. As a consequence, the XML parser is relatively inefficient compared to the CSV parser. Therefore, we prefer the CSV format and would normally first translate traces into this format.

One can use different events in the specification and the trace when monitoring with MARQ. For example, an abstract event in the specification can have a different name, arity, and parameter order as the corresponding event in the trace. Furthermore, multiple events in the trace can be mapped to an abstract event, and vice-versa. To handle this, MARQ requires the use of so-called *translators* that can translate event names as well as permuting or dropping event parameters. Additionally, translators can be used to *interpret* values, i.e., to parse strings into integer objects. Translators are required when a

parameter value should be treated as its interpreted value, as is the case with a counter.

## 3.4 Summary

Table 5 summarizes some of the features of the tools presented in this section. A checkmark sign (✓) indicates a supported feature. Four categories of features are presented. *Input requirement specification* The first category concerns the specification of the input requirement that a tool can monitor. The entry *user-enabled* in Table 5 is ticked when the corresponding tool allows the user to specify the requirement. In this case, the tool supports one or more specification languages that allow the user to write flexible requirements to be monitored. The entry *built-in* is ticked when the corresponding tool has a number of built-in specifications that can be checked at runtime without any specification effort by the user. Table 5 lists next some of the following common specification language features: *automata-based*, *regular-expressions-based*, and *logic-based*, supporting *logical-time* where only the relative ordering of events is important or *real-time* where the event occurrence times are also relevant. The language can support *propositional events* and/or *parametric events*, depending on whether runtime events cannot carry or, respectively, can carry data values. Generally, more expressive specification languages require more complex monitoring algorithms. The monitoring code can be generated from a high-level specification language or directly implemented in a programming language.

*Instrumentation* The entry *own instrumentation* indicates that the tool implements its own instrumentation phase of the RV process. The entry *relies on AspectJ* indicates that the tool uses AspectJ for instrumentation purposes. The entry *relies on another technique* indicates that the tool uses a third-party technique and/or tool different from AspectJ for instrumentation purposes.

*Monitored systems* The entries in this category have their expected meaning and indicate the kind of systems that the tool can monitor (C programs, Java programs, or traces).

<footnote n="5">⁵ www.scala-lang.org.</footnote>
<table><caption>**Table 5** Summary of features of the tools</caption><thead><tr><th>Participating tool</th><th>User-enabled in</th><th>Built-in events</th><th>Propositional Parametric events</th><th>Automated events</th><th>Automated based</th><th>Logic-based</th><th>Regular Expressions-based</th><th>Logical-time</th><th>Real-time</th><th>Own instrumentation</th><th>Relies on another technique</th><th>C programs</th><th>Java programs</th><th>Traces-Triggered</th><th>Event triggered</th><th>Monitoring mode</th></tr></thead><tbody><tr><td>RITHM</td><td>✓</td><td>✓</td><td>✓</td><td></td><td></td><td>✓</td><td></td><td>✓</td><td></td><td>✓</td><td></td><td></td><td></td><td>✓</td><td>✓</td><td></td></tr><tr><td>E-ACSL</td><td>✓</td><td>✓</td><td>✓</td><td></td><td></td><td>✓</td><td></td><td></td><td></td><td>✓</td><td></td><td></td><td></td><td>✓</td><td>✓</td><td></td></tr><tr><td>RTC</td><td>✓</td><td>✓</td><td></td><td></td><td></td><td>✓</td><td></td><td></td><td></td><td>✓</td><td></td><td></td><td>✓</td><td>✓</td><td>✓</td><td></td></tr><tr><td>LARVA</td><td>✓</td><td></td><td>✓</td><td>✓</td><td></td><td></td><td></td><td></td><td></td><td>✓</td><td></td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td></td></tr><tr><td>JUNIT<sup>RV</sup></td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td>✓</td><td>✓</td><td></td><td>✓</td><td></td></tr><tr><td>JAVAMOP</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td>✓</td><td>✓</td></tr><tr><td>MONPOLY</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td>✓</td><td>✓</td></tr><tr><td>STEPR</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td>✓</td><td>✓</td></tr><tr><td>MARQ</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td>✓</td><td>✓</td></tr></tbody></table>

**Monitoring mode** The entry *time triggered* indicates that the stream of observations from the system is obtained through sampling. The entry *event triggered* indicates that the stream of observations is obtained following the execution of events in the system.

## 4 Benchmarks for the monitoring competition

In this section, we provide a description of the benchmarks provided by participants.

The benchmarks can be downloaded by cloning the repository and following the instructions available at: https://gitlab.inria.fr/crv14/benchmarks.

In the following, for each benchmark, we describe the related program and property.

### 4.1 C track

#### 4.1.1 Maximum chunk size in Dropbox connections

This benchmark is provided by RiTHM team.

**Description of the monitored program** The program simulates Dropbox connections. The program uses the dataset described in [43] to run the simulation.

**Description of the property** The property states that for all connections, it is always the case that *chunk size* (used to split files) is less than or equal to 999,999. The property is formalized using a fragment of first-order LTL [68] as follows:

$$ \forall \text{connection} : G(\text{chunksize}(\text{connection}) \leq 999,999). $$

#### 4.1.2 Changes in the chunk size of Dropbox connections

This benchmark is provided by RiTHM team.

**Description of the monitored program** The benchmark uses the same program as the one in the benchmark described in Sect. 4.1.1.

**Description of the property** The property states that for all connections, it is always the case that when the *chunk size* becomes strictly larger than 10,000, its value eventually becomes less than or equal to 10,000. The property is formalized using a fragment of first-order LTL [68] as follows:

$$ \begin{array}{l} \forall \text{connection} : G(\text{chunksize}(\text{connection}) > 10,000) \\ \implies F(\text{chunksize}(\text{connection}) \leq 10,000). \end{array} $$

#### 4.1.3 Maximum bandwidth of Youtube connections

**Description of the monitored program** The program simulates Youtube connections. The program uses the dataset described in [85] to run the simulation.

<figure><img src="image_7.png" /></figure>
<table><caption>**Table 5** Summary of features of the tools</caption><thead><tr><th>Participating tool</th><th>User-enabled in</th><th>Built-in events</th><th>Propositional Parametric events</th><th>Automata-based</th><th>Logic-based</th><th>Regular Expressions-based</th><th>Logical-Real-time</th><th>Own instrumentation</th><th>Relies on another technique</th><th>C programs</th><th>Java programs</th><th>Traces-Time triggered</th><th>Event triggered</th><th>Monitoring mode</th></tr></thead><tbody><tr><td>Input requirement specification</td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td>Instrumentation</td><td></td><td></td><td></td><td></td><td></td><td></td></tr><tr><td>RITHM</td><td>✓</td><td>✓</td><td>✓</td><td></td><td>✓</td><td></td><td>✓</td><td>✓</td><td></td><td>✓</td><td></td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>E- ACSL</td><td>✓</td><td>✓</td><td>✓</td><td></td><td>✓</td><td></td><td>✓</td><td>✓</td><td></td><td>✓</td><td></td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>RTC</td><td>✓</td><td>✓</td><td>✓</td><td></td><td>✓</td><td></td><td>✓</td><td>✓</td><td></td><td>✓</td><td></td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>LARVA</td><td>✓</td><td>✓</td><td>✓</td><td></td><td>✓</td><td></td><td>✓</td><td>✓</td><td></td><td>✓</td><td></td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>JUNIT<sup>RV</sup></td><td>✓</td><td>✓</td><td>✓</td><td></td><td>✓</td><td></td><td>✓</td><td>✓</td><td></td><td>✓</td><td></td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>JAVAMOP</td><td>✓</td><td>✓</td><td>✓</td><td></td><td>✓</td><td></td><td>✓</td><td>✓</td><td></td><td>✓</td><td></td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>MONPOLY</td><td>✓</td><td>✓</td><td>✓</td><td></td><td>✓</td><td></td><td>✓</td><td>✓</td><td></td><td>✓</td><td></td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>STEPR</td><td>✓</td><td>✓</td><td>✓</td><td></td><td>✓</td><td></td><td>✓</td><td>✓</td><td></td><td>✓</td><td></td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>MARQ</td><td>✓</td><td>✓</td><td>✓</td><td></td><td>✓</td><td></td><td>✓</td><td>✓</td><td></td><td>✓</td><td></td><td>✓</td><td>✓</td><td>✓</td></tr></tbody></table>

**Monitoring mode** The entry *time triggered* indicates that the stream of observations from the system is obtained through sampling. The entry *event triggered* indicates that the stream of observations is obtained following the execution of events in the system.

## 4 Benchmarks for the monitoring competition

In this section, we provide a description of the benchmarks provided by participants.

The benchmarks can be downloaded by cloning the repository and following the instructions available at: https://gitlab.inria.fr/crv14/benchmarks.

In the following, for each benchmark, we describe the related program and property.

### 4.1 C track

#### 4.1.1 Maximum chunk size in Dropbox connections

This benchmark is provided by RiTHM team.

**Description of the monitored program** The program simulates Dropbox connections. The program uses the dataset described in [43] to run the simulation.

**Description of the property** The property states that for all connections, it is always the case that *chunk size* (used to split files) is less than or equal to 999,999. The property is formalized using a fragment of first-order LTL [68] as follows:

$$ \forall \text{connection} : G(\text{chunksize}(\text{connection}) \leq 999,999). $$

#### 4.1.2 Changes in the chunk size of Dropbox connections

This benchmark is provided by RiTHM team.

**Description of the monitored program** The benchmark uses the same program as the one in the benchmark described in Sect. 4.1.1.

**Description of the property** The property states that for all connections, it is always the case that when the *chunk size* becomes strictly larger than 10,000, its value eventually becomes less than or equal to 10,000. The property is formalized using a fragment of first-order LTL [68] as follows:

$$ \begin{array}{l} \forall \text{connection} : G(\text{chunksize}(\text{connection}) > 10,000) \\ \implies F(\text{chunksize}(\text{connection}) \leq 10,000). \end{array} $$

#### 4.1.3 Maximum bandwidth of Youtube connections

**Description of the monitored program** The program simulates Youtube connections. The program uses the dataset described in [85] to run the simulation.
**Description of the property** The property states that for all connections, it is always the case that the bandwidth is less than or equal to 100,000. The property is formalized using a fragment of first-order LTL [68] as follows:

$$ \forall connection : G(bandwidth(connection) \leq 100,000). $$

### 4.1.4 Changes in the bandwidth of Youtube connections

**Description of the monitored program** This benchmark uses the same program as the one in Sect. 4.1.3.

**Description of the property** The property states that, for all connections, it is always the case that when the *bandwidth* is strictly larger than 10,000, it *eventually* becomes less than or equal to 10,000. The bandwidth is a parameter of the execution trace. It is calculated by using *size_in_bytes* attribute which provides the number of bytes transferred, and *duration* which provides the time in seconds for the transfer. The property is formalized using a fragment of first-order LTL [68] as follows:

$$ \forall connection : G (bandwidth(connection) > 10,000 \Rightarrow F bandwidth(connection) \leq 10,000). $$

### 4.1.5 Allowed operations on files and sockets

**Description of the monitored program** The program simulates I/O operations by multiple processes on files and sockets. The output of this program is similar to that of running the *strace* utility in Linux to produce a system call trace for a set of processes.

**Description of the property** The property states that for all the processes and all the files, it is always the case that if a file (resp. a socket) is opened then it is eventually closed by the process. The property is formalized using a fragment of first-order LTL [68] as the conjunction of the two following formulae:

$$ \forall process, \forall file : $$

$$ G (open (process, file) \implies F close (process, file)) $$

$$ \forall process, \forall socket : $$

$$ G (accept (process, socket) \implies F close (process, socket)) $$

### 4.1.6 Binary search

This benchmark is provided by the E-ACSL team.

**Description of the monitored program** This benchmark consists in monitoring the standard binary search function defined below. It searches some key in a sorted array a of a given length.

```c
int binary_search
```

```c
(int* a, int length, int key)
{
    int low = 0, high = length - 1;
    while (low <= high) {
        int mid = low + (high - low) / 2;
        if (a[ mid ] == key) return mid;
        if (a[ mid ] < key) low = mid + 1;
        else high = mid - 1;
    }
    return -1;
}
```

The main function of the program calls this function 3 times on an array of 2,000,000 elements in order to:

- search an existing key and check that the return index is correct;

- search an unknown key and check that the function returns -1;

- search an existing well-chosen key in a wrongly sorted array (1 element is misplaced) and check that the function incorrectly returns -1.

**Description of the property** The monitored program must verify the following function contract of *binary_search*:

- it takes as input a positive *length* and a fully allocated sorted array of at least *length* elements;

- it returns either an index *idx* such that *a[*idx*] == key*; or -1 if there is no such index.

In the formal specification language E-ACSL [41] based on behavioral first-order logic, this specification may be described by the following function contract:

```c
/*@ requires \valid(a+(0..length-1));
   requires \forallall integer i;
   0<= i< length-1==>a[i]<= a[i+1];
   requires length >=0;
```

behavior exists:
assumes \exists exists integer i;
0 <= i < length && a[i] == key;
ensures 0 <= \result < length
ensures a[\result] == key;

behavior not_exists:
assumes \forallall integer i;
0 <= i < length ==> a[i] != key;
ensures \result == -1;
*/
int binary_search
(int* a, int length, int key);
**Description of the property** The property states that for all connections, it is always the case that the bandwidth is less than or equal to 100,000. The property is formalized using a fragment of first-order LTL [68] as follows:

$$ \forall connection : G(bandwidth(connection) \leq 100,000). $$

### 4.1.4 Changes in the bandwidth of Youtube connections

**Description of the monitored program** This benchmark uses the same program as the one in Sect. 4.1.3.

**Description of the property** The property states that, for all connections, it is always the case that when the *bandwidth* is strictly larger than 10,000, it *eventually* becomes less than or equal to 10,000. The bandwidth is a parameter of the execution trace. It is calculated by using *size_in_bytes* attribute which provides the number of bytes transferred, and *duration* which provides the time in seconds for the transfer. The property is formalized using a fragment of first-order LTL [68] as follows:

$$ \forall connection : G (bandwidth(connection) > 10,000 \Rightarrow F bandwidth(connection) \leq 10,000). $$

### 4.1.5 Allowed operations on files and sockets

**Description of the monitored program** The program simulates I/O operations by multiple processes on files and sockets. The output of this program is similar to that of running the *strace* utility in Linux to produce a system call trace for a set of processes.

**Description of the property** The property states that for all the processes and all the files, it is always the case that if a file (resp. a socket) is opened then it is eventually closed by the process. The property is formalized using a fragment of first-order LTL [68] as the conjunction of the two following formulae:

$$ \forall process, \forall file : $$

$$ G(\text{open}(\text{process}, \text{file}) \implies F \text{ close}(\text{process}, \text{file})) $$

$$ \forall process, \forall socket : $$

$$ G(\text{accept}(\text{process}, \text{socket}) \implies F \text{ close}(\text{process}, \text{socket})) $$

### 4.1.6 Binary search

This benchmark is provided by the E-ACSL team.

**Description of the monitored program** This benchmark consists in monitoring the standard binary search function defined below. It searches some key in a sorted array a of a given length.

$$ \text{int binary\_search} $$

(int* a, int length, int key)
{
    int low = 0, high = length - 1;
    while (low <= high) {
        int mid = low + (high - low) / 2;
        if (a[ mid ] == key) return mid;
        if (a[ mid ] < key) low = mid + 1;
        else high = mid - 1;
    }
    return -1;
}

The main function of the program calls this function 3 times on an array of 2,000,000 elements in order to:

- search an existing key and check that the return index is correct;

- search an unknown key and check that the function returns -1;

- search an existing well-chosen key in a wrongly sorted array (1 element is misplaced) and check that the function incorrectly returns -1.

**Description of the property** The monitored program must verify the following function contract of *binary_search*:

- it takes as input a positive *length* and a fully allocated sorted array of at least *length* elements;

- it returns either an index *idx* such that *a[*idx*] == key*; or -1 if there is no such index.

In the formal specification language E-ACSL [41] based on behavioral first-order logic, this specification may be described by the following function contract:

/*@ requires \valid(a+(0..length-1));
   requires \forallall integer i;
   0<= i< length-1==>a[i]<= a[i+1];
   requires length >=0;

behavior exists:

assumes \exists exists integer i;
0 <= i < length && a[i] == key;
ensures 0 <= \result < length
ensures a[\result] == key;

behavior not_exists:

assumes \forallforall integer i;
0 <= i < length ==> a[i] != key;
ensures \result == -1;

*/

int binary_search
(int* a, int length, int key);
The first *requires* clause states that each cell of the array must be correctly allocated, the second one states that the array must be sorted, and the third one indicates that the length must be positive. Then, the first behavior says that if the searched key exists in the array, the result of the function must be an array index corresponding to this key, while the second behavior says that the function returns -1 if there is no such index.

E- ACSL reports that the second requirement is violated when calling this function on the wrongly sorted array. Here is the result of the execution:

```
Precondition failed at line 18 in
function binary_search.
The failing predicate is:
\forall integer i;
0<=i< length-1==>*(a+i)<==*(a+(i+1)).
```

### 4.1.7 Merging arrays

This benchmark is provided by the E- ACSL team.

*Description of the monitored program* This benchmark provides two different implementations of a merging algorithm which merges two sorted arrays into a third one in a way that the resulting array is also sorted. The first implementation is assumed to be correct and is provided below, while the second one introduces an error by removing the marked instruction.

```c
void merge
(int *t1, int *t2, int *t3, int 11, int 12)
{
    int i = 0, j = 0, k = 0;
    while (i < 11 && j < 12) {
        if (t1[i] < t2[j]) {
            t3[k] = t1[i];
            i++;
        } else {
            t3[k] = t2[j];
            j++;
        }
        k++;
    }
    while (i < 11) {
        t3[k] = t1[i];
        i++;
        k++; // removed instruction
    }
    while (j < 12) {
        t3[k] = t2[j];
        j++;
        k++;
    }
}
```

The main function of the program calls both functions with one array of 6000 elements and another one of 4000 elements. *Description of the properties* The monitored program must check that each call to both functions:

- takes as input two positive lengths 11 and 12 and two sorted arrays t1 and t2 of length 11 and 12, respectively;

- modifies t3 such that it is a sorted array of length 11+12 where each element belongs to either t1 or t2. Reciprocally, each element of t1 and t2 must belong to t3.

In the formal specification language E- ACSL [41] based on behavioral first-order logic, this specification may be described by the following function contract:

```c
/*@ requires 11 >= 0;
requires 12 >= 0;
requires \forallall integer i; 0<=i<11-1
==> t1[i] <= t1[i+1];
requires \forallall integer i; 0<=i<12-1
==> t2[i] <= t2[i+1];
ensures\forallall integer i; 0<=i<11+12-1
==> t3[i] <= t3[i+1];
ensures \forallall integer i; 0<=i<11
==> \exists exists integer j; 0<=j<11+12
&& t1[i] == t3[j];
ensures \forallall integer i; 0<=i<12
==> \exists exists integer j; 0<=j<11+12
&& t2[i] == t3[j];
ensures\forallall integer i; 0<=i<11+12
==> ((\exists exists integer j; 0<=j<11
&& t3[i] == t1[j])
|| \exists exists integer j; 0<=j<12
&& t3[i] == t2[j]);
*/
void merge
(int *t1, int *t2, int *t3, int 11, int 12);
```

The two first requirements indicate that the lengths 11 and 12 of the input arrays t1 and t2 must be positive, while the two other requirements say that these arrays must be sorted. If the requirements of the function are satisfied, it must ensure 4 postcondition provided by the *ensures* clause. The first one indicates that the output array t3 must be sorted. The second (resp. third) postconditions indicates that each element of t1 (resp. t2) must also belong to t2, while the last postcondition states the reverse condition which is that each element of t3 belongs to either t1 or t2.

E- ACSL reports that the first postcondition is violated when calling the incorrect implementation. It states that the output array is sorted. Indeed, because of the missing instruction, the end of the output array contains (unsorted) garbage. Here is the result of the execution.
The first *requires* clause states that each cell of the array must be correctly allocated, the second one states that the array must be sorted, and the third one indicates that the length must be positive. Then, the first behavior says that if the searched key exists in the array, the result of the function must be an array index corresponding to this key, while the second behavior says that the function returns -1 if there is no such index.

E- ACSL reports that the second requirement is violated when calling this function on the wrongly sorted array. Here is the result of the execution:

```
Precondition failed at line 18 in
function binary_search.
The failing predicate is:
\forall integer i;
0<=i< length-1==>*(a+i <=* (a+(i+1)).
```

### 4.1.7 Merging arrays

This benchmark is provided by the E- ACSL team.

*Description of the monitored program* This benchmark provides two different implementations of a merging algorithm which merges two sorted arrays into a third one in a way that the resulting array is also sorted. The first implementation is assumed to be correct and is provided below, while the second one introduces an error by removing the marked instruction.

```c
void merge
(int *t1, int *t2, int *t3, int 11, int 12)
{
    int i = 0, j = 0, k = 0;
    while (i < 11 && j < 12) {
        if (t1[i] < t2[j]) {
            t3[k] = t1[i];
            i++;
        } else {
            t3[k] = t2[j];
            j++;
        }
        k++;
    }
    while (i < 11) {
        t3[k] = t1[i];
        i++;
        k++; // removed instruction
    }
    while (j < 12) {
        t3[k] = t2[j];
        j++;
        k++;
    }
}
```

The main function of the program calls both functions with one array of 6000 elements and another one of 4000 elements. *Description of the properties* The monitored program must check that each call to both functions:

- takes as input two positive lengths 11 and 12 and two sorted arrays t1 and t2 of length 11 and 12, respectively;

- modifies t3 such that it is a sorted array of length 11+12 where each element belongs to either t1 or t2. Reciprocally, each element of t1 and t2 must belong to t3.

In the formal specification language E- ACSL [41] based on behavioral first-order logic, this specification may be described by the following function contract:

```c
/*@ requires 11 >= 0;
requires 12 >= 0;
requires \forallall integer i; 0<=i<11-1
==> t1[i] <= t1[i+1];
requires \forallall integer i; 0<=i<12-1
==> t2[i] <= t2[i+1];
ensures\forallall integer i; 0<=i<11+12-1
==> t3[i] <= t3[i+1];
ensures \forallall integer i; 0<=i<11
==> \exists exists integer j; 0<=j<11+12
&& t1[i] == t3[j];
ensures \forallall integer i; 0<=i<12
==> \exists exists integer j; 0<=j<11+12
&& t2[i] == t3[j];
ensures\forallall integer i; 0<=i<11+12
==> ((\exists exists integer j; 0<=j<11
&& t3[i] == t1[j])
|| \exists exists integer j; 0<=j<12
&& t3[i] == t2[j]);
*/
void merge
(int *t1, int *t2, int *t3, int 11, int 12);
```

The two first requirements indicate that the lengths 11 and 12 of the input arrays t1 and t2 must be positive, while the two other requirements say that these arrays must be sorted. If the requirements of the function are satisfied, it must ensure 4 postcondition provided by the *ensures* clause. The first one indicates that the output array t3 must be sorted. The second (resp. third) postconditions indicates that each element of t1 (resp. t2) must also belong to t2, while the last postcondition states the reverse condition which is that each element of t3 belongs to either t1 or t2.

E- ACSL reports that the first postcondition is violated when calling the incorrect implementation. It states that the output array is sorted. Indeed, because of the missing instruction, the end of the output array contains (unsorted) garbage. Here is the result of the execution.

<figure><img src="image_7.png" /></figure>
Postcondition failed at line 59 in
function wrong_merge.
The failing predicate is:
\forall integer i;
0 <= i < (\old(11)+\old(12))-1
==>* (\old(t3)+i) <=* (\old(t3)+(i+1)).

### 4.1.8 Quicksort

This benchmark is provided by the E-ACSL team.
*Description of the monitored program* This benchmark provides an implementation of the standard quicksort algorithm, which sorts a given array between two indexes left and right:

void quicksort
(int *array, int left, int right)
{
  if(left < right) {
    int idx = (left+right)/2;
    int new_idx =
        partition(array, left, right, idx);
    quicksort(array, left, new_idx-1);
    quicksort(array, new_idx+1, right);
  }
}

This implementation uses two helper functions *partition* and *swap*. Only the first one is given below. The second one which swaps the contents of two array cells is straightforward.

int partition
(int *array, int left, int right, int idx)
{
  int valarray[idx], store=left, i;
  swap(array, idx, right);
  for(i = left; i < right; i++) {
    if(array[i] <= val) {
      swap(array, i, store);
      store++;
    }
  }
  swap(array, store, right);
  return store;
}

The main function of the program contains 2 calls to the quicksort function on an unsorted array of 10,000 elements. The first call is a correct one, but the second call gives 10,001 as the right bound instead of 10,000 (at most).

*Description of the properties* The only property that must be checked by this benchmark is that quicksort is called on a fully allocated array up to the given length.

In the formal specification language E-ACSL [41] based on behavioral first-order logic, this specification may be described by the following function contract which formally expresses that each cell of the array between left and right must be valid (non-null and points to a memory location that the program is allowed to write).

/*@ requires \forallall integer j;
         left <= j <= right
         ===> \valid(array+j); */
void quicksort
(int* array, int left, int right);

E-ACSL reports that this property is violated on the second function call since the function tries to access to the invalid index 10,001 of the array. Here is the result of the execution.

Precondition failed at line 35 in
function quicksort.
The failing predicate is:
\forall integer j;
left <= j <= right==>\valid(array+j).

### 4.1.9 Accesses to arrays without off-by-one nor out-of-bounds

This benchmark is provided by the RTC team.
*Description of the monitored program* The program is a test case from the Juliet test suite [23], a collection of test cases in the C/C++ language produced by the NIST. This program is a minimal example of a violation of the property described below. It does an array access from a statically allocated array of size 1024 at index 1024.

*Description of the property* The property states that there should not be off-by-one errors (see item 193 in the Common Weakness Enumeration<fnref n="6" /> list) nor out-of-bounds read (see item 125 in the Common Weakness Enumeration<fnref n="7" /> list) on a global array.

### 4.1.10 Absence of buffer overflow in a palindrome generator

This benchmark is provided by the RTC team.
*Description of the monitored program* The program finds the next highest number that is a palindrome after a number provided as input. The program has been modified by adding a heap-based buffer overflow when reading the input number. The number is written with an unbounded string copy to the heap allocated buffer 'k' of size MAX_LEN (300). The program contains a call to strcpy() that copies a single character

<footnote n="6">⁶ https://cwe.mitre.org/data/definitions/193.html.</footnote>

<footnote n="7">⁷ https://cwe.mitre.org/data/definitions/125.html.</footnote>
Postcondition failed at line 59 in
function wrong_merge.
The failing predicate is:
\forall integer i;
0 <= i < (\old(11)+\old(12))-1
==>* (\old(t3)+i) <=* (\old(t3)+(i+1)).

### 4.1.8 Quicksort

This benchmark is provided by the E- ACSL team.
*Description of the monitored program* This benchmark provides an implementation of the standard quicksort algorithm, which sorts a given array between two indexes left and right:

void quicksort
(int *array, int left, int right)
{
  if(left < right) {
    int idx = (left+right)/2;
    int new_idx =
        partition(array, left, right, idx);
    quicksort(array, left, new_idx-1);
    quicksort(array, new_idx+1, right);
  }
}

This implementation uses two helper functions *partition* and *swap*. Only the first one is given below. The second one which swaps the contents of two array cells is straightforward.

int partition
(int *array, int left, int right, int idx)
{
  int val[idx], store=left, i;
  swap(array, idx, right);
  for(i = left; i < right; i++) {
    if(array[i] <= val) {
      swap(array, i, store);
      store++;
    }
  }
  swap(array, store, right);
  return store;
}

The main function of the program contains 2 calls to the quicksort function on an unsorted array of 10,000 elements. The first call is a correct one, but the second call gives 10,001 as the right bound instead of 10,000 (at most).

*Description of the properties* The only property that must be checked by this benchmark is that quicksort is called on a fully allocated array up to the given length.

In the formal specification language E- ACSL [41] based on behavioral first-order logic, this specification may be described by the following function contract which formally expresses that each cell of the array between left and right must be valid (non-null and points to a memory location that the program is allowed to write).

/*@ requires \forallall integer j;
         left <= j <= right
         ===> \valid(array+j); */
void quicksort
(int* array, int left, int right);

E- ACSL reports that this property is violated on the second function call since the function tries to access to the invalid index 10,001 of the array. Here is the result of the execution.

Precondition failed at line 35 in
function quicksort.
The failing predicate is:
\forall integer j;
left <= j <= right==>\valid(array+j).

### 4.1.9 Accesses to arrays without off-by-one nor out-of-bounds

This benchmark is provided by the RTC team.
*Description of the monitored program* The program is a test case from the Juliet test suite [23], a collection of test cases in the C/C++ language produced by the NIST. This program is a minimal example of a violation of the property described below. It does an array access from a statically allocated array of size 1024 at index 1024.

*Description of the property* The property states that there should not be off-by-one errors (see item 193 in the Common Weakness Enumeration<fnref n="6" /> list) nor out-of-bounds read (see item 125 in the Common Weakness Enumeration<fnref n="7" /> list) on a global array.

### 4.1.10 Absence of buffer overflow in a palindrome generator

This benchmark is provided by the RTC team.
*Description of the monitored program* The program finds the next highest number that is a palindrome after a number provided as input. The program has been modified by adding a heap-based buffer overflow when reading the input number. The number is written with an unbounded string copy to the heap allocated buffer 'k' of size MAX_LEN (300). The program contains a call to strcpy() that copies a single character

<footnote n="6">⁶ https://cwe.mitre.org/data/definitions/193.html.</footnote>

<footnote n="7">⁷ https://cwe.mitre.org/data/definitions/125.html.</footnote>
from the input string to the buffer, and this line is reached multiple times as the program scans over the input string. The program is a test case of the STONESOUP test suite [17], a collection of test cases in the C and Java languages produced by the NIST.

*Description of the property* The property states the absence of buffer overflow. The vulnerability could allow an attacker to execute code by writing past the buffer and overwriting function pointers that exist in memory (see item 122 in the Common Weakness Enumeration<fnref n="8" /> list).

### 4.1.11 Absence of negative pointers in function calls

This benchmark is provided by the RTC team.

*Description of the monitored program* The program attempts to call a standard library function, `strcat()`, with a negative pointer index. The program is a test case from the Juliet test suite [23], a collection of test cases in the C/C++ language produced by the NIST. The program contains an array access with a negative pointer index in the arguments to `strcat()`.

*Description of the property* The property states that there should not be pointers referring to negative values passed as arguments to function.

## 4.2 Java track

### 4.2.1 Gold users of the financial transaction system

The benchmark is provided by the LARVA team. The LARVA team provided five benchmarks (described also in Sects. 4.2.2, 4.2.3, 4.2.4, and 4.2.5). Common to all the benchmarks is that the considered properties concern a financial transaction system described in the following.

*Description of the monitored program* FiTS (Financial Transaction System) is a cut-down version of a financial transaction system aimed at providing basic functionality to ensure that the focus is on the verification techniques and not on understanding the underlying system. Based on FiTS, a number of properties inspired from real-life case studies are specified. FiTS is a barebone system mocking the behavior of a financial transaction system. It emulates a virtual banking system in which users may open accounts from which they may perform money transfers. The system has two types of users: administrators and clients. The former have more rights than normal clients enabling them to perform certain actions such as approving the opening of an account, enabling a new user and registering new users. A client can invoke a number of actions to access their (money) accounts which they have registered on FiTS—actions which they may invoke through an online interface. Information about each registered client is stored in a database, including information such as the

client's name and country of origin, and client classification information.

Under FiTS, each client may be associated with a number of money accounts belonging to him. Clients may request the creation of a new account or close down one of their accounts at any point in time. To access accounts, an existing client may open a login session on FiTS to make transfers or manage their money accounts. A user may have multiple sessions open at the same time.

The following properties are specified in a guarded-command language (GCL) as a series of Java-based rules of the form `event | condition → action`.

*Description of the property* The property states that only users based in Argentina can be Gold users. The property can be expressed as follows:

$$ 
\begin{array}{l}
*.makeGoldUser(..) target (UserInfo u) \\
| ! (u.getCountry().equals("Argentina")) \\
\rightarrow Verification人大. fail("P1 violated");
\end{array}
$$

Informally, upon giving the status of Gold user to a client, it must be ensured that he or she is from Argentina. Thus, any trace containing a call to `makeGoldUser` on a user whose country is not Argentina violates the property and vice-versa.

### 4.2.2 Initialization in the financial transaction system

The benchmark is provided by the LARVA team. *Description of the monitored program* The program of this benchmark is described in Sect. 4.2.1.

*Description of the property* The property states that the transaction system must be initialized before any user logs in. The property can be expressed as follows:

$$ 
\begin{array}{l}
*.initialize(..) | \rightarrow Verification. initialized=true; \\
UserInfo. openSession(..) | !Verification. initialized \\
\rightarrow Verification. 大人. fail("P2 violated");
\end{array}
$$

Informally, set a *initialized* flag to true when the system is initialized and check this flag upon the start of any user session. Hence, a trace containing a call to *openSession* before *initialize* violates the property while any other trace satisfies it.

### 4.2.3 Negative balance in the financial transaction system

The benchmark is provided by the LARVA team.

*Description of the monitored program* The program of this benchmark is described in Sect. 4.2.1.

*Description of the property* The property states that no account may end up with a negative balance after being accessed. The property can be expressed as follows:

$$ 
\begin{array}{l}
*.withdraw(..) target (UserAccount a) | a.getBalance() < 0 \\
\rightarrow Verification. 大人. fail("P3 violated");
\end{array}
$$

<figure><img src="image_8.png" /></figure>

<footnote n="8">⁸ https://cwe.mitre.org/data/definitions/122.html.</footnote>
from the input string to the buffer, and this line is reached multiple times as the program scans over the input string. The program is a test case of the STONESOUP test suite [17], a collection of test cases in the C and Java languages produced by the NIST.

*Description of the property* The property states the absence of buffer overflow. The vulnerability could allow an attacker to execute code by writing past the buffer and overwriting function pointers that exist in memory (see item 122 in the Common Weakness Enumeration<fnref n="8" /> list).

### 4.1.11 Absence of negative pointers in function calls

This benchmark is provided by the RTC team.

*Description of the monitored program* The program attempts to call a standard library function, `strcat()`, with a negative pointer index. The program is a test case from the Juliet test suite [23], a collection of test cases in the C/C++ language produced by the NIST. The program contains an array access with a negative pointer index in the arguments to `strcat()`.

*Description of the property* The property states that there should not be pointers referring to negative values passed as arguments to function.

## 4.2 Java track

### 4.2.1 Gold users of the financial transaction system

The benchmark is provided by the LARVA team. The LARVA team provided five benchmarks (described also in Sects. 4.2.2, 4.2.3, 4.2.4, and 4.2.5). Common to all the benchmarks is that the considered properties concern a financial transaction system described in the following.

*Description of the monitored program* FiTS (Financial Transaction System) is a cut-down version of a financial transaction system aimed at providing basic functionality to ensure that the focus is on the verification techniques and not on understanding the underlying system. Based on FiTS, a number of properties inspired from real-life case studies are specified. FiTS is a barebone system mocking the behavior of a financial transaction system. It emulates a virtual banking system in which users may open accounts from which they may perform money transfers. The system has two types of users: administrators and clients. The former have more rights than normal clients enabling them to perform certain actions such as approving the opening of an account, enabling a new user and registering new users. A client can invoke a number of actions to access their (money) accounts which they have registered on FiTS—actions which they may invoke through an online interface. Information about each registered client is stored in a database, including information such as the

client's name and country of origin, and client classification information.

Under FiTS, each client may be associated with a number of money accounts belonging to him. Clients may request the creation of a new account or close down one of their accounts at any point in time. To access accounts, an existing client may open a login session on FiTS to make transfers or manage their money accounts. A user may have multiple sessions open at the same time.

The following properties are specified in a guarded-command language (GCL) as a series of Java-based rules of the form `event | condition → action`.

*Description of the property* The property states that only users based in Argentina can be Gold users. The property can be expressed as follows:

$$ 
\begin{array}{l}
*.makeGoldUser(..) target (UserInfo u) \\
| ! (u.getCountry().equals("Argentina")) \\
\rightarrow Verification.fail("P1 violated");
\end{array}
$$

Informally, upon giving the status of Gold user to a client, it must be ensured that he or she is from Argentina. Thus, any trace containing a call to `makeGoldUser` on a user whose country is not Argentina violates the property and vice-versa.

### 4.2.2 Initialization in the financial transaction system

The benchmark is provided by the LARVA team. *Description of the monitored program* The program of this benchmark is described in Sect. 4.2.1.

*Description of the property* The property states that the transaction system must be initialized before any user logs in. The property can be expressed as follows:

$$ 
\begin{array}{l}
*.initialize(..) | \rightarrow Verification-o initialized=true; \\
UserInfo.openSession(..) | !Verification-o initialized \\
\rightarrow Verification.fail("P2 violated");
\end{array}
$$

Informally, set a *initialized* flag to true when the system is initialized and check this flag upon the start of any user session. Hence, a trace containing a call to *openSession* before *initialize* violates the property while any other trace satisfies it.

### 4.2.3 Negative balance in the financial transaction system

The benchmark is provided by the LARVA team.

*Description of the monitored program* The program of this benchmark is described in Sect. 4.2.1.

*Description of the property* The property states that no account may end up with a negative balance after being accessed. The property can be expressed as follows:

$$ 
\begin{array}{l}
*.withdraw(..) target (UserAccount a) | a.getBalance() < 0 \\
\rightarrow Verification.fail("P3 violated");
\end{array}
$$

<footnote n="8">⁸ https://cwe.mitre.org/data/definitions/122.html.</footnote>
\*.deposit(..) target (UserAccount a) | a.getBalance() < 0 → Verification fail("P3 violated");

Informally, the rules check the balance of the account after a withdraw or deposit actions to ensure that it is always positive. A trace containing a withdraw or deposit on an account with subsequent negative balance violates the property. Otherwise, the trace satisfies the property.

### 4.2.4 Unique account in the financial transaction system

The benchmark is provided by the LARVA team.

**Description of the monitored program** The program of this benchmark is described in Sect. 4.2.1.

**Description of the property** The property states that an account approved by the administrator may not have the same account number as any other already existing account in the system. The property can be expressed as follows:

\*.approveOpenAccount Integer uid, String acc_number) | → Verification approvedAccounts add acc_number;

\*.approveOpenAccount Integer uid, String acc_number) | Verification approvedAccounts contains acc_number) → Verification fail("P4 violated");

Informally, a `hashmap` is kept for all account numbers and each number assigned to a new account is checked for membership in this `hashmap`. A trace containing two calls to `approveOpenAccount` with the same account number violates the property.

### 4.2.5 Reactivation in the financial transaction system

The benchmark is provided by the LARVA team.

**Description of the monitored program** The program of this benchmark is described in Sect. 4.2.1.

**Description of the property** The property states that once a user is disabled, he or she may not withdraw from an account until activated again. The property can be specified as follows:

UserInfo.makeDisabled(..) target (UserInfo u) | → Verification disabledUsers add(u);
UserInfo.makeActive(..) target (UserInfo u) | → Verification disabledUsers remove(u);
UserInfo.withdrawFrom(..) target (UserInfo u) | (Verification disabledUsers contains(u)) → Verification fail("P5 violated");

Informally, the rules keep track of disabled users by adding the user to a list upon being disabled and removing the user upon activating. Subsequently, upon a withdraw the third rule ensures that the user is not in the list. Thus, a trace containing a call to `makeDisabled` followed by a withdraw on the same

user, violates the property. On the contrary, a user performing a withdraw after being disabled but later activated satisfies the property.

### 4.2.6 Incrementing a counter

This benchmark is provided by the JUNITRV team.

The JUNITRV team provided five benchmarks (described also in Sects. 4.2.7, 4.2.8, 4.2.9, and 4.2.10). Common to all the benchmarks is that the considered programs are simple Java programs that generate random method calls that in turn generate events for the property of the benchmark. Moreover, the properties are given in linear temporal logic over first-order formulae as defined in [40]. Free variables are assumed to be universally quantified at the outermost position. First-order symbols either refer to some fixed theory or to the current system observation (called observation symbols). The benchmark properties only use the theories of IDs, linear equations over integers and linear equations over reals.

In this benchmark, the property holds on the program.
**Description of the monitored program** The aim of this benchmark is to test the ability to monitor properties involving counting. The program simply calls a method `step(int counter)` repeatedly. With each call, the value for counter increases by one.

**Description of the property** The required property is that the parameter counter of method `step` has to increase by one with each call. Formally:

$$ \forall x G(\mathit{counter} = x \implies \bar{\mathit{x}}(\mathit{counter} = x + 1)) $$

Here, $x$ is a globally quantified variable and `counter` is an integer-valued observation symbol. The observed event is the call to method `step`, and the observation symbol `counter` is a constant referring to the current value of the corresponding parameter of `step`.

**Example traces** A positive example would be the sequence `{counter $\mapsto$ 1}`, `{counter $\mapsto$ 2}`, `{counter $\mapsto$ 3}`, a negative example the sequence `{counter $\mapsto$ 1}`, `{counter $\mapsto$ 2}`, `{counter $\mapsto$ 1}`.

### 4.2.7 Request and response

This benchmark is provided by the JUNITRV team. This benchmark uses the common setting where certain service are requested and providers have to respond to such requests. In this benchmark, the property holds on the program.

**Description of the monitored program** The program calls a method `request` (int service) indicating a service with the given id was requested and `respond(int service, int provider)` to indicate that a provider responded to a request for the given service.
\*.deposit(..) target (UserAccount a) | a.getBalance() < 0 → Verification fail("P3 violated");

Informally, the rules check the balance of the account after a withdraw or deposit actions to ensure that it is always positive. A trace containing a withdraw or deposit on an account with subsequent negative balance violates the property. Otherwise, the trace satisfies the property.

### 4.2.4 Unique account in the financial transaction system

The benchmark is provided by the LARVA team.

**Description of the monitored program** The program of this benchmark is described in Sect. 4.2.1.

**Description of the property** The property states that an account approved by the administrator may not have the same account number as any other already existing account in the system. The property can be expressed as follows:

\*.approveOpenAccount Integer uid, String acc_number) | → Verification approvedAccounts add acc_number;

\*.approveOpenAccount Integer uid, String acc_number) | Verification approvedAccounts contains acc_number) → Verification fail("P4 violated");

Informally, a `hashmap` is kept for all account numbers and each number assigned to a new account is checked for membership in this `hashmap`. A trace containing two calls to `approveOpenAccount` with the same account number violates the property.

### 4.2.5 Reactivation in the financial transaction system

The benchmark is provided by the LARVA team.

**Description of the monitored program** The program of this benchmark is described in Sect. 4.2.1.

**Description of the property** The property states that once a user is disabled, he or she may not withdraw from an account until activated again. The property can be specified as follows:

UserInfo.makeDisabled(..) target (UserInfo u) | → Verification disabledUsers add(u);
UserInfo.makeActive(..) target (UserInfo u) | → Verification disabledUsers remove(u);
UserInfo.withdrawFrom(..) target (UserInfo u) | (Verification disabledUsers contains(u)) → Verification fail("P5 violated");

Informally, the rules keep track of disabled users by adding the user to a list upon being disabled and removing the user upon activating. Subsequently, upon a withdraw the third rule ensures that the user is not in the list. Thus, a trace containing a call to `makeDisabled` followed by a withdraw on the same

user, violates the property. On the contrary, a user performing a withdraw after being disabled but later activated satisfies the property.

### 4.2.6 Incrementing a counter

This benchmark is provided by the JUNITRV team.

The JUNITRV team provided five benchmarks (described also in Sects. 4.2.7, 4.2.8, 4.2.9, and 4.2.10). Common to all the benchmarks is that the considered programs are simple Java programs that generate random method calls that in turn generate events for the property of the benchmark. Moreover, the properties are given in linear temporal logic over first-order formulae as defined in [40]. Free variables are assumed to be universally quantified at the outermost position. First-order symbols either refer to some fixed theory or to the current system observation (called observation symbols). The benchmark properties only use the theories of IDs, linear equations over integers and linear equations over reals.

In this benchmark, the property holds on the program.
**Description of the monitored program** The aim of this benchmark is to test the ability to monitor properties involving counting. The program simply calls a method `step(int counter)` repeatedly. With each call, the value for counter increases by one.

**Description of the property** The required property is that the parameter counter of method `step` has to increase by one with each call. Formally:

$$ \forall x G(\mathit{counter} = x \implies \bar{\mathit{x}}(\mathit{counter} = x + 1)) $$

Here, $x$ is a globally quantified variable and `counter` is an integer-valued observation symbol. The observed event is the call to method `step`, and the observation symbol `counter` is a constant referring to the current value of the corresponding parameter of `step`.

**Example traces** A positive example would be the sequence `{counter $\mapsto$ 1}`, `{counter $\mapsto$ 2}`, `{counter $\mapsto$ 3}`, a negative example the sequence `{counter $\mapsto$ 1}`, `{counter $\mapsto$ 2}`, `{counter $\mapsto$ 1}`.

### 4.2.7 Request and response

This benchmark is provided by the JUNITRV team. This benchmark uses the common setting where certain service are requested and providers have to respond to such requests. In this benchmark, the property holds on the program.

**Description of the monitored program** The program calls a method `request` (int service) indicating a service with the given id was requested and `respond(int service, int provider)` to indicate that a provider responded to a request for the given service.
**Description of the property** The required property is that whenever a service is requested, eventually there is a response for that request from some provider.

Formally:

$$ \forall s \forall p \begin{array}{l} G((\text{request} \land \text{service} = s) \\ \Rightarrow \ X \exists p (\text{respond} \land \text{service} = s \land \text{provider} = p)) \end{array} $$

The observed events are the calls to methods request and respond. The observation symbol **service** refers to the service id of the current event. The observation symbol **provider** refers to the provider id of the current event.

**Example traces** A positive example would be the sequence

```
{request, service $\mapsto$ 1, provider $\mapsto$ 2},
{request, service $\mapsto$ 3, provider $\mapsto$ 4},
{respond, service $\mapsto$ 1, provider $\mapsto$ 2},
{respond, service $\mapsto$ 3, provider $\mapsto$ 4},
```

a negative example the sequence

```
{request, service $\mapsto$ 1, provider $\mapsto$ 2},
{request, service $\mapsto$ 3, provider $\mapsto$ 4},
{respond, service $\mapsto$ 3, provider $\mapsto$ 4}.
```

### 4.2.8 Locking critical resources

This benchmark is provided by the JUNITRV team. For this benchmark, the setting of a critical action requiring locking is considered. In this benchmark, the property holds on the program.

**Description of the monitored program** The program runs multiple threads in parallel performing some critical action. The critical action must only be performed by one thread at a time. Thus, the threads have to call the method boolean lock() and obtain the return value true before calling action(). The lock is released by calling unlock().

**Description of the property** The property consists of two parts: A thread has to call lock (returning true) to acquire the lock before it may call action and a call to lock only returns true, if no thread is currently holding the lock. Formally:

$$ \forall i \begin{array}{l} G((\text{run} \lor \text{unlock}) \land \text{id} = i) \\ \Rightarrow \neg(\text{action} \land \text{id} = i) \bar{U}(\text{lockTrue} \land \text{id} = i)) \\ \land G((\text{lock} \land \text{id} = i) \Rightarrow X(\neg\text{lockTrue} \lor \text{ unlock} \land \text{id} = i))) \end{array} $$

The observed events are the calls to method run() (the main method of a thread), unlock and action and the return of unlock. The symbol lockTrue not only indicates that lock returned, but also that the return value was true. The observation sym-

bol id refers to the id of the thread performing the current event.

**Example traces** A positive example would be the sequence `{lock, id $\mapsto$ 1}, {action, id $\mapsto$ 1}, {unlock, id $\mapsto$ 1},` a negative example the sequence `{lock, id $\mapsto$ 1}, {action, id $\mapsto$ 2}, { unlock, id $\mapsto$ 1}`.

### 4.2.9 Velocity of an object

This benchmark is provided by the JUNITRV team. This benchmark pertains the ability to express constraints over real numbers. In this benchmark, the property holds on the program.

**Description of the monitored program** The program simulates an object moving with changing velocity. The object's position is observed in discrete steps. A call to the method step(double pos, double time) indicates such an observation.

**Description of the property** The required property is that the average speed between two observations (i.e., calls to step) must never exceed the maximal velocity 10:

$$ \forall s \forall t \begin{array}{l} G((\text{time} = t \land \text{pos} = s) \\ \Rightarrow \bar{X}(\text{pos} - s < 10 \cdot \text{time} - t))) \end{array} $$

The observed event is the call to method step. The observation symbol time refers to the time parameter of method step. The observation symbol pos refers to the time parameter of method step.

**Example traces** A positive example would be the sequence

```
{time $\mapsto$ 0.0, pos $\mapsto$ 0.0},
{time $\mapsto$ 1.0, pos $\mapsto$ 5.0},
{time $\mapsto$ 2.0, pos $\mapsto$ 10.0},
```

a negative example the sequence

```
{time $\mapsto$ 0.0, pos $\mapsto$ 0.0},
{time $\mapsto$ 1.0, pos $\mapsto$ 50.0},
{time $\mapsto$ 2.0, pos $\mapsto$ 100.0}.
```

### 4.2.10 Non-crossing routes

This benchmark is provided by the JUNITRV team. The aim of this benchmark is to demonstrate the expressiveness of linear temporal logic combined with first-order constraints. It therefore requires a property for which it would be rather difficult to implement a monitor manually. The setting is inspired by the idea of agents in a multi agent system. The agents request a route from one point to another. Blocked routes must not cross.

**Description of the monitored program** The program simulates such a scenario by repeatedly blocking and freeing
**Description of the property** The required property is that whenever a service is requested, eventually there is a response for that request from some provider.

Formally:

$$ \forall s \forall p \begin{array}{l} G((\text{request} \land \text{service} = s) \\ \qquad \Rightarrow \text{XF} \exists p (\text{respond} \land \text{service} = s \land \text{provider} = p)) \end{array} $$

The observed events are the calls to methods request and respond. The observation symbol service refers to the service id of the current event. The observation symbol provider refers to the provider id of the current event.

**Example traces** A positive example would be the sequence

$$ \begin{array}{l} \{\text{request, service} \mapsto 1, \text{provider} \mapsto 2\}, \\ \{\text{request, service} \mapsto 3, \text{provider} \mapsto 4\}, \\ \{\text{respond, service} \mapsto 1, \text{provider} \mapsto 2\}, \\ \{\text{respond, service} \mapsto 3, \text{provider} \mapsto 4\}, \end{array} $$

a negative example the sequence

$$ \begin{array}{l} \{\text{request, service} \mapsto 1, \text{provider} \mapsto 2\}, \\ \{\text{request, service} \mapsto 3, \text{provider} \mapsto 4\}, \\ \{\text{respond, service} \mapsto 3, \text{provider} \mapsto 4\}. \end{array} $$

### 4.2.8 Locking critical resources

This benchmark is provided by the JUNITRV team. For this benchmark, the setting of a critical action requiring locking is considered. In this benchmark, the property holds on the program.

**Description of the monitored program** The program runs multiple threads in parallel performing some critical action. The critical action must only be performed by one thread at a time. Thus, the threads have to call the method boolean lock() and obtain the return value true before calling action(). The lock is released by calling unlock().

**Description of the property** The property consists of two parts: A thread has to call lock (returning true) to acquire the lock before it may call action and a call to lock only returns true, if no thread is currently holding the lock. Formally:

$$ \forall i \begin{array}{l} G((\text{run} \lor \text{unlock}) \land \text{id} = i) \\ \qquad \Rightarrow \neg(\text{action} \land \text{id} = i) \bar{U}(\text{lockTrue} \land \text{id} = i)) \\ \land G((\text{lock} \land \text{id} = i) \Rightarrow X(\neg\text{lockTrue} \lor \text{ unlock} \land \text{id} = i))) \end{array} $$

The observed events are the calls to method run() (the main method of a thread), unlock and action and the return of unlock. The symbol lockTrue not only indicates that lock returned, but also that the return value was true. The observation sym-

bol id refers to the id of the thread performing the current event.

**Example traces** A positive example would be the sequence $\{\text{lock, id} \mapsto 1\}$, $\{\text{action, id} \mapsto 1\}$, $\{\text{unlock, id} \mapsto 1\}$, a negative example the sequence $\{\text{lock, id} \mapsto 1\}$, $\{\text{action, id} \mapsto 2\}$, $\{\text{ unlock, id} \mapsto 1\}$.

### 4.2.9 Velocity of an object

This benchmark is provided by the JUNITRV team. This benchmark pertains the ability to express constraints over real numbers. In this benchmark, the property holds on the program.

**Description of the monitored program** The program simulates an object moving with changing velocity. The object's position is observed in discrete steps. A call to the method step(double pos, double time) indicates such an observation.

**Description of the property** The required property is that the average speed between two observations (i.e., calls to step) must never exceed the maximal velocity 10:

$$ \forall s \forall t \begin{array}{l} G((\text{time} = t \land \text{pos} = s) \\ \qquad \Rightarrow \bar{X}(\text{pos} - s < 10 \cdot \text{time} - t))) \end{array} $$

The observed event is the call to method step. The observation symbol time refers to the time parameter of method step. The observation symbol pos refers to the time parameter of method step.

**Example traces** A positive example would be the sequence

$$ \begin{array}{l} \{\text{time} \mapsto 0.0, \text{pos} \mapsto 0.0\}, \\ \{\text{time} \mapsto 1.0, \text{pos} \mapsto 5.0\}, \\ \{\text{time} \mapsto 2.0, \text{pos} \mapsto 10.0\}, \end{array} $$

a negative example the sequence

$$ \begin{array}{l} \{\text{time} \mapsto 0.0, \text{pos} \mapsto 0.0\}, \\ \{\text{time} \mapsto 1.0, \text{pos} \mapsto 50.0\}, \\ \{\text{time} \mapsto 2.0, \text{pos} \mapsto 100.0\}. \end{array} $$

### 4.2.10 Non-crossing routes

This benchmark is provided by the JUNITRV team. The aim of this benchmark is to demonstrate the expressiveness of linear temporal logic combined with first-order constraints. It therefore requires a property for which it would be rather difficult to implement a monitor manually. The setting is inspired by the idea of agents in a multi agent system. The agents request a route from one point to another. Blocked routes must not cross.

**Description of the monitored program** The program simulates such a scenario by repeatedly blocking and freeing
routes. Blocking a route is indicated by a call to `block(Route route)`. Freeing a route is indicated by a call to `free(Route route)`. A route is a simple line segment described by a starting and end point. The mentioned property can be formulated as: If a point $p$ belongs to a route that is being blocked, no other route that contains $p$ can be blocked as long as $p$ has not been freed again. (The point $p$ is freed by freeing a route that contains $p$.) Formally:

$$ 
\begin{aligned}
\forall p & G(\mathit{block} \land \mathit{onRoute}(p)) \\
& \Rightarrow \bar{X}(\neg(\mathit{block} \land \mathit{onRoute}(p))) \\
& \qquad \bar{U}(\mathit{free} \land \mathit{onRoute}(p)))
\end{aligned}
$$

The observed events are the calls to methods `block` and `free`. Let $q$ and $r$ be the start and end points, respectively, given as arguments to the called method. The only observation symbol is `onRoute($p$)` which indicates whether a point $p$ is on the route between $q$ and $r$. This predicate can be expressed as an equation `onRoute($p$) := $\exists c (p = q + c \cdot (r-q) \land 0 \le c \le 1)$`. Example traces A positive example would be the sequence

$$ 
\begin{aligned}
\{\mathit{block}, \mathit{onRoute} \mapsto & \{p \mid \exists c \mid 0 \le c \le 1 (p = (1, 2) + c \cdot (2, 2))\}, \\
& \{\mathit{free}, \mathit{onRoute} \mapsto \{p \mid \exists c \mid 0 \le c \le 1 (p = (1, 2) + c \cdot (1, 1))\}\},
\end{aligned}
$$

a negative example the sequence

$$ 
\begin{aligned}
\{\mathit{block}, \mathit{onRoute} \mapsto & \{p \mid \exists c \mid 0 \le c \le 1 (p = (1, 2) + c \cdot (2, 2))\}, \\
& \{\mathit{block}, \mathit{onRoute} \mapsto \{p \mid \exists c \mid 0 \le c \le 1 (p = (2, 2) + c \cdot (-1, 1))\}\}.
\end{aligned}
$$

### 4.2.11 HasNext on DaCapo Avrora

This benchmark is provided by the `JAVA-` MOP team. The benchmark considers the (classical) **HasNext** property on one of the so-called DaCapo [22] benchmark. In this benchmark, the property does not hold on the program.

**Description of the monitored program** The considered program is the DaCapo Avrora benchmark, which simulates a number of programs running on a grid of AVR microcontrollers. The program is slightly modified to violate the **HasNext** property intentionally.

**Description of the property** This property requires that the `hasNext()` method is called and returns true before calling `next()` method for each `Iterator` object $i$. It may raise a false positive because one may safely call method `next()` multiple times after retrieving the actual number of elements. The following LTL describes the **HasNext** property.

$$ \forall i G(next(i) \implies Yhasnext_true(i)) $$

In the formula, $X^{-1}$ means previous. Event `next(i)` corresponds to a call to the method `next()` on iterator $i$ and event `hasnext_true(i)` corresponds to a call to the `hasnext()` method on the same iterator that returns true.

### 4.2.12 Safe usage of locks

This benchmark is provided by the `JAVA-` MOP team. In this benchmark, the property does not hold on the program.

**Description of the monitored program** One considers a simple program with 6 threads. Give of the threads release the same number of times as they acquire a lock. However, one thread releases one time less than it acquires. Consequently, the program does not terminate.

**Description of the property** The property requires a thread to **release** as many times as it **acquires** a lock. Otherwise, it may cause deadlock and the program may not terminate. The following CFG formalizes the property.

$$ 
\begin{array}{l}
S \rightarrow S \begin{array}{l} \mathit{begin}(t) \\ \mathit{end}(t) \end{array} \\
\qquad \mid S \begin{array}{l} \mathit{acquire}(t, 1) \\ \mathit{release}(t, 1) \end{array} \\
\qquad \mid \epsilon
\end{array}
$$

Events `begin(t)` and `end(t)` map to the start and the end of the execution of a thread $t$, respectively. Events `acquire(t, 1)` and `release(t, 1)` map, respectively, to a call to methods `lock()` and ` unlock()` on lock 1 in a thread $t$.

### 4.2.13 Calling methods the same number of times

This benchmark is provided by the `JAVA-` MOP team. In this benchmark, the property does not hold on the program.

**Description of the monitored program** One considers a simple program which calls some dummy methods `A()`, `B()`, and `C()` a certain number of times. These methods are not called the same number of times.

**Description of the property** The property states that methods `A()`, `B()`, and `C()` should be called equal times. The following SRS (String Rewriting System) formalizes the property.

$$ 
\begin{array}{l}
b a \rightarrow a b . \\
c a \rightarrow a c . \\
c b \rightarrow b c . \\
a b \rightarrow E . \\
E b \rightarrow b E . \\
E a \rightarrow a E . \\
E c \rightarrow \epsilon \\
c E \rightarrow \epsilon \\
\qquad \text{^ done} \rightarrow \#\text{succeed} . \\
a \text{ done} \rightarrow \#\text{fail} . \\
b \text{ done} \rightarrow \#\text{fail} . \\
c \text{ done} \rightarrow \#\text{fail} .
\end{array}
$$

Events `a`, `b` and `c` map to the calls to the methods `A()`, `B()`, and `C()`, respectively. The event `done` corresponds to the end of a program.
routes. Blocking a route is indicated by a call to `block(Route route)`. Freeing a route is indicated by a call to `free(Route route)`. A route is a simple line segment described by a starting and end point. The mentioned property can be formulated as: If a point `p` belongs to a route that is being blocked, no other route that contains `p` can be blocked as long as `p` has not been freed again. (The point `p` is freed by freeing a route that contains `p`.) Formally:

$$ 
\begin{aligned}
\forall p \ G(\mathit{block} \land \mathit{onRoute}(p) \\
\qquad \Rightarrow \bar{X}(\neg(\mathit{block} \land \mathit{onRoute}(p)) \\
\qquad \qquad \bar{U}(\mathit{free} \land \mathit{onRoute}(p))))
\end{aligned}
$$

The observed events are the calls to methods `block` and `free`. Let `q` and `r` be the start and end points, respectively, given as arguments to the called method. The only observation symbol is `onRoute(p)` which indicates whether a point `p` is on the route between `q` and `r`. This predicate can be expressed as an equation `onRoute(p) := ∃c (p = q + c · (r − q) ∧ 0 ≤ c ≤ 1)`. *Example traces* A positive example would be the sequence

$$ 
\begin{aligned}
\{\mathit{block}, \mathit{onRoute} \mapsto \{p \mid \exists c \mid 0 \le c \le 1 (p = (1, 2) + c \cdot (2, 2))\}, \\
\{\mathit{free}, \mathit{onRoute} \mapsto \{p \mid \exists c \mid 0 \le c \le 1 (p = (1, 2) + c \cdot (1, 1))\},
\end{aligned}
$$

a negative example the sequence

$$ 
\begin{aligned}
\{\mathit{block}, \mathit{onRoute} \mapsto \{p \mid \exists c \mid 0 \le c \le 1 (p = (1, 2) + c \cdot (2, 2))\}, \\
\{\mathit{block}, \mathit{onRoute} \mapsto \{p \mid \exists c \mid 0 \le c \le 1 (p = (2, 2) + c \cdot (-1, 1))\}.
\end{aligned}
$$

### 4.2.11 HasNext on DaCapo Avrora

This benchmark is provided by the `JAVA-` MOP team. The benchmark considers the (classical) **HasNext** property on one of the so-called DaCapo [22] benchmark. In this benchmark, the property does not hold on the program.

*Description of the monitored program* The considered program is the DaCapo Avrora benchmark, which simulates a number of programs running on a grid of AVR microcontrollers. The program is slightly modified to violate the **HasNext** property intentionally.

*Description of the property* This property requires that the `hasNext()` method is called and returns true before calling `next()` method for each `Iterator` object `i`. It may raise a false positive because one may safely call method `next()` multiple times after retrieving the actual number of elements. The following LTL describes the **HasNext** property.

$$ \forall i G(next(i) \implies Yhasnext_true(i)) $$

In the formula, $X^{-1}$ means previous. Event `next(i)` corresponds to a call to the method `next()` on iterator `i` and event `hasnext_true(i)` corresponds to a call to the `hasnext()` method on the same iterator that returns true.

### 4.2.12 Safe usage of locks

This benchmark is provided by the `JAVA-` MOP team. In this benchmark, the property does not hold on the program.

*Description of the monitored program* One considers a simple program with 6 threads. Give of the threads release the same number of times as they acquire a lock. However, one thread releases one time less than it acquires. Consequently, the program does not terminate.

*Description of the property* The property requires a thread to **release** as many times as it **acquires** a lock. Otherwise, it may cause deadlock and the program may not terminate. The following CFG formalizes the property.

$$ 
\begin{array}{l}
S \rightarrow S \begin{array}{l} \mathit{begin}(t) \\ \mathit{end}(t) \end{array} \\
\qquad \mid S \begin{array}{l} \mathit{acquire}(t, 1) \\ \mathit{release}(t, 1) \end{array} \\
\qquad \mid \epsilon
\end{array}
$$

Events `begin(t)` and `end(t)` map to the start and the end of the execution of a thread `t`, respectively. Events `acquire(t, 1)` and `release(t, 1)` map, respectively, to a call to methods `lock()` and ` unlock()` on lock `l` in a thread `t`.

### 4.2.13 Calling methods the same number of times

This benchmark is provided by the `JAVA-` MOP team. In this benchmark, the property does not hold on the program.

*Description of the monitored program* One considers a simple program which calls some dummy methods `A()`, `B()`, and `C()` a certain number of times. These methods are not called the same number of times.

*Description of the property* The property states that methods `A()`, `B()`, and `C()` should be called equal times. The following SRS (String Rewriting System) formalizes the property.

$$ 
\begin{array}{l}
b a \rightarrow a b . \\
c a \rightarrow a c . \\
c b \rightarrow b c . \\
a b \rightarrow E . \\
E b \rightarrow b E . \\
E a \rightarrow a E . \\
E c \rightarrow \epsilon \\
c E \rightarrow \epsilon \\
\qquad \^ \text{ done} \rightarrow \#\text{succeed} . \\
a \text{ done} \rightarrow \#\text{fail} . \\
b \text{ done} \rightarrow \#\text{fail} . \\
c \text{ done} \rightarrow \#\text{fail} .
\end{array}
$$

Events `a`, `b` and `c` map to the calls to the methods `A()`, `B()`, and `C()`, respectively. The event `done` corresponds to the end of a program.
### 4.2.14 Safe usage of maps with iterators

This benchmark is provided by the JAVA- MOP team. In this benchmark, the property does not hold on the program.

**Description of the monitored program** The program has 3 iterators for 2 collections which are created from 2 different maps. The usage of one iterator in this program creates an unsafe map iterator.

**Description of the property** This property matches the case where a collection created from a map is modified while it is iterated. The following extended regular expression describes the property.

```java
createColl.update*.createIter
    .useIter*.update+.useIter
```

The events map to the following pointcuts in a program:

```java
event createColl after(Map map)
    returning(Collection c) :
        (call(* Map.values())
         || call(* Map keySet())
         && target(map) {}
```

```java
event createIter after(Collection c)
    returning(Iterator i) :
        call(* Collectionphantom sveiterator())
        && target(c) {}
```

```java
event useIter before(Iterator i) :
    call(* Iterator.next())
    && target(i) {}
```

```java
event update after(Map map) :
    (call(* Map.putAll(..))
     || call(* Map.putAll*(..))
     || call(* Map.clear())
     || call(* Map.remove*(..))
    && target(map) {}
```

### 4.2.15 HasNext on full DaCapo

This benchmark is provided by the PRM4J team.

**Description of the monitored program** This benchmark considers the full DaCapo [22] benchmark suite for evaluation.

This consists of X programs of varying size and complexity.

**Description of the property** The property being monitored is the same as that described in Sects. 4.2.11 and 4.2.20, i.e., a property about the safe usage of next() on Java Iterators.

In PRM4J, this property can be specified using the following Java code:

```java
public class FSM_HasNext {
    public final Alphabet alphabet
        = new Alphabet();
    public final Parameter<Iterator> i =
        alphabet.createParameter
            ("i", Iterator.class);
```

```java
public final Symbol1<Iterator>
    hasNext =
        alphabet.createSymbol1
            ("hasNext", i);
public final Symbol1<Iterator> next =
    alphabet.createSymbol1("next", i);
public final FSM fsm = new
    FSM(alphabet);
public final MatchHandler
    matchHandler =
        MatchHandler.NO_OP;
public final FSMState initial =
    fsm.createInitialState();
public final FSMState safe =
    fsm.createState();
public final FSMState error =
    fsm.createAcceptingState
        (matchHandler);
public FSM_HasNext() {
    initial.addTransition(hasNext, safe);
    initial.addTransition(next, error);
    safe.addTransition(hasNext, safe);
    safe.addTransition(next, initial);
    error.addTransition(next, error);
    error.addTransition(hasNext, safe);
}
```

### 4.2.16 SafeSyncCollection on full DaCapo

This benchmark is provided by the PRM4J team.

**Description of the monitored program** This benchmark considers the same programs as that in Sect. 4.2.15.

**Description of the property** The property being monitored relates to the safe usage of collections created using the Collections.synchronized() method. The property is that if a synchronized collection is created in this way, then there are two invalid actions that should be detected. Firstly, an iterator should not be created for the collection by a thread not holding the collection's lock. Secondly, if an iterator is created correctly (i.e., while holding the lock), then it should not be used incorrectly (i.e., without the lock).

In PRM4J, this property can be specified using the following finite state machine. The preceding definitions have been omitted for conciseness.

```java
public FSM_SafeSyncCollection() {
    initial.addTransition sync, s1);
    initial.addTransition
        (asyncCreateIter, initial);
    initial.addTransition
        (syncCreateIter, initial);
    initial.addTransition
        (accessIter, initial);
    s1.addTransition
        (asyncCreateIter, error);
    s1.addTransition
```
### 4.2.14 Safe usage of maps with iterators

This benchmark is provided by the JAVA- MOP team. In this benchmark, the property does not hold on the program.

**Description of the monitored program** The program has 3 iterators for 2 collections which are created from 2 different maps. The usage of one iterator in this program creates an unsafe map iterator.

**Description of the property** This property matches the case where a collection created from a map is modified while it is iterated. The following extended regular expression describes the property.

```java
createColl.update*.createIter
    .useIter*.update+.useIter
```

The events map to the following pointcuts in a program:

```java
event createColl after(Map map)
    returning(Collection c) :
        (call(* Map.values())
        || call(* Map keySet())
        && target(map) {}
```

```java
event createIter after(Collection c)
    returning(Iterator i) :
        call(* Collectionphantom除外のiterable)
        && target(c) {}
```

```java
event useIter before(Iterator i) :
    call(* Iterator.next())
    && target(i) {}
```

```java
event update after(Map map) :
    (call(* Map.putAll(..))
    || call(* Map.putAll*(..))
    || call(* Map.clear())
    || call(* Map.remove*(..))
    && target(map) {}
```

### 4.2.15 HasNext on full DaCapo

This benchmark is provided by the PRM4J team.

**Description of the monitored program** This benchmark considers the full DaCapo [22] benchmark suite for evaluation.

This consists of X programs of varying size and complexity.

**Description of the property** The property being monitored is the same as that described in Sects. 4.2.11 and 4.2.20, i.e., a property about the safe usage of `next()` on Java Iterators.

In PRM4J, this property can be specified using the following Java code:

```java
public class FSM_HasNext {
    public final Alphabet alphabet
        = new Alphabet();
    public final Parameter<Iterator> i =
        alphabet.createParameter
            ("i", Iterator.class);
```

```java
public final Symbol1<Iterator>
    hasNext =
        alphabet.createSymbol1
            ("hasNext", i);
public final Symbol1<Iterator> next =
    alphabet.createSymbol1("next", i);
public final FSM fsm = new
    FSM(alphabet);
public final MatchHandler
    matchHandler =
        MatchHandler.NO_OP;
public final FSMState initial =
    fsm.createInitialState();
public final FSMState safe =
    fsm.createState();
public final FSMState error =
    fsm.createAcceptingState
        (matchHandler);
public FSM_HasNext() {
    initial.addTransition(hasNext, safe);
    initial.addTransition(next, error);
    safe.addTransition(hasNext, safe);
    safe.addTransition(next, initial);
    error.addTransition(next, error);
    error.addTransition(hasNext, safe);
}
```

### 4.2.16 SafeSyncCollection on full DaCapo

This benchmark is provided by the PRM4J team.

**Description of the monitored program** This benchmark considers the same programs as that in Sect. 4.2.15.

**Description of the property** The property being monitored relates to the safe usage of collections created using the `Collections.synchronized()` method. The property is that if a *synchronized* collection is created in this way, then there are two invalid actions that should be detected. Firstly, an iterator should not be created for the collection by a thread not holding the collection's lock. Secondly, if an iterator is created correctly (i.e., while holding the lock), then it should not be used incorrectly (i.e., without the lock).

In PRM4J, this property can be specified using the following finite state machine. The preceding definitions have been omitted for conciseness.

```java
public FSM_SafeSyncCollection() {
    initial.addTransition.sync, s1);
    initial.addTransition
        (asyncCreateIter, initial);
    initial.addTransition
        (syncCreateIter, initial);
    initial.addTransition
        (accessIter, initial);
    s1.addTransition
        (asyncCreateIter, error);
    s1.addTransition
```
```java
    (syncCreateIter, s2);
    s2.addTransition
        (accessIter, error);
}
```

The sync event relates to create a synchronized collection, the asyncCreateIter and syncCreateIter events relate to creating iterators with and without the collection's lock respectively and the accessIter event is the 'bad' access without holding the lock.

### 4.2.17 UnsafeIterator on full DaCapo

This benchmark is provided by the PRM4J team.

**Description of the monitored program** This benchmark considers the same programs as that in Sect. 4.2.15.

**Description of the property** The property being monitored is a common property relating Java Iterators and the collections they are create from. It states that an Iterator *i* created from a Collection *c* is invalid and should be used after *c* has been updated. In PRM4J, this property can be specified using the following finite state machine. The preceding definitions have been omitted for conciseness.

```java
public FSM_UnsafeIterator() {
    initial.addTransition/updateColl,
        (initial);
    initial.addTransition/useIter, initial;
    initial.addTransition/createIter, s1;
    s1.addTransition/useIter, s1;
    s1.addTransition/updateColl, s2;
    s2.addTransition/updateColl, s2;
    s2.addTransition/useIter, error;
}
```

The state machine describes the path to an error state, i.e., creating an iterator, updating the collection and then using the iterator.

### 4.2.18 UnsafeMapIterator on full DaCapo

This benchmark is provided by the PRM4J team.

**Description of the monitored program** This benchmark considers the same programs as that in Sect. 4.2.15.

**Description of the property** The property being monitored is the same as that described in Sect. 4.2.14. In PRM4J, this property can be specified using the following state machine. The preceding definitions have been omitted for conciseness.

```java
public FSM_UnsafeMapIterator() {
    initial.addTransition
        (createColl, s1);
    initial.addTransition
        (updateMap, initial);
    initial.addTransition
        (useIter, initial);
    initial.addTransition
        (createIter, initial);
    s1.addTransition/updateMap, s1;
    s1.addTransition/createIter, s2;
}
```

```java
    s2.addTransition(useIter, s2);
    s2.addTransition/updateMap, s3);
    s3.addTransition/updateMap, s3);
    s3.addTransition(useIter, error);
}
```

### 4.2.19 Combination of properties on DaCapo suite

This benchmark is provided by the PRM4J team. The benchmark checks the combination of the properties described in Sects. 4.2.15, 4.2.17 and 4.2.18 on the full DaCapo benchmark suite.

### 4.2.20 HasNext on DaCapo Batik

This benchmark is provided by the QEA team.

**Description of the monitored program** The considered program is the DaCapo [22] Batik benchmark, which is a single-threaded benchmark that produces a number of Scalable Vector Graphics (SVG) images based on the unit tests in Apache Batik.

**Description of the property** This is the standard iterator based property used frequently as an example for runtime verification of Java properties. Informally, the Java API requires that for each Iterator object the hasNext() method be called and return true before the next() method is called. The following QEA captures the HasNext property. There are two states which capture the status of unsafe and safe iteration, respectively, i.e., when it is valid to call next() (mapped to donext to distinguish it from the state modifier). A hasnext event with a true result fires a transition from the unsafe to safe state. A donext event in the unsafe state leads to failure.

```java
qea {
    Forall (i)
        accept skip (unsafe) {
            hasnext(i,r) if [ r = true ] ->
                safe
            donext(i) -> failure
        }
        accept skip (safe) {
            donext(i) -> unsafe
        }
}
```

The hasnext and donext events relate to the corresponding events in java.utilNAVerator. For example, the following traces satisfy the property

$$ \tau_1 = \text{hasnext}(A, \text{true}).\text{donext}(A).\text{hasnext}(A, \text{true}).\text{donext}(A).\text{hasnext}(A, \text{false}) $$

$$ \tau_2 = \text{hasnext}(A, \text{true}).\text{hasnext}(B, \text{true}).\text{donext}(B).\text{hasnext}(B, \text{false}).\text{donext}(A).\text{hasnext}(A, \text{false}) $$
```java
    (syncCreateIter, s2);
    s2.addTransition
        (accessIter, error);
}
```

The sync event relates to create a synchronized collection, the asyncCreateIter and syncCreateIter events relate to creating iterators with and without the collection's lock respectively and the accessIter event is the 'bad' access without holding the lock.

### 4.2.17 UnsafeIterator on full DaCapo

This benchmark is provided by the PRM4J team.

**Description of the monitored program** This benchmark considers the same programs as that in Sect. 4.2.15.

**Description of the property** The property being monitored is a common property relating Java Iterators and the collections they are create from. It states that an Iterator *i* created from a Collection *c* is invalid and should be used after *c* has been updated. In PRM4J, this property can be specified using the following finite state machine. The preceding definitions have been omitted for conciseness.

```java
public FSM_UnsafeIterator() {
    initial.addTransition/updateColl,
        (initial);
    initial.addTransition/useIter, initial;
    initial.addTransition/createIter, s1;
    s1.addTransition/useIter, s1;
    s1.addTransition/updateColl, s2;
    s2.addTransition/updateColl, s2;
    s2.addTransition/useIter, error;
}
```

The state machine describes the path to an error state, i.e., creating an iterator, updating the collection and then using the iterator.

### 4.2.18 UnsafeMapIterator on full DaCapo

This benchmark is provided by the PRM4J team.

**Description of the monitored program** This benchmark considers the same programs as that in Sect. 4.2.15.

**Description of the property** The property being monitored is the same as that described in Sect. 4.2.14. In PRM4J, this property can be specified using the following state machine. The preceding definitions have been omitted for conciseness.

```java
public FSM_UnsafeMapIterator() {
    initial.addTransition
        (createColl, s1);
    initial.addTransition
        (updateMap, initial);
    initial.addTransition
        (useIter, initial);
    initial.addTransition
        (createIter, initial);
    s1.addTransition/updateMap, s1;
    s1.addTransition/createIter, s2;
}
```

```java
    s2.addTransition(useIter, s2);
    s2.addTransition/updateMap, s3);
    s3.addTransition/updateMap, s3);
    s3.addTransition(useIter, error);
}
```

### 4.2.19 Combination of properties on DaCapo suite

This benchmark is provided by the PRM4J team. The benchmark checks the combination of the properties described in Sects. 4.2.15, 4.2.17 and 4.2.18 on the full DaCapo benchmark suite.

### 4.2.20 HasNext on DaCapo Batik

This benchmark is provided by the QEA team.

**Description of the monitored program** The considered program is the DaCapo [22] Batik benchmark, which is a single-threaded benchmark that produces a number of Scalable Vector Graphics (SVG) images based on the unit tests in Apache Batik.

**Description of the property** This is the standard iterator based property used frequently as an example for runtime verification of Java properties. Informally, the Java API requires that for each Iterator object the hasNext() method be called and return true before the next() method is called. The following QEA captures the HasNext property. There are two states which capture the status of unsafe and safe iteration, respectively, i.e., when it is valid to call next() (mapped to donext to distinguish it from the state modifier). A hasnext event with a true result fires a transition from the unsafe to safe state. A donext event in the unsafe state leads to failure.

```java
qea {
    Forall (i)
        accept skip (unsafe) {
            hasnext(i,r) if [ r = true ] ->
                safe
            donext(i) -> failure
        }
        accept skip (safe) {
            donext(i) -> unsafe
        }
}
```

The hasnext and donext events relate to the corresponding events in java.utilSexIter. For example, the following traces satisfy the property

$$ \tau_1 = \text{hasnext}(A, \text{true}).\text{donext}(A).\text{hasnext}(A, \text{true}).\text{donext}(A).\text{hasnext}(A, \text{false}) $$

$$ \tau_2 = \text{hasnext}(A, \text{true}).\text{hasnext}(B, \text{true}).\text{donext}(B).\text{hasnext}(B, \text{false}).\text{donext}(A).\text{hasnext}(A, \text{false}) $$
and the following traces violate the property

$\tau_3 = \text{hasnext}(A, true).donext(A).donext(A)$

$\tau_4 = \text{hasnext}(A, false).donext(A)$

### 4.2.21 Safe iterators on DaCapo Batik

This benchmark is provided by the QEA team. Description of the monitored program The program is the same program as the one of the benchmarks in Sect. 4.2.20.

Description of the property The HasNext property often leads to false positives when a collection's size is used to iterate over its contents, as is the case in the following code snippet.

```java
int size = collection.size();
Iterator<Object> iter = collection.
    iterator();
for (int i=0; i < size; i++) {
    doStuff(iter.next());
}
```

A more lenient property is to restrict the number of iterations to the size of the underlying collection. The property can be captured by a QEA with two states. The iterate state is entered when the iterator is created and a donext event can occur as long as the number of previous donext events is no more than csize. As iterate is a next state, if the transition cannot be taken due to the guard csize > 0 failing, then there is a transition to the failure state.

```java
qea {
    Forall (i)
        accept skip (start) {
            iterator(i, csize) -> iterate
        }
        accept next (iterate) {
            donext(i) if [ csize > 0 ]
                do [ csize-- ] -> iterate
        }
}
```

Note that to record the iterator event on a call to java.util COLLECTION iterator, a call to size() is required to extract csize. For example, the following traces satisfy the property

$\tau_1 = \text{iterator}(A, 2).donext(A).donext(A)$

$\tau_2 = \text{iterator}(A, 8).donext(A).donext(A)$

and the following trace violates the property

$\tau_3 = \text{iterator}(A, 1).donext(A).donext(A)$

### 4.2.22 Persistent hashcodes on DaCapo Batik

This benchmark is provided by the QEA team.

Description of the monitored program The program is the same program as the one of the benchmarks in Sect. 4.2.20.

Description of the property Hashing structures such as HashMap and HashSet rely on the property that the `hashCode` of an object remains the same while the object is inside the collection. The property can be captured by the following QEA. The states in and out indicate whether the quantified object o is in a hashing structure. The counter count is used to count the number of occurrences. Note that this relies on the fact that these structures are set-like and o cannot belong to a collection more than once. Without this restriction, the QEA would need to also have a quantification over collections. The `hashCode` on insertion is recorded in h and checked later; note the use of a next state to ensure that only valid transitions are taken in the out state.

```java
qea {
    Forall (o)
        accept skip (out) {
            add(c, o, h) do [ count:=1; ] -> in
        }
        accept next (in) {
            add(c, o, h2) if [ h=h2 ]
                do [ count++ ] -> in
            observe(c, o, h2) if [ h=h2 ] -> in
            remove(c, o, h2) if [ count>1 and h=
                h2 ]
                do [ count-- ] -> in
            remove(c, o, h2) if [ count=1 and h=
                h2 ] -> out
        }
}
```

The add, remove, and observe events relate to the successful corresponding (add, put, remove, get, contains, containsKey) methods in java.util.Map or java.util.Map.

For example, the following traces satisfy the property

$\tau_1 = \text{add}(A, O, 5).add(B, O, 5).remove(B, O, 5)$

$\tau_2 = \text{add}(A, M, 5).add(A, N, 6).observe(A, M, 5)$

$\tau_3 = \text{add}(A, O, 5).remove(A, O, 5).add(B, O, 8)$

and the following trace violates the property

$\tau_4 = \text{add}(A, O, 5).add(B, O, 6).remove(B, O, 7)$

$\tau_5 = \text{add}(A, O, 5).add(C, O, 5).remove(A, O, 5).$
add(B, O, 6).observe(B, O, 6).remove(B, O, 6)

The final trace ($\tau_5$) violates the property as object O is still in the collection C when it added to B with a different hash code. The explanation for other traces should be straightforward.

### 4.2.23 Lock ordering on DaCapo Avrora

This benchmark is provided by the QEA team.

Description of the monitored program The considered program is the DaCapo [22] Avrora benchmark, which is a
and the following traces violate the property

$\tau_3 = \text{hasnext}(A, true).donext(A).donext(A)$

$\tau_4 = \text{hasnext}(A, false).donext(A)$

### 4.2.21 Safe iterators on DaCapo Batik

This benchmark is provided by the QEA team. Description of the monitored program The program is the same program as the one of the benchmarks in Sect. 4.2.20.

Description of the property The HasNext property often leads to false positives when a collection's size is used to iterate over its contents, as is the case in the following code snippet.

```java
int size = collection.size();
Iterator<Object> iter = collection.
    iterator();
for (int i=0; i < size; i++) {
    doStuff(iter.next());
}
```

A more lenient property is to restrict the number of iterations to the size of the underlying collection. The property can be captured by a QEA with two states. The iterate state is entered when the iterator is created and a donext event can occur as long as the number of previous donext events is no more than csize. As iterate is a next state, if the transition cannot be taken due to the guard csize > 0 failing, then there is a transition to the failure state.

```java
qea {
    Forall (i)
        accept skip (start) {
            iterator(i, csize) -> iterate
        }
        accept next (iterate) {
            donext(i) if [ csize > 0 ]
                do [ csize-- ] -> iterate
        }
}
```

Note that to record the iterator event on a call to java.util COLLECTION iterator, a call to size() is required to extract csize. For example, the following traces satisfy the property

$\tau_1 = \text{iterator}(A, 2).donext(A).donext(A)$

$\tau_2 = \text{iterator}(A, 8).donext(A).donext(A)$

and the following trace violates the property

$\tau_3 = \text{iterator}(A, 1).donext(A).donext(A)$

### 4.2.22 Persistent hashcodes on DaCapo Batik

This benchmark is provided by the QEA team.

Description of the monitored program The program is the same program as the one of the benchmarks in Sect. 4.2.20.

Description of the property Hashing structures such as HashMap and HashSet rely on the property that the `hashCode` of an object remains the same while the object is inside the collection. The property can be captured by the following QEA. The states in and out indicate whether the quantified object o is in a hashing structure. The counter count is used to count the number of occurrences. Note that this relies on the fact that these structures are set-like and o cannot belong to a collection more than once. Without this restriction, the QEA would need to also have a quantification over collections. The `hashCode` on insertion is recorded in h and checked later; note the use of a next state to ensure that only valid transitions are taken in the out state.

```java
qea {
    Forall (o)
        accept skip (out) {
            add(c, o, h) do [ count:=1; ] -> in
        }
        accept next (in) {
            add(c, o, h2) if [ h=h2 ]
                do [ count++ ] -> in
            observe(c, o, h2) if [ h=h2 ] -> in
            remove(c, o, h2) if [ count>1 and h=
                h2 ]
                do [ count-- ] -> in
            remove(c, o, h2) if [ count=1 and h=
                h2 ] -> out
        }
}
```

The add, remove, and observe events relate to the successful corresponding (add, put, remove, get, contains, containsKey) methods in java.util.Map or java.util.Map.

For example, the following traces satisfy the property

$\tau_1 = \text{add}(A, O, 5).add(B, O, 5).remove(B, O, 5)$

$\tau_2 = \text{add}(A, M, 5).add(A, N, 6).observe(A, M, 5)$

$\tau_3 = \text{add}(A, O, 5).remove(A, O, 5).add(B, O, 8)$

and the following trace violates the property

$\tau_4 = \text{add}(A, O, 5).add(B, O, 6).remove(B, O, 7)$

$\tau_5 = \text{add}(A, O, 5).add(C, O, 5).remove(A, O, 5).$
add(B, O, 6).observe(B, O, 6).remove(B, O, 6)

The final trace ($\tau_5$) violates the property as object O is still in the collection C when it added to B with a different hash code. The explanation for other traces should be straightforward.

### 4.2.23 Lock ordering on DaCapo Avrora

This benchmark is provided by the QEA team.

Description of the monitored program The considered program is the DaCapo [22] Avrora benchmark, which is a
multi-threaded benchmark that uses the available threads to simulate a number of programs run on a grid of AVR microcontrollers.

### Description of the property
A common deadlock avoidance strategy is to order locks to ensure that no cycles can exist between pairs of locks. Note there exists a more general version of this property considering cycles of any length. For the competition, this property was specified using a QEA as follows. Two (non-equal) locks were quantified over, and the state machine captures a 'path to failure,' i.e., the steps required to violate the property.

```
qea {
    Forall (11, 12)
    Where (11 != 12)

    accept skip (start) { lock(11) -> lock1 }
    accept skip (lock1) {
        unlock(11) -> start
        lock(12) -> lock12
    }
    accept skip (lock12) { lock(12) -> lock122 }
    accept skip (lock122) {
        unlock(12) -> lock12
        lock(11) -> failure
    }
}
```

However, after the competition it was pointed out by Klaus Havelund that this formulation is overly restrictive as it does not constrain which threads are taking the locks. A corrected formulation of the property (along with specifications of this property and others from the competition in QEA and LOG-FIRE) can be found in [52].

For example, the following trace satisfies the property

$$ \tau_1 = \text{lock}(A).\text{unlock}(A).\text{lock}(B).\text{ unlock}(B) $$

and the following trace violates the property

$$ \tau_2 = \text{lock}(A).\text{lock}(B).\text{ unlock}(B).\text{ unlock}(A) \\ \text{lock}(B).\text{lock}(A).\text{ unlock}(A).\text{ unlock}(B) $$

note that $\tau_2$ would not violate the corrected version of the property in [52] if the locks were taken by the same thread.

## 4.3 Offline track

### 4.3.1 Maximum chunksize of Dropbox connections

This benchmark is provided by the RiTHM team. Description of the traces The traces of this benchmark are extracted from a real-world dataset [43]. The dataset contains various attributes of Dropbox connections. The dataset is pre-processed, and the details of chunksize used for file-transfer are extracted from the connections.

### Description of the property
This property expresses the requirement that for all connections, it is always the case that chunksize is lesser than or equal to 999 999. The property is formalized using a fragment of first-order LTL [68] as follows:

$$ \forall \text{connection} : G (\text{chunksize} (\text{connection}) \leq 999999) $$

### 4.3.2 Evolution of the chunksize of Dropbox connections

This benchmark is provided by the RiTHM team. Description of the traces. This benchmark uses the same dataset of Dropbox traces as the benchmark in Sect. 4.3.1. This property expresses the requirement that for all connections, it is always the case that when chunksize becomes strictly greater than 100 000, its value eventually becomes lesser than or equal to 100 000.

### Description of the property
The property is formalized using a fragment of first-order LTL [68] as follows:

$$ \begin{array}{l} \forall \text{connection} : G (\text{chunksize} (\text{connection}) > 10,000) \\ \implies F (\text{chunksize} (\text{connection}) \leq 10,000). \end{array} $$

### 4.3.3 Maximum bandwidth for Youtube connections

This benchmark is provided by the RiTHM team.

Description of the traces For this benchmark, RiTHM processes a real-world dataset [85], which contains logs for Youtube connections on a campus network. The dataset is preprocessed, and the value of bandwidth is calculated for each Youtube connection using various parameters in the original data.

### Description of the property
This property expresses the idea that for all connections, it is always the case that the bandwidth lesser than or equal to 100,000. The property is formalized using a fragment of first-order LTL [68] as follows:

$$ \forall \text{connection} : G (\text{bandwidth} (\text{connection}) \leq 100,000) $$

### 4.3.4 Changes in the bandwidth of Youtube connections

This benchmark is provided by the RiTHM team.

Description of the traces This benchmark uses the same dataset of Youtube traces as the benchmark in Sect. 4.3.3.

### Description of the property
The property expresses the requirement that, for all connections, it is always the case that when the bandwidth is strictly greater than 10,000, it eventually becomes lesser than or equal to 10,000. The property is formalized using a fragment of first-order LTL [68] as follows:
multi-threaded benchmark that uses the available threads to simulate a number of programs run on a grid of AVR microcontrollers.

**Description of the property** A common deadlock avoidance strategy is to order locks to ensure that no cycles can exist between pairs of locks. Note there exists a more general version of this property considering cycles of any length. For the competition, this property was specified using a QEA as follows. Two (non-equal) locks were quantified over, and the state machine captures a 'path to failure,' i.e., the steps required to violate the property.

```
qea {
    Forall (11, 12)
    Where (11 != 12)

    accept skip (start) { lock(11) -> lock1 }
    accept skip (lock1) {
        unlock(11) -> start
        lock(12) -> lock12
    }
    accept skip (lock12) { lock(12) -> lock122 }
    accept skip (lock122) {
        unlock(12) -> lock12
        lock(11) -> failure
    }
}
```

However, after the competition it was pointed out by Klaus Havelund that this formulation is overly restrictive as it does not constrain which threads are taking the locks. A corrected formulation of the property (along with specifications of this property and others from the competition in QEA and LOG-FIRE) can be found in [52].

For example, the following trace satisfies the property

$$ \tau_1 = \text{lock}(A).\text{unlock}(A).\text{lock}(B).\text{ unlock}(B) $$

and the following trace violates the property

$$ \tau_2 = \text{lock}(A).\text{lock}(B).\text{ unlock}(B).\text{ unlock}(A) \\ \text{lock}(B).\text{lock}(A).\text{ unlock}(A).\text{ unlock}(B) $$

note that $\tau_2$ would not violate the corrected version of the property in [52] if the locks were taken by the same thread.

## 4.3 Offline track

### 4.3.1 Maximum chunksize of Dropbox connections

This benchmark is provided by the RiTHM team. **Description of the traces** The traces of this benchmark are extracted from a real-world dataset [43]. The dataset contains various attributes of Dropbox connections. The dataset is pre-processed, and the details of chunksize used for file-transfer are extracted from the connections.

**Description of the property** This property expresses the requirement that for all connections, it is always the case that chunksize is lesser than or equal to 999 999. The property is formalized using a fragment of first-order LTL [68] as follows:

$$ \forall connection : G (\text{chunksize}(connection) \leq 999999) $$

### 4.3.2 Evolution of the chunksize of Dropbox connections

This benchmark is provided by the RiTHM team. **Description of the traces** This benchmark uses the same dataset of Dropbox traces as the benchmark in Sect. 4.3.1. This property expresses the requirement that for all connections, it is always the case that when chunksize becomes strictly greater than 100 000, its value eventually becomes lesser than or equal to 100 000.

**Description of the property** The property is formalized using a fragment of first-order LTL [68] as follows:

$$ \begin{array}{l} \forall connection : G (\text{chunksize}(connection) > 10,000) \\ \implies F (\text{chunksize}(connection) \leq 10,000). \end{array} $$

### 4.3.3 Maximum bandwidth for Youtube connections

This benchmark is provided by the RiTHM team.

**Description of the traces** For this benchmark, RiTHM processes a real-world dataset [85], which contains logs for Youtube connections on a campus network. The dataset is preprocessed, and the value of bandwidth is calculated for each Youtube connection using various parameters in the original data.

**Description of the property** This property expresses the idea that for all connections, it is always the case that the bandwidth lesser than or equal to 100,000. The property is formalized using a fragment of first-order LTL [68] as follows:

$$ \forall connection : G (\text{bandwidth}(connection) \leq 100,000) $$

### 4.3.4 Changes in the bandwidth of Youtube connections

This benchmark is provided by the RiTHM team.

**Description of the traces** This benchmark uses the same dataset of Youtube traces as the benchmark in Sect. 4.3.3.

**Description of the property** The property expresses the requirement that, for all connections, it is always the case that when the bandwidth is strictly greater than 10,000, it eventually becomes lesser than or equal to 10,000. The property is formalized using a fragment of first-order LTL [68] as follows:
∀connection :

$$
\begin{align*}
G (\mathit{bandwidth} (\mathit{connection}) > 10,000) \\
\qquad \Rightarrow F \mathit{bandwidth} (\mathit{connection}) \leq 10,000)
\end{align*}
$$

4.3.5 Closing opened files by processes

This benchmark is provided by the RiTHM team.

Description of the traces The log file is obtained by trac-
ing various system calls made by a set of processes, using
strace utility in Linux. The log file of strace is prepro-
cessed to produce an XML file in the format described in
Sect. 2.1. The entries of the log files contain the process IDs,
file descriptors, and the details of the operations performed
on the files.

*Description of the property*
The property expresses require-
ment that for all processes and for all files, it is always the
case that if a file is opened, then it is eventually closed by the
process. A similar condition is expressed for sockets. The
property is formalized using a fragment of first-order LTL
fragment [68] as follows:

∀process, ∀file :

$$
G (\mathit{open} (\mathit{process}, \mathit{file}) \implies \mathit{F close} (\mathit{process}, \mathit{file}))
$$

∧

∀process, ∀socket :

$$
\begin{align*}
G (\mathit{accept}(\mathit{process}, \mathit{socket}) \\
\qquad \Rightarrow \mathit{F close}(\mathit{process}, \mathit{socket}))
\end{align*}
$$

4.3.6 Reporting financial transactions of a banking system

This benchmark is provided by the MONPOLY team. The MONPOLY team provided five benchmarks from different areas (described also in Sects. 4.3.7, 4.3.8, 4.3.9, and 4.3.10). Common to all the benchmarks is that the considered properties are policies in IT systems.

In the following, we describe the log format and the
property of each benchmark. The provided MFOTL formal-
izations are close to MONPOLY’s input format. In particular,
we use a textual representation of the Boolean connectives
and the metric temporal operators. MFOTL’s semantics fol-
lows the standard semantics of first-order logic and the
real-time logic MTL. See [12], for details on MONPOLY’s
specification language.

*Description of the log*
The log file is syntactically generated
and is provided in CSV format. To represent a sequence of
timestamped databases in this format, we have used the con-
ventions explained next, illustrated by the following example.

trans, tp=10, ts=32, c=Alice, t=132, a=2035
trans, tp=10, ts=32, c=Bob, t=135, a=2100
trans, tp=11, ts=32, c=Charlie, t=137, a=60
report, tp=12, ts=38, t=132

Each line corresponds to one tuple in one of the timestamped
databases. The name of the relation to which the tuple belongs
to is given by the first, unnamed field. The next two fields
are: 1) the index of the database in the sequence, called *time
point*, and 2) the timestamp of the database. The other fields
provide the tuple's value on each attribute of the correspond-
ing relation. For instance, the first line in the previous log
excerpt corresponds to a transaction event of the customer
c = Alice with the transaction number t = 132 and the
amount a = 2035. The event was carried out at time 32 and
is at the tenth position of the event stream.

This representation of the MFOTL's semantic models fits
reasonably well with the competition's trace format. That is,
the first field represents the event's name, and all other fields
are the event's parameters. However, events with the same
value of the tp parameter are unordered from the MFOTL
semantics' perspective.

The size of the log is 13MB. The following property is
violated on the log file.

Description of the property

This property formalizes a compliance policy for a bank-
ing system that processes customer transactions. It stipulated
that executed transactions *t* of any customer *c* must be
reported within at most five days if the transferred amount *a*
exceeds $2000. The property’s formalization in MFOTL is:

ALWAYS FORALL c, t, a.
trans(c, t, a) AND 2000 < a IMPLIES
EVENTUALLY[0, 5] report(t).

The event trans(c, t, a) denotes that the client c performs the
transaction t, transferring the amount a. The event report(t)
denotes that the transaction t is reported. The temporal oper-
ator ALWAYS requires that the policy is satisfied at every
time point. The interval attached to the temporal operator
EVENTUALLY specifies that transactions must be reported
within zero to five days.

Assuming that the previous log excerpt represents the
complete event stream, we observe that there are two viola-
tions. First, the event trans(Alice, 132, 2035) that occurred
on day 32 is reported too late, namely on day 38. Second, the
event trans(Bob, 135, 2100) is not reported at all.

4.3.7 Authorizing financial transactions in a banking system

This benchmark is provided by the MONPOLY team.

*Description of the log*
The description of the log format is
presented in Sect. 4.3.6. The size of the log is 13MB. The
following property is violated on the log file.

*Description of the property*
This property also formalizes a
compliance policy for a banking system that processes cus-
tomer transactions. It stipulates that executed transactions *t*
of any customer *c* must be authorized by some employee *e*

<figure><img src="image_9.png" /></figure>
∀connection :

$$
\begin{array}{l}
G (\text{bandwidth (connection)} > 10,000) \\
\quad \Rightarrow \quad F \text{ bandwidth (connection)} \le 10,000)
\end{array}
$$

4.3.5 Closing opened files by processes

This benchmark is provided by the RiTHM team.

Description of the traces The log file is obtained by trac-
ing various system calls made by a set of processes, using
strace utility in Linux. The log file of strace is prepro-
cessed to produce an XML file in the format described in
Sect. 2.1. The entries of the log files contain the process IDs,
file descriptors, and the details of the operations performed
on the files.

*Description of the property*
The property expresses require-
ment that for all processes and for all files, it is always the
case that if a file is opened, then it is eventually closed by the
process. A similar condition is expressed for sockets. The
property is formalized using a fragment of first-order LTL
fragment [68] as follows:

∀process, ∀file :

$$
G (\mathit{open} (\mathit{process}, \mathit{file}) \implies \mathit{F close} (\mathit{process}, \mathit{file}))
$$

∧

∀process, ∀socket :

$$
\begin{array}{l}
G (\mathit{accept}(\mathit{process}, \mathit{socket}) \\
\quad \Rightarrow \quad F \mathit{close}(\mathit{process}, \mathit{socket}))
\end{array}
$$

4.3.6 Reporting financial transactions of a banking system

This benchmark is provided by the MONPOLY team. The MONPOLY team provided five benchmarks from different areas (described also in Sects. 4.3.7, 4.3.8, 4.3.9, and 4.3.10). Common to all the benchmarks is that the considered properties are policies in IT systems.

In the following, we describe the log format and the
property of each benchmark. The provided MFOTL formal-
izations are close to MONPOLY’s input format. In particular,
we use a textual representation of the Boolean connectives
and the metric temporal operators. MFOTL’s semantics fol-
lows the standard semantics of first-order logic and the
real-time logic MTL. See [12], for details on MONPOLY’s
specification language.

*Description of the log*
The log file is syntactically generated
and is provided in CSV format. To represent a sequence of
timestamped databases in this format, we have used the con-
ventions explained next, illustrated by the following example.

trans, tp=10, ts=32, c=Alice, t=132, a=2035
trans, tp=10, ts=32, c=Bob, t=135, a=2100
trans, tp=11, ts=32, c=Charlie, t=137, a=60
report, tp=12, ts=38, t=132

Each line corresponds to one tuple in one of the timestamped
databases. The name of the relation to which the tuple belongs
to is given by the first, unnamed field. The next two fields
are: 1) the index of the database in the sequence, called *time
point*, and 2) the timestamp of the database. The other fields
provide the tuple's value on each attribute of the correspond-
ing relation. For instance, the first line in the previous log
excerpt corresponds to a transaction event of the customer
c = Alice with the transaction number t = 132 and the
amount a = 2035. The event was carried out at time 32 and
is at the tenth position of the event stream.

This representation of the MFOTL's semantic models fits
reasonably well with the competition's trace format. That is,
the first field represents the event's name, and all other fields
are the event's parameters. However, events with the same
value of the tp parameter are unordered from the MFOTL
semantics' perspective.

The size of the log is 13MB. The following property is
violated on the log file.

Description of the property

This property formalizes a compliance policy for a bank-
ing system that processes customer transactions. It stipulated
that executed transactions *t* of any customer *c* must be
reported within at most five days if the transferred amount *a*
exceeds $2000. The property’s formalization in MFOTL is:

ALWAYS FORALL c, t, a.
trans(c, t, a) AND 2000 < a IMPLIES
EVENTUALLY[0, 5] report(t).

The event trans(c, t, a) denotes that the client c performs the
transaction t, transferring the amount a. The event report(t)
denotes that the transaction t is reported. The temporal oper-
ator ALWAYS requires that the policy is satisfied at every
time point. The interval attached to the temporal operator
EVENTUALLY specifies that transactions must be reported
within zero to five days.

Assuming that the previous log excerpt represents the
complete event stream, we observe that there are two viola-
tions. First, the event trans(Alice, 132, 2035) that occurred
on day 32 is reported too late, namely on day 38. Second, the
event trans(Bob, 135, 2100) is not reported at all.

4.3.7 Authorizing financial transactions in a banking system

This benchmark is provided by the MONPOLY team.

*Description of the log*
The description of the log format is
presented in Sect. 4.3.6. The size of the log is 13MB. The
following property is violated on the log file.

*Description of the property*
This property also formalizes a
compliance policy for a banking system that processes cus-
tomer transactions. It stipulates that executed transactions *t*
of any customer *c* must be authorized by some employee *e*

<figure><img src="image_8.png" /></figure>
before they are executed if the transferred amount *a* exceeds $ 2000. The property's formalization in MFOTL is:

ALWAYS FORALL c, t, a.
trans(c, t, a) AND 2000 < a IMPLIES
ONCE[2, 20] EXISTS e. auth(e, t).

The event `trans(c, t, a)` is as in Property 1. The event `auth(e, t)` denotes the authorization of the transaction `t` by the employee `e`. Similar to Property 1, the interval `[2, 20]` attached to the temporal past-time operator `ONCE` specifies the time period in which transactions must be authorized.

### 4.3.8 Approval policy of business reports within a company

This benchmark is provided by the MONPOLY team.

**Description of the log** The description of the log format is presented in Sect. 4.3.6. The size of the log is 2MB. The following property is violated on the log file.aa

**Description of the property** This property formalizes an approval policy for publishing business reports within a company. It stipulates that any report must be approved prior to its publication. Furthermore, the person who publishes the report must be an accountant and the person who approves the publication must be the accountant's manager. Finally, the approval must happen within at most ten days before the publication. The property's formalization in MFOTL is:

ALWAYS FORALL a, f.
publish(a, f) IMPLIES
(NOT acc<sub>F</sub>(a) SINCE acc<sub>S</sub>(a)) AND
ONCE[0, 10] EXISTS m. approve(m, f) AND
(NOT mgr<sub>F</sub>(m, a) SINCE mgr<sub>S</sub>(m, a)).

The event `publish(a, f)` denotes the publication of the report `f` by `a`. The event `approve(m, f)` denotes that `m` approves to publish the report `f`. The event `acc<sub>S</sub>(a)` marks the time when `a` starts being an accountant and the event `acc<sub>F</sub>(a)` marks the corresponding finishing time. The subformula `NOT acc<sub>F</sub>(a) SINCE acc<sub>S</sub>(a)` thus specifies when `a` is an accountant. Analogously, the events `mgr<sub>S</sub>(m, a)` and `mgr<sub>F</sub>(m, a)` mark the starting and finishing times of `m` being `a`'s manager.

### 4.3.9 Withdrawals of users over time

This benchmark is provided by the MONPOLY team.

**Description of the log** The description of the log format is presented in Sect. 4.3.6. The size of the log is 10MB. The following property is violated on the log file.

**Description of the property** This property is rooted in the domain of fraud detection. It stipulates that the sum of withdrawals of each user in the last 28 days does not exceed the

limit of $ 10,000. The property's formalization is:

ALWAYS FORALL s, u.
(s ← SUM a; u. ONCE[0, 28] withdraw(u, a) AND tp(i))
IMPLIES
s ≤ 10,000.

The event `withdraw(u, a)` denotes the withdrawal by the user `u` of the amount `a`. The event `tp(i)` denotes that the current time point is `i`. This event is used in the formalization to distinguish different events `withdraw(u, a)` with the same values for `u` and `a` in the relevant time window. Each user's withdrawals are accumulated into `s` by the aggregation operation `SUM [15]` over the specified time period.

### 4.3.10 Data usage in Nokia's Lausanne data-collection campaign

This benchmark is provided by the MONPOLY team.

**Description of the log** The description of the log format is presented in Sect. 4.3.6. The log file in this benchmark is taken from a real-world case study [65] and is publicly available on the MONPOLY's web page in an anonymized form. The log is 14GB large. The following property is violated on the log file.

**Description of the property** This property is taken from the case study [65]. Several policies stipulate restrictions on the usage of data in Nokia's Lausanne data-collection campaign [65] in which sensitive data is uploaded by smartphones into the database `db1` and propagated to the databases `db2` and `db3`, where it is eventually stored anonymized. The property used for the competition stipulates that data may be inserted into `db3` only if it was inserted into `db2` within the last minute. The property's formalization in MFOTL is:

ALWAYS FORALL u, p, d.
insert(u, db3, p, d) AND d ≠ unknown IMPLIES
ONCE[0, 60) EXISTS u', q. insert(u', db2, q, d).

The event `insert(u, db, p, d)` corresponds to a logged SQL insert operation performed on the database `db` by the database user `u`, involving the campaign participant `p` and the data `d`.

### 4.3.11 Early alarm of machine operations

This benchmark is provided by the STEPR team.

**Description of the log** The log file for this benchmark is an artificially created data set representing the typical shape of event logs produced during machine operations, e.g., during development, testing or productive use. It is inspired by industrial case studies and projects carried out in the safety critical domain. The XML file represents a sequence of events that carry different attributes such as, for example, `alarm`,
before they are executed if the transferred amount *a* exceeds $ 2000. The property's formalization in MFOTL is:

ALWAYS FORALL c, t, a.
trans(c, t, a) AND 2000 < a IMPLIES
ONCE[2, 20] EXISTS e. auth(e, t).

The event trans(c, t, a) is as in Property 1. The event auth(e, t) denotes the authorization of the transaction t by the employee e. Similar to Property 1, the interval [2, 20] attached to the temporal past-time operator ONCE specifies the time period in which transactions must be authorized.

### 4.3.8 Approval policy of business reports within a company

This benchmark is provided by the MONPOLY team.

**Description of the log** The description of the log format is presented in Sect. 4.3.6. The size of the log is 2MB. The following property is violated on the log file.aa

**Description of the property** This property formalizes an approval policy for publishing business reports within a company. It stipulates that any report must be approved prior to its publication. Furthermore, the person who publishes the report must be an accountant and the person who approves the publication must be the accountant's manager. Finally, the approval must happen within at most ten days before the publication. The property's formalization in MFOTL is:

ALWAYS FORALL a, f.
publish(a, f) IMPLIES
(NOT acc<sub>F</sub>(a) SINCE acc<sub>S</sub>(a)) AND
ONCE[0, 10] EXISTS m. approve(m, f) AND
(NOT mgr<sub>F</sub>(m, a) SINCE mgr<sub>S</sub>(m, a)).

The event publish(a, f) denotes the publication of the report f by a. The event approve(m, f) denotes that m approves to publish the report f. The event acc<sub>S</sub>(a) marks the time when a starts being an accountant and the event acc<sub>F</sub>(a) marks the corresponding finishing time. The subformula NOT acc<sub>F</sub>(a) SINCE acc<sub>S</sub>(a) thus specifies when a is an accountant. Analogously, the events mgr<sub>S</sub>(m, a) and mgr<sub>F</sub>(m, a) mark the starting and finishing times of m being a's manager.

### 4.3.9 Withdrawals of users over time

This benchmark is provided by the MONPOLY team.

**Description of the log** The description of the log format is presented in Sect. 4.3.6. The size of the log is 10MB. The following property is violated on the log file.

**Description of the property** This property is rooted in the domain of fraud detection. It stipulates that the sum of withdrawals of each user in the last 28 days does not exceed the

limit of $ 10,000. The property's formalization is:

ALWAYS FORALL s, u.
(s ← SUM a; u. ONCE[0, 28] withdraw(u, a) AND tp(i))
IMPLIES
s ≤ 10,000.

The event withdraw(u, a) denotes the withdrawal by the user u of the amount a. The event tp(i) denotes that the current time point is i. This event is used in the formalization to distinguish different events withdraw(u, a) with the same values for u and a in the relevant time window. Each user's withdrawals are accumulated into s by the aggregation operation SUM [15] over the specified time period.

### 4.3.10 Data usage in Nokia's Lausanne data-collection campaign

This benchmark is provided by the MONPOLY team.

**Description of the log** The description of the log format is presented in Sect. 4.3.6. The log file in this benchmark is taken from a real-world case study [65] and is publicly available on the MONPOLY's web page in an anonymized form. The log is 14GB large. The following property is violated on the log file.

**Description of the property** This property is taken from the case study [65]. Several policies stipulate restrictions on the usage of data in Nokia's Lausanne data-collection campaign [65] in which sensitive data is uploaded by smartphones into the database db1 and propagated to the databases db2 and db3, where it is eventually stored anonymized. The property used for the competition stipulates that data may be inserted into db3 only if it was inserted into db2 within the last minute. The property's formalization in MFOTL is:

ALWAYS FORALL u, p, d.
insert(u, db3, p, d) AND d ≠ unknown IMPLIES
ONCE[0, 60) EXISTS u', q. insert(u', db2, q, d).

The event insert(u, db, p, d) corresponds to a logged SQL insert operation performed on the database db by the database user u, involving the campaign participant p and the data d.

### 4.3.11 Early alarm of machine operations

This benchmark is provided by the STEPR team.

**Description of the log** The log file for this benchmark is an artificially created data set representing the typical shape of event logs produced during machine operations, e.g., during development, testing or productive use. It is inspired by industrial case studies and projects carried out in the safety critical domain. The XML file represents a sequence of events that carry different attributes such as, for example, alarm,
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{array}{l} 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{array} $$

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.