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 proceedingConference contributionAcademicpeer-review

    12 Citations (Scopus)
    49 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 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
    Pages787-803
    Number of pages17
    ISBN (Electronic)978-3-319-47169-3
    ISBN (Print)978-3-319-47168-6
    DOIs
    Publication statusPublished - Oct 2016
    Event7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016 - Corfu, Greece
    Duration: 10 Oct 201614 Oct 2016
    Conference number: 7
    http://www.isola-conference.org/isola2016/

    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

    Keywords

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

    Fingerprint Dive into the research topics of 'RERS 2016: Parallel and Sequential Benchmarks with Focus on LTL Verification'. Together they form a unique fingerprint.

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