iBet uBet web content aggregator. Adding the entire web to your favor.
iBet uBet web content aggregator. Adding the entire web to your favor.



Link to original content: https://unpaywall.org/10.1007/978-3-319-47169-3_59
RERS 2016: Parallel and Sequential Benchmarks with Focus on LTL Verification | SpringerLink
Skip to main content
Springer Nature Link
Log in

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

  • Conference paper
  • First Online:
Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications (ISoLA 2016)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9953))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    As stated online at http://www.rers-challenge.org/.

  2. 2.

    https://sv-comp.sosy-lab.org/.

  3. 3.

    www.rers-challenge.org/2016/index.php?page=trainingphase.

  4. 4.

    The name was shortened for space reasons, in the challenge the function is named calculate_output.

  5. 5.

    Java version: http://rers-challenge.org/2016/index.php?page=java-code C version: http://rers-challenge.org/2016/index.php?page=c-code.

  6. 6.

    http://www.graphviz.org/content/dot-language.

  7. 7.

    For detailed definitions, please refer to https://spot.lrde.epita.fr/trans.html.

  8. 8.

    http://rv2015.conf.tuwien.ac.at/.

References

  1. Almeida, E.E., Luntz, J.E., Tilbury, D.M.: Event-condition-action systems for reconfigurable logic control. IEEE Trans. Autom. Sci. Eng. 4(2), 167–181 (2007)

    Article  Google Scholar 

  2. Beyer, D.: Status report on software verification. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 373–388. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54862-8_25

    Chapter  Google Scholar 

  3. Beyer, D.: Reliable and reproducible competition results with benchexec and witnesses (report on SV-COMP 2016). In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 887–904. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49674-9_55

    Chapter  Google Scholar 

  4. Broy, M., Jonsson, B., Katoen, J.-P., Leucker, M., Pretschner, A. (eds.): Model-Based Testing of Reactive Systems. LNCS, vol. 3472. Springer, Heidelberg (2005)

    MATH  Google Scholar 

  5. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2001)

    Book  Google Scholar 

  6. Geske, M., Isberner, M., Steffen, B.: Rigorous examination of reactive systems: the RERS challenge 2015. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 423–429. Springer, Heidelberg (2015). doi:10.1007/978-3-319-23820-3_28

    Chapter  Google Scholar 

  7. Holzmann, G.J., Smith, M.H.: Software model checking: extracting verification models from source code. Softw. Test. Verification Reliab. 11(2), 65–79 (2001)

    Article  Google Scholar 

  8. Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual, 1st edn. Addison-Wesley Professional (2011)

    Google Scholar 

  9. Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D., Păsăreanu, C.: Rigorous examination of reactive systems. The RERS challenges 2012 and 2013. Softw. Tools Technol. Transfer 16(5), 457–464 (2014)

    Google Scholar 

  10. Huisman, M., Klebanov, V., Monahan, R.: VerifyThis 2012 - a program verification competition. STTT 17(6), 647–657 (2015)

    Article  Google Scholar 

  11. King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)

    Article  MathSciNet  MATH  Google Scholar 

  12. Kordon, F., Garavel, H., Hillah, L.M., Hulin-Hubard, F., Chiardo, G., Hamez, A., Jezequel, L., Miner, A., Meijer, J., Paviot-Adet, E., Racordon, D., Rodriguez, C., Rohr, C., Srba, J., Thierry-Mieg, Y., Trinh, G., Wolf, K.: Complete Results for the 2016 Edition of the Model Checking Contest, June 2016. http://mcc.lip6.fr/2016/results.php

  13. McCarthy, D., Dayal, U.: The architecture of an active database management system. ACM Sigmod Rec. 18(2), 215–224 (1989). ACM

    Google Scholar 

  14. Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999)

    Book  MATH  Google Scholar 

  15. Schordan, M., Quinlan, D.: A source-to-source architecture for user-defined optimizations. In: Böszörményi, L., Schojer, P. (eds.) JMLC 2003. LNCS, vol. 2789, pp. 214–223. Springer, Heidelberg (2003). doi:10.1007/978-3-540-45213-3_27

    Chapter  Google Scholar 

  16. Steffen, B., Isberner, M., Naujokat, S., Margaria, T., Geske, M.: Property-driven benchmark generation: synthesizing programs of realistic structure. Softw. Tools Technol. Transfer 16(5), 465–479 (2014)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. TU Dortmund University, Programming Systems, 44227, Dortmund, Germany

    Maren Geske, Marc Jasper & Bernhard Steffen

  2. Lawrence Livermore National Laboratory, Livermore, California, 94551, USA

    Marc Jasper & Markus  Schordan

  3. Clausthal University of Technology, Clausthal-Zellerfeld, Germany

    Falk Howar

  4. University of Twente, Formal Methods and Tools, Enschede, The Netherlands

    Jaco van de Pol

Authors
  1. Maren Geske
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marc Jasper
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Bernhard Steffen
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Falk Howar
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Markus  Schordan
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Jaco van de Pol
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Maren Geske .

Editor information

Editors and Affiliations

  1. Lero, Limerick, Ireland

    Tiziana Margaria

  2. TU Dortmund, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Geske, M., Jasper, M., Steffen, B., Howar, F., Schordan, M., van de Pol, J. (2016). RERS 2016: Parallel and Sequential Benchmarks with Focus on LTL Verification. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications. ISoLA 2016. Lecture Notes in Computer Science(), vol 9953. Springer, Cham. https://doi.org/10.1007/978-3-319-47169-3_59

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-47169-3_59

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-47168-6

  • Online ISBN: 978-3-319-47169-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation