Movatterモバイル変換

[0]ホーム
URL:

Skip to main content

Advertisement

Springer Nature Link
Log in

Concolic Unbounded-Thread Reachability via Loop Summaries

  • Conference paper
  • First Online:

Part of the book series:Lecture Notes in Computer Science ((LNPSE,volume 10009))

Included in the following conference series:

Abstract

We present a method for accelerating explicit-state backward search algorithms for systems of arbitrarily many finite-state threads. Our method statically analyzes the program executed by the threads for the existence of simple loops. We show how such loops can be collapsedwithout approximation into Presburger arithmetic constraints that symbolically summarize the effect of executing the backward search algorithm along the loop in the multi-threaded program. As a result, the subsequent explicit-state search does not need to explore the summarized part of the state space. The combination of concrete and symbolic exploration gives our algorithm aconcolic flavor. We demonstrate the power of this method for proving and refuting safety properties of unbounded-thread programs.

This work is supported by US National Science Foundation grant no. 1253331.

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

Access this chapter

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

Similar content being viewed by others

Notes

  1. 1.

    Dynamic thread creation is discussed at end of Sect. 6.

  2. 2.

    Simple SCC nodes (representing a simple loop) are not to be confused withtrivial SCC nodes (representing a single node). Simple nodes are by definition non-trivial.

  3. 3.

    We exploit the fact that cover preimages in systems induced by TTDs increase the number of threads in a state by at most 1 (see [20, Lemma 1] for a proof).

  4. 4.

    Loop-free paths (\(m=0\)) can be processed either using Algorithm 1, or via summaries.

  5. 5.

    Cutr “=”ConcolicUnbounded-ThreadReachability analysis.

  6. 6.

References

  1. Abdulla, P.A.: Well (and better) quasi-ordered transition systems. Bull. Symb. Log.16(4), 457–515 (2010)

    Article MathSciNet MATH  Google Scholar 

  2. Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.K.: General decidability theorems for infinite-state systems. In: LICS, pp. 313–321 (1996)

    Google Scholar 

  3. Athanasiou, K., Liu, P., Wahl, T.: Unbounded-thread program verification using thread-state equations. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS, vol. 9706, pp. 516–531. Springer, Heidelberg (2016)

    Google Scholar 

  4. Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: PLDI, pp. 203–213 (2001)

    Google Scholar 

  5. Bardin, S., Finkel, A., Leroux, J., Schnoebelen, P.: Flat acceleration in symbolic model checking. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 474–488. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  6. Cardoza, E., Lipton, R.J., Meyer, A.R.: Exponential space complete problems for Petri nets and commutative semigroups: preliminary report. In: STOC, pp. 50–54 (1976)

    Google Scholar 

  7. Donaldson, A., Kaiser, A., Kroening, D., Wahl, T.: Symmetry-aware predicate abstraction for shared-variable concurrent programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 356–371. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  8. Esparza, J., Ledesma-Garza, R., Majumdar, R., Meyer, P., Niksic, F.: An SMT-based approach to coverability analysis. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 603–619. Springer, Heidelberg (2014)

    Google Scholar 

  9. Finkel, A., Leroux, J.: How to compose presburger-accelerations: applications to broadcast protocols. In: Agrawal, M., Seth, A.K. (eds.) FSTTCS 2002. LNCS, vol. 2556, pp. 145–156. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  10. Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere!. Theor. Comput. Sci.256(1–2), 63–92 (2001)

    Article MathSciNet MATH  Google Scholar 

  11. Geeraerts, G., Raskin, J.F., Begin, L.V.: Expand, enlarge and check: new algorithms for the coverability problem of WSTS. J. Comput. Syst. Sci.72(1), 180–203 (2006)

    Article MathSciNet MATH  Google Scholar 

  12. Geeraerts, G., Raskin, J.-F., Van Begin, L.: On the efficient computation of the minimal coverability set for Petri nets. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 98–113. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  13. German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM39(3), 675–735 (1992)

    Article MathSciNet MATH  Google Scholar 

  14. Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: CAV, pp. 72–83 (1997)

    Google Scholar 

  15. Jonsson, B., Saksena, M.: Systematic acceleration in regular model checking. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 131–144. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  16. Kaiser, A., Kroening, D., Wahl, T.: A widening approach to multithreaded program verification. ACM Trans. Program. Lang. Syst.36(4), 14 (2014)

    Article  Google Scholar 

  17. Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. Syst. Sci.3(2), 147–195 (1969)

    Article MathSciNet MATH  Google Scholar 

  18. Leroux, J.: The general vector addition system reachability problem by Presburger inductive invariants. In: LICS, pp. 4–13 (2009)

    Google Scholar 

  19. Leroux, J.: Presburger vector addition systems. In: LICS, pp. 23–32 (2013)

    Google Scholar 

  20. Liu, P., Wahl, T.: Infinite-state backward exploration of Boolean broadcast programs. In: FMCAD, pp. 155–162 (2014)

    Google Scholar 

  21. Liu, P., Wahl, T.: Concolic unbounded-thread reachability via loop summaries (extended technical report). CoRR abs/1607.08273 (2016).http://arxiv.org/abs/1505.02637

    Google Scholar 

  22. de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  23. Reynier, P.A., Servais, F.: Minimal coverability set for Petri nets: Karp and Miller algorithm with pruning. In: Petri Nets, pp. 69–88 (2011)

    Google Scholar 

  24. Valmari, A., Hansen, H.: Old and new algorithms for minimal coverability sets. In: Haddad, S., Pomello, L. (eds.) PETRI NETS 2012. LNCS, vol. 7347, pp. 208–227. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Northeastern University, Boston, USA

    Peizun Liu & Thomas Wahl

Authors
  1. Peizun Liu

    You can also search for this author inPubMed Google Scholar

  2. Thomas Wahl

    You can also search for this author inPubMed Google Scholar

Corresponding author

Correspondence toPeizun Liu.

Editor information

Editors and Affiliations

  1. School of Information Science, Japan Advanced Institute of Science and Technology (JAIST), Nomi, Japan

    Kazuhiro Ogata

  2. Department of Computing and Software, McMaster University, Hamilton, Ontario, Canada

    Mark Lawford

  3. Department of Computer Science, Hosei University, Tokyo, Japan

    Shaoying Liu

Rights and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Liu, P., Wahl, T. (2016). Concolic Unbounded-Thread Reachability via Loop Summaries. In: Ogata, K., Lawford, M., Liu, S. (eds) Formal Methods and Software Engineering. ICFEM 2016. Lecture Notes in Computer Science(), vol 10009. Springer, Cham. https://doi.org/10.1007/978-3-319-47846-3_22

Download citation

Publish with us

Access this chapter

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

[8]ページ先頭
©2009-2025 Movatter.jp