RERS 2016: Parallel and Sequential Benchmarks with Focus on LTL Verification

M. Geske, M. Jasper, B. Steffen, F. Howar, M. Schordan, Jan Cornelis van de Pol

  • 4 Citations

Abstract

The 5th challenge of Rigorous Examination of Reactive Systems (RERS 2016) once again provided generated and tailored benchmarks suited for comparing the effectiveness of automatic software verifiers. RERS is the only software verification challenge that features problems with linear temporal logic (LTL) properties in larger sizes that are available in different programming languages. This paper describes the revised rules and the refined profile of the challenge, which lowers the entry hurdle for new participants. The challenge format with its three tracks, their benchmarks, and the related LTL and reachability properties are explained. Special emphasis is put on changes that were implemented in RERS - compared to former RERS challenges. The competition comprised 18 sequential and 20 parallel benchmarks. The 20 benchmarks from the new parallel track feature LTL properties and a compact representation as labeled transition systems and Promela code.
Original languageEnglish
Title of host publicationLeveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications
Subtitle of host publication7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part II
EditorsT. Margaria, B. Steffen
Place of PublicationBerlin
PublisherSpringer Verlag
Pages787-803
Number of pages17
ISBN (Electronic)978-3-319-47169-3
ISBN (Print)978-3-319-47168-6
DOIs
StatePublished - Oct 2016
Event7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016 - Corfu, Greece

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume9953
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016
Abbreviated titleISoLA 2016
CountryGreece
CityCorfu
Period10/10/1614/10/16
Internet address

Fingerprint

Temporal logic
Computer programming languages

Keywords

  • CR-D.2.4
  • EWI-27827
  • FMT-MC: MODEL CHECKING

Cite this

Geske, M., Jasper, M., Steffen, B., Howar, F., Schordan, M., & van de Pol, J. C. (2016). RERS 2016: Parallel and Sequential Benchmarks with Focus on LTL Verification. In T. Margaria, & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications: 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part II (pp. 787-803). (Lecture Notes in Computer Science; Vol. 9953). Berlin: Springer Verlag. DOI: 10.1007/978-3-319-47169-3_59

Geske, M.; Jasper, M.; Steffen, B.; Howar, F.; Schordan, M.; van de Pol, Jan Cornelis / RERS 2016 : Parallel and Sequential Benchmarks with Focus on LTL Verification.

Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications: 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part II. ed. / T. Margaria; B. Steffen. Berlin : Springer Verlag, 2016. p. 787-803 (Lecture Notes in Computer Science; Vol. 9953).

Research output: Scientific - peer-reviewConference contribution

@inbook{f7af1d75e29d45b0877c5a355313e1c1,
title = "RERS 2016: Parallel and Sequential Benchmarks with Focus on LTL Verification",
abstract = "The 5th challenge of Rigorous Examination of Reactive Systems (RERS 2016) once again provided generated and tailored benchmarks suited for comparing the effectiveness of automatic software verifiers. RERS is the only software verification challenge that features problems with linear temporal logic (LTL) properties in larger sizes that are available in different programming languages. This paper describes the revised rules and the refined profile of the challenge, which lowers the entry hurdle for new participants. The challenge format with its three tracks, their benchmarks, and the related LTL and reachability properties are explained. Special emphasis is put on changes that were implemented in RERS - compared to former RERS challenges. The competition comprised 18 sequential and 20 parallel benchmarks. The 20 benchmarks from the new parallel track feature LTL properties and a compact representation as labeled transition systems and Promela code.",
keywords = "CR-D.2.4, EWI-27827, FMT-MC: MODEL CHECKING",
author = "M. Geske and M. Jasper and B. Steffen and F. Howar and M. Schordan and {van de Pol}, {Jan Cornelis}",
year = "2016",
month = "10",
doi = "10.1007/978-3-319-47169-3_59",
isbn = "978-3-319-47168-6",
series = "Lecture Notes in Computer Science",
publisher = "Springer Verlag",
pages = "787--803",
editor = "T. Margaria and B. Steffen",
booktitle = "Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications",

}

Geske, M, Jasper, M, Steffen, B, Howar, F, Schordan, M & van de Pol, JC 2016, RERS 2016: Parallel and Sequential Benchmarks with Focus on LTL Verification. in T Margaria & B Steffen (eds), Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications: 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part II. Lecture Notes in Computer Science, vol. 9953, Springer Verlag, Berlin, pp. 787-803, 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016, Corfu, Greece, 10-14 October. DOI: 10.1007/978-3-319-47169-3_59

RERS 2016 : Parallel and Sequential Benchmarks with Focus on LTL Verification. / Geske, M.; Jasper, M.; Steffen, B.; Howar, F.; Schordan, M.; van de Pol, Jan Cornelis.

Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications: 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part II. ed. / T. Margaria; B. Steffen. Berlin : Springer Verlag, 2016. p. 787-803 (Lecture Notes in Computer Science; Vol. 9953).

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

T1 - RERS 2016

T2 - Parallel and Sequential Benchmarks with Focus on LTL Verification

AU - Geske,M.

AU - Jasper,M.

AU - Steffen,B.

AU - Howar,F.

AU - Schordan,M.

AU - van de Pol,Jan Cornelis

PY - 2016/10

Y1 - 2016/10

N2 - The 5th challenge of Rigorous Examination of Reactive Systems (RERS 2016) once again provided generated and tailored benchmarks suited for comparing the effectiveness of automatic software verifiers. RERS is the only software verification challenge that features problems with linear temporal logic (LTL) properties in larger sizes that are available in different programming languages. This paper describes the revised rules and the refined profile of the challenge, which lowers the entry hurdle for new participants. The challenge format with its three tracks, their benchmarks, and the related LTL and reachability properties are explained. Special emphasis is put on changes that were implemented in RERS - compared to former RERS challenges. The competition comprised 18 sequential and 20 parallel benchmarks. The 20 benchmarks from the new parallel track feature LTL properties and a compact representation as labeled transition systems and Promela code.

AB - The 5th challenge of Rigorous Examination of Reactive Systems (RERS 2016) once again provided generated and tailored benchmarks suited for comparing the effectiveness of automatic software verifiers. RERS is the only software verification challenge that features problems with linear temporal logic (LTL) properties in larger sizes that are available in different programming languages. This paper describes the revised rules and the refined profile of the challenge, which lowers the entry hurdle for new participants. The challenge format with its three tracks, their benchmarks, and the related LTL and reachability properties are explained. Special emphasis is put on changes that were implemented in RERS - compared to former RERS challenges. The competition comprised 18 sequential and 20 parallel benchmarks. The 20 benchmarks from the new parallel track feature LTL properties and a compact representation as labeled transition systems and Promela code.

KW - CR-D.2.4

KW - EWI-27827

KW - FMT-MC: MODEL CHECKING

U2 - 10.1007/978-3-319-47169-3_59

DO - 10.1007/978-3-319-47169-3_59

M3 - Conference contribution

SN - 978-3-319-47168-6

T3 - Lecture Notes in Computer Science

SP - 787

EP - 803

BT - Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications

PB - Springer Verlag

ER -

Geske M, Jasper M, Steffen B, Howar F, Schordan M, van de Pol JC. RERS 2016: Parallel and Sequential Benchmarks with Focus on LTL Verification. In Margaria T, Steffen B, editors, Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications: 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part II. Berlin: Springer Verlag. 2016. p. 787-803. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-319-47169-3_59