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

doi:10.1007/978-3-319-47169-3_59

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

13 Citations (Scopus)

101 Downloads (Pure)

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 language	English
Title of host publication	Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications
Subtitle of host publication	7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part II
Editors	T. Margaria, B. Steffen
Place of Publication	Berlin
Publisher	Springer
Pages	787-803
Number of pages	17
ISBN (Electronic)	978-3-319-47169-3
ISBN (Print)	978-3-319-47168-6
DOIs	https://doi.org/10.1007/978-3-319-47169-3_59
Publication status	Published - Oct 2016
Event	7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016 - Corfu, Greece Duration: 10 Oct 2016 → 14 Oct 2016 Conference number: 7 http://www.isola-conference.org/isola2016/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Verlag
Volume	9953
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016
Abbreviated title	ISoLA 2016
Country/Territory	Greece
City	Corfu
Period	10/10/16 → 14/10/16
Internet address	http://www.isola-conference.org/isola2016/

Keywords

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

Access to Document

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

RERS 2016Accepted author version, 636 KB

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). Springer. https://doi.org/10.1007/978-3-319-47169-3_59

Geske, M. ; Jasper, M. ; Steffen, B. et al. / 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. editor / T. Margaria ; B. Steffen. Berlin : Springer, 2016. pp. 787-803 (Lecture Notes in Computer Science).

@inproceedings{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 = oct,

doi = "10.1007/978-3-319-47169-3_59",

language = "English",

isbn = "978-3-319-47168-6",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "787--803",

editor = "T. Margaria and B. Steffen",

booktitle = "Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications",

note = "7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016, ISoLA 2016 ; Conference date: 10-10-2016 Through 14-10-2016",

url = "http://www.isola-conference.org/isola2016/",

}

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, Berlin, pp. 787-803, 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016, Corfu, Greece, 10/10/16. https://doi.org/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. et al.
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, 2016. p. 787-803 (Lecture Notes in Computer Science; Vol. 9953).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - RERS 2016

T2 - 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016

AU - Geske, M.

AU - Jasper, M.

AU - Steffen, B.

AU - Howar, F.

AU - Schordan, M.

AU - van de Pol, Jan Cornelis

N1 - Conference code: 7

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

A2 - Margaria, T.

A2 - Steffen, B.

PB - Springer

CY - Berlin

Y2 - 10 October 2016 through 14 October 2016

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. 2016. p. 787-803. (Lecture Notes in Computer Science). doi: 10.1007/978-3-319-47169-3_59