Verification of Concurrent Programs Using Trace Abstraction Refinement | SpringerLink
Skip to main content
Springer Nature Link
Log in

Verification of Concurrent Programs Using Trace Abstraction Refinement

  • Conference paper
  • First Online:
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2015)

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

Included in the following conference series:

Abstract

Verifying concurrent programs is notoriously hard due to the state explosion problem: (1) the data state space can be very large as the variables can range over very large sets, and (2) the control state space is the Cartesian product of the control state space of the concurrent components and thus grows exponentially in the number of components. On the one hand, the most successful approaches to address the control state explosion problem are based on assume-guarantee reasoning or model-checking coupled with partial order reduction. On the other hand, the most successful techniques to address the data space explosion problem for sequential programs verification are based on the abstraction/refinement paradigm which consists in refining an abstract over-approximation of a program via predicate refinement. In this paper, we show that we can combine partial order reduction techniques with trace abstraction refinement. We apply our approach to standard benchmarks and show that it matches current state-of-the-art analysis techniques.

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
¥17,985 /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
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • 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.

    Without loss of generality we focus on reachability of control locations as reachability of a specific data state can easily be encoded in this setting.

  2. 2.

    We define it here for local states of \(P_2\) but the property holds for each component of a multi-threaded program.

  3. 3.

    In our experiments, Impara  0.2 failed to yield the correct analysis result.

References

  1. Beyer, D.: International software verification competition. http://sv-comp.sosy-lab.org/2015/

  2. 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  Google Scholar 

  3. Ball, T., Levin, V., Rajamani, S.K.: A decade of software model checking with SLAM. Commun. ACM 54(7), 68–76 (2011)

    Article  Google Scholar 

  4. Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596–619 (1983)

    Article  MATH  Google Scholar 

  5. Godefroid, P. (ed.): Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. LNCS, vol. 1032. Springer, Heidelberg (1996)

    MATH  Google Scholar 

  6. Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  7. Valmari, A.: Stubborn sets for reduced state space generation. Applications and Theory of Petri Nets. LNCS, vol. 483, pp. 491–515. Springer, Heidelberg (1989)

    Google Scholar 

  8. Holzmann, G.J.: Software model checking with spin. Adv. Comput. 65, 78–109 (2005)

    Google Scholar 

  9. Flanagan, C., Qadeer, S., Seshia, S.A.: A modular checker for multithreaded programs. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 180–194. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  10. Henzinger, T.A., Jhala, R., Majumdar, R., Qadeer, S.: Thread-modular abstraction refinement. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 262–274. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  11. Gupta, A., Popeea, C., Rybalchenko, A.: Predicate abstraction and refinement for verifying multi-threaded programs. In: POPL, pp. 331–344. ACM (2011)

    Google Scholar 

  12. Wachter, B., Kroening, D., Ouaknine, J.: Verifying multi-threaded software with impact. In: FMCAD, pp. 210–217. IEEE (2013)

    Google Scholar 

  13. Heizmann, M., Hoenicke, J., Podelski, A.: Refinement of trace abstraction. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 69–85. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  14. Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 36–52. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  15. Farzan, A., Kincaid, Z., Podelski, A.: Inductive data flow graphs. In: POPL, pp. 129–142. ACM (2013)

    Google Scholar 

  16. Tomasco, E., Inverso, O., Fischer, B., La Torre, S., Parlato, G.: MU-CSeq 0.3: Sequentialization by read-implicit and coarse-grained memory unwindings. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 436–438. Springer, Heidelberg (2015)

    Google Scholar 

  17. Inverso, O. et al.: Lazy-CSeq 0.6c: An improved lazy sequentialization tool for C. In: SV-COMP, (TACAS) 2015

    Google Scholar 

  18. Ziegler, F.: Verification of concurrent programs via partial-order reduction and trace refinement. MSc, Institut für Software & Systems Engineering, University of Ausgburg, Germany (2014)

    Google Scholar 

  19. Abdulla, P.A., Aronis, S., Jonsson, B., Sagonas, K.F.: Optimal dynamic partial order reduction. In: POPL, pp. 373–384. ACM (2014)

    Google Scholar 

  20. Kahlon, V., Wang, C., Gupta, A.: Monotonic partial order reduction: an optimal symbolic partial order reduction technique. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 398–413. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  21. Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: An interpolating SMT solver. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 248–254. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  22. Flanagan, C., Qadeer, S.: Thread-modular model checking. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 213–224. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  23. Henzinger, T.A., Jhala, R., Majumdar, R.: Race checking by context inference. In: PLDI 2004, pp. 1–13. ACM (2004)

    Google Scholar 

  24. Malkis, A., Podelski, A., Rybalchenko, A.: Thread-modular counterexample-guided abstraction refinement. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 356–372. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  25. Gupta, A., Popeea, C., Rybalchenko, A.: Threader: A constraint-based verifier for multi-threaded programs. [34] 412–417

    Google Scholar 

  26. Miné, A.: Static analysis by abstract interpretation of concurrent programs. Habilitation à Diriger les Recherches, ENS, France (2013)

    Google Scholar 

  27. Godefroid, P.: Software model checking: The verisoft approach. Form. Methods Syst. Des. 26(2), 77–101 (2005)

    Article  Google Scholar 

  28. Cimatti, A., Narasamdya, I., Roveri, M.: Boosting lazy abstraction for system C with partial order reduction. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 341–356. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  29. Donaldson, A.F., Kaiser, A., Kroening, D., Wahl, T.: Symmetry-aware predicate abstraction for shared-variable concurrent programs. [34] 356–371

    Google Scholar 

  30. Donaldson, A.F., Kaiser, A., Kroening, D., Tautschnig, M., Wahl, T.: Counterexample-guided abstraction refinement for symmetric concurrent programs. Form. Methods Syst. Des. 41(1), 25–44 (2012)

    Article  MATH  Google Scholar 

  31. Zielonka, W.: Notes on finite asynchronous automata. ITA 21(2), 99–135 (1987)

    MATH  MathSciNet  Google Scholar 

  32. Cassez, F., Müller, C., Burnett, K.: Summary-based inter-procedural analysis via modular trace refinement. In: FSTTCS 2014, pp. 545–556 (2014)

    Google Scholar 

  33. Cassez, F., Matsuoka, T., Pierzchalski, E., Smyth, N.: Perentie: modular trace refinement and selective value tracking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 439–442. Springer, Heidelberg (2015)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Macquarie University, NICTA/UNSW, Sydney, Australia

    Franck Cassez

  2. Augsburg University, Augsburg, Germany

    Frowin Ziegler

Authors
  1. Franck Cassez
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Frowin Ziegler
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Franck Cassez .

Editor information

Editors and Affiliations

  1. New York University, New York, New York, USA

    Martin Davis

  2. University of the South Pacific, Suva, Fiji

    Ansgar Fehnker

  3. Macquarie University, Sydney, New South Wales, Australia

    Annabelle McIver

  4. The University of Manchester, Manchester, United Kingdom

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Cassez, F., Ziegler, F. (2015). Verification of Concurrent Programs Using Trace Abstraction Refinement. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2015. Lecture Notes in Computer Science(), vol 9450. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-48899-7_17

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-48899-7_17

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-48898-0

  • Online ISBN: 978-3-662-48899-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics