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.
This research is supported by the NSFC Grant No. 61751207, 61732013 and 61420106004.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
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)
Abdulla, P.A.: Well (and better) quasi-ordered transition systems. Bull. Symb. Log. 16(4), 457–515 (2010)
Ball, T., Rajamani, S.K.: Boolean programs: a model and process for software analysis. Microsoft Research Technical report 2000–14 (2000)
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_7
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)
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_40
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)
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)
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_28
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)
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_10
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)
Kaiser, A., Kroening, D., Wahl, T.: A widening approach to multithreaded program verification. ACM Trans. Program. Lang. Syst. 36(4), 1–29 (2014)
Liu, P., Wahl, T.: Infinite-state backward exploration of Boolean broadcast programs. In: Formal Methods in Computer-Aided Design, pp. 155–162 (2014)
Liu, P., Wahl, T.: Concolic unbounded-thread reachability via loop summaries. In: International Conference on Formal Engineering Methods, pp. 346–362 (2016)
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_24
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Tian, C., Wang, J., Duan, Z., Zhao, L. (2018). Reducing Extension Edges of Concurrent Programs for Reachability Analysis. In: Kim, D., Uma, R., Zelikovsky, A. (eds) Combinatorial Optimization and Applications. COCOA 2018. Lecture Notes in Computer Science(), vol 11346. Springer, Cham. https://doi.org/10.1007/978-3-030-04651-4_26
Download citation
DOI: https://doi.org/10.1007/978-3-030-04651-4_26
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-04650-7
Online ISBN: 978-3-030-04651-4
eBook Packages: Computer ScienceComputer Science (R0)