Advertisement

Reducing Extension Edges of Concurrent Programs for Reachability Analysis

  • Cong Tian
  • Jiaying Wang
  • Zhenhua Duan
  • Liang Zhao
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11346)

Abstract

Predicate abstraction technique makes boolean programs a simple and popular model for program verification, of which the state reachability problem is decidable. However, the existing approach to reachability analysis of a concurrent boolean program, by applying the backward search (BWS) algorithm to the thread transition diagram (TTD) of the program, is of high complexity. To accelerate this approach, a method that expands the TTD with a kind of expansion edges and summarizes each path in the expanded TTD into a set of Presburger formulas has been proposed, so that the reachability problem is reduced to the satisfiability of the summary formulas. In this paper, we present a method for reachability analysis of concurrent boolean programs which improves the existing work in two aspects. First, with refined constraints on edge expansion, only a small number of expansion edges are required to be added to the TTD, which reduces the space consumption. Second, with optimized algorithm of path summarization using counter abstraction, less local state counters are dealt with and less summary formulas are generated. We have implemented the method and evaluated it on a large set of benchmark concurrent boolean programs. Experimental results show its efficiency on summarization and verification.

Keywords

Concurrent programs Thread transition diagram Reachability Boolean programs Backward search 

References

  1. 1.
    Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.K.: General decidability theorems for infinite-state systems. In: Proceedings of the Eleventh IEEE Symposium on Logic in Computer Science, pp. 313–321 (1996)Google Scholar
  2. 2.
    Abdulla, P.A.: Well (and better) quasi-ordered transition systems. Bull. Symb. Log. 16(4), 457–515 (2010)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Ball, T., Rajamani, S.K.: Boolean programs: a model and process for software analysis. Microsoft Research Technical report 2000–14 (2000)Google Scholar
  4. 4.
    Ball, T., Rajamani, S.K.: Bebop: a symbolic model checker for Boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 113–130. Springer, Heidelberg (2000).  https://doi.org/10.1007/10722468_7CrossRefzbMATHGoogle Scholar
  5. 5.
    Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI-C programs using SAT. Form. Methods Syst. Des. (FMSD) 25, 105–127 (2004)CrossRefGoogle Scholar
  6. 6.
    Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: SATABS: SAT-based predicate abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 570–574. Springer, Heidelberg (2005).  https://doi.org/10.1007/978-3-540-31980-1_40CrossRefzbMATHGoogle Scholar
  7. 7.
    Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: The Workshop on Logic of Programs, pp. 52–71 (1981)Google Scholar
  8. 8.
    Cousot, P.: The role of abstract interpretation in formal methods. In: Proceedings of the 5th IEEE International Conference on Software Engineering and Formal Methods, pp. 135–137 (2007)Google Scholar
  9. 9.
    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).  https://doi.org/10.1007/978-3-642-22110-1_28CrossRefGoogle Scholar
  10. 10.
    Emerson, E.A.: From asymmetry to full symmetry: new techniques for symmetry reduction in model checking. In: Advanced Research Working Conference on Correct Hardware Design and Verification Methods, pp. 142–157 (1999)Google Scholar
  11. 11.
    Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997).  https://doi.org/10.1007/3-540-63166-6_10CrossRefGoogle Scholar
  12. 12.
    Hoare, C.A.R., He, J.: Unifying theories of programming. In: Participants Copies for Relational Methods in Logic, Algebra and Computer Science, International Seminar Relmics, Warsaw, Poland, Septermber, pp. 97–99 (1998)Google Scholar
  13. 13.
    Kaiser, A., Kroening, D., Wahl, T.: A widening approach to multithreaded program verification. ACM Trans. Program. Lang. Syst. 36(4), 1–29 (2014)CrossRefGoogle Scholar
  14. 14.
    Liu, P., Wahl, T.: Infinite-state backward exploration of Boolean broadcast programs. In: Formal Methods in Computer-Aided Design, pp. 155–162 (2014)Google Scholar
  15. 15.
    Liu, P., Wahl, T.: Concolic unbounded-thread reachability via loop summaries. In: International Conference on Formal Engineering Methods, pp. 346–362 (2016)CrossRefGoogle Scholar
  16. 16.
    de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78800-3_24CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Cong Tian
    • 1
  • Jiaying Wang
    • 1
  • Zhenhua Duan
    • 1
  • Liang Zhao
    • 1
  1. 1.ICTT and ISN LabXidian UniversityXi’anPeople’s Republic of China

Personalised recommendations