Skip to main content
SpringerLink
Log in

Counterexample-Guided Prefix Refinement Analysis for Program Verification

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

Part of the book series: Communications in Computer and Information Science ((CCIS,volume 683))

Included in the following conference series:

Abstract

Counterexample-guided abstraction refinement (cegar) has become a successful approach to the automatic verification of program properties. Starting from a coarse abstract model, cegar incrementally refines the model based on spurious counterexamples that are retrieved from model checking attempts. In addition to purely symbolic representations of program states, recent work shows that a combination of an explicit-value and an abstract domain can be beneficial for cegar approaches. This paper introduces the counterexample-guided prefix refinement analysis (cegpra) that is based on the cegar idea and features a purely path-based model refinement. A first evaluation based on benchmarks from the rigorous examination of reactive systems (RERS) challenge indicates that cegpra is useful for analyzing a subset of temporal properties on large-scale reactive systems.

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

Access this chapter

Log in via an institution
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

Notes

  1. 1.

    http://www.rers-challenge.org/.

  2. 2.

    http://www.rers-challenge.org/2014Isola/problems/WhiteBox/Problem3/Problem3.c.

  3. 3.

    http://www.rers-challenge.org/2014Isola/problems/constraints-RERS14-5.txt.

  4. 4.

    The syntax of the auto-generated LTL property 84 has been altered for this example without changing the semantics.

  5. 5.

    http://www.rers-challenge.org/2014Isola/problems/constraints-RERS14-5.txt.

References

  1. Baier, C., Katoen, J.P., et al.: Principles of Model Checking, vol. 26202649. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  2. Bauer, O., Geske, M., Isberner, M.: Analyzing program behavior through active automata learning. Int. J. Softw. Tools Technol. Transfer 16(5), 531–542 (2014)

    Article  Google Scholar 

  3. Beyer, D., Henzinger, T.A., Théoduloz, G.: Program analysis with dynamic precision adjustment. In: 23rd IEEE/ACM International Conference on Automated Software Engineering, ASE 2008, pp. 29–38. IEEE (2008)

    Google Scholar 

  4. Beyer, D., Löwe, S.: Explicit-state software model checking based on CEGAR and interpolation. In: Cortellessa, V., Varró, D. (eds.) FASE 2013. LNCS, vol. 7793, pp. 146–162. Springer, Heidelberg (2013). doi:10.1007/978-3-642-37057-1_11

    Chapter  Google Scholar 

  5. Beyer, D., Stahlbauer, A.: BDD-based software verification. Applications to event-condition-action systems. Int. J. Softw. Tools Technol. Transfer 16(5), 507–518 (2014)

    Article  Google Scholar 

  6. Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  7. Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods Syst. Des. 19(1), 7–34 (2001)

    Article  MATH  Google Scholar 

  8. Dams, D., Grumberg, O., Gerth, R.: Generation of reduced models for checking fragments of CTL. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 479–490. Springer, Heidelberg (1993). doi:10.1007/3-540-56922-7_39

    Chapter  Google Scholar 

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

    Article  Google Scholar 

  10. Jasper, M.: Counterexample-guided abstraction refinement for the verification of large-scale reactive systems. Bachelor thesis, TU Dortmund University (2015)

    Google Scholar 

  11. Morse, J., Cordeiro, L., Nicole, D., Fischer, B.: Applying symbolic bounded model checking to the 2012 RERS greybox challenge. Int. J. Softw. Tools Technol. Transfer 16(5), 519–529 (2014)

    Article  Google Scholar 

  12. van de Pol, J., Ruys, T.C., te Brinke, S.: Thoughtful brute-force attack of the RERS 2012 and 2013 challenges. Int. J. Softw. Tools Technol. Transfer 16(5), 481–491 (2014)

    Article  Google Scholar 

  13. Schordan, M., Prantl, A.: Combining static analysis and state transition graphs for verification of event-condition-action systems in the RERS 2012 and 2013 challenges. Int. J. Softw. Tools Technol. Transfer 16(5), 493–505 (2014)

    Article  Google Scholar 

  14. Steffen, B.: Data flow analysis as model checking. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol. 526, pp. 346–364. Springer, Heidelberg (1991). doi:10.1007/3-540-54415-1_54

    Chapter  Google Scholar 

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

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. TU Dortmund University, 44221, Dortmund, Germany

    Marc Jasper

Authors
  1. Marc Jasper
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Marc Jasper .

Editor information

Editors and Affiliations

  1. Lero - Irish Software Research Center, University of Limerick, Limerick, Ireland

    Anna-Lena Lamprecht

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Jasper, M. (2016). Counterexample-Guided Prefix Refinement Analysis for Program Verification. In: Lamprecht, AL. (eds) Leveraging Applications of Formal Methods, Verification, and Validation . ISoLA 2016. Communications in Computer and Information Science, vol 683. Springer, Cham. https://doi.org/10.1007/978-3-319-51641-7_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-51641-7_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-51640-0

  • Online ISBN: 978-3-319-51641-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation