×

Verification of Boolean programs with unbounded thread creation. (English) Zbl 1143.68043

Summary: Most symbolic software model checkers use abstraction techniques to reduce the verification of infinite-state programs to that of decidable classes. Boolean programs [T. Ball and S. K. Rajamani, Lect. Notes Comput. Sci. 1885, 113–130 (2000; Zbl 0976.68540)] are the most popular representation for these abstractions. Unfortunately, today’s symbolic software model checkers are limited to the analysis of sequential programs due to the fact that reachability in Boolean programs with unbounded thread creation is undecidable. We address this limitation with a novel algorithm for over-approximating reachability in Boolean programs with unbounded thread creation. Although the Boolean programs are not of finite state, the algorithm always reaches a fix-point. The fixed points are detected by projecting the state of the threads to the globally visible parts, which are finite.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q55 Semantics in the theory of computing

Citations:

Zbl 0976.68540
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Ball, T.; Rajamani, S. K., Bebop: A symbolic model checker for Boolean programs, (SPIN 00. SPIN 00, Lecture Notes in Computer Science, vol. 1885 (2000), Springer), 113-130 · Zbl 0976.68540
[2] Cook, B.; Kroening, D.; Sharygina, N., Symbolic model checking for asynchronous Boolean programs, (SPIN. SPIN, Lecture Notes in Computer Science, vol. 3639 (2005), Springer), 75-90 · Zbl 1151.68367
[3] Cook, B.; Kroening, D.; Sharygina, N., Over-approximating Boolean programs with unbounded thread creation, (Proceedings of FMCAD (2006), IEEE), 53-59
[4] Graf, S.; Saïdi, H., Construction of abstract state graphs with PVS, (Computer-Aided Verification (CAV). Computer-Aided Verification (CAV), Lecture Notes in Computer Science, vol. 1254 (1997), Springer), 72-83
[5] Podelski, A.; Wies, T., Boolean heaps, (Static Analysis (SAS). Static Analysis (SAS), Lecture Notes in Computer Science, vol. 3672 (2005), Springer), 268-283 · Zbl 1141.68374
[6] Yorsh, G.; Reps, T. W.; Sagiv, M.; Wilhelm, R., Logical characterizations of heap abstractions, ACM Transactions on Computational Logic, 8, 1 (2007) · Zbl 1367.68078
[7] Clarke, E. M.; Grumberg, O.; Jha, S.; Lu, Y.; Veith, H., Counterexample-guided abstraction refinement for symbolic model checking, Journal of the ACM, 50, 5, 752-794 (2003) · Zbl 1325.68145
[8] Rinard, M. C., Analysis of multithreaded programs, (Static Analysis (SAS). Static Analysis (SAS), Lecture Notes in Computer Science, vol. 2126 (2001), Springer), 1-19 · Zbl 1005.68896
[9] Ramalingam, G., Context-sensitive synchronization-sensitive analysis is undecidable, ACM Transactions on Programming Languages and Systems, 22, 2, 416-430 (2000)
[10] Burkart, O.; Steffen, B., Composition, decomposition and model checking of pushdown processes, Nordic Journal of Computing, 2, 89-125 (1995) · Zbl 0839.68028
[11] Esparza, J.; Schwoon, S., A BDD-based model checker for recursive programs, (Computer-Aided Verification (CAV). Computer-Aided Verification (CAV), Lecture Notes in Computer Science, vol. 2102 (2001), Springer), 324-336 · Zbl 0991.68539
[12] Leino, K. R.M., A SAT characterization of Boolean-program correctness, (Model Checking Software (SPIN). Model Checking Software (SPIN), Lecture Notes in Computer Science, vol. 2648 (2003), Springer), 104-120 · Zbl 1023.68534
[13] Jain, H.; Clarke, E.; Kroening, D., Verification of SpecC and Verilog using predicate abstraction, (Proceedings of MEMOCODE 2004 (2004), IEEE), 7-16
[14] Cimatti, A., NuSMV 2: An opensource tool for symbolic model checking, (Computer Aided Verification (CAV). Computer Aided Verification (CAV), Lecture Notes in Computer Science (2002), Springer), 359-364 · Zbl 1010.68766
[15] Chaki, S.; Clarke, E. M.; Kidd, N.; Reps, T. W.; Touili, T., Verifying concurrent message-passing C programs with recursive calls, (Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science, vol. 3920 (2006), Springer), 334-349 · Zbl 1180.68109
[16] Qadeer, S.; Rehof, J., Context-bounded model checking of concurrent software, (Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science, vol. 3440 (2005), Springer), 93-107 · Zbl 1087.68598
[17] Clarke, E.; Talupur, M.; Touili, T.; Veith, H., Verification by network decomposition, (CONCUR 04. CONCUR 04, Lecture Notes in Computer Science, vol. 3170 (2004), Springer), 276-291 · Zbl 1099.68653
[18] Ip, C.; Dill, D., Verifying systems with replicated components in mur \(\phi \), (Computer-Aided Verification (CAV). Computer-Aided Verification (CAV), Lecture Notes in Computer Science, vol. 1102 (1996), Springer), 147-158
[19] Pnueli, A.; Arons, T., TLPVS: A PVS-based LTL verification system, (Verification—Theory and Practice: Proceedings of an International Symposium in Honor of Zohar Manna’s 64th Birthday. Verification—Theory and Practice: Proceedings of an International Symposium in Honor of Zohar Manna’s 64th Birthday, Lecture Notes in Computer Science (2003), Springer), 84-98 · Zbl 1274.68202
[20] Henzinger, T. A.; Jhala, R.; Majumdar, R., Race checking by context inference, (PLDI (2004), ACM), 1-13
[21] Flanagan, C.; Qadeer, S., Thread-modular model checking, (SPIN. SPIN, Lecture Notes in Computer Science, vol. 2648 (2003), Springer), 213-224 · Zbl 1023.68529
[22] Bouajjani, A.; Esparza, J.; Touili, T., Reachability analysis of synchronized PA systems, Electronic Notes in Theoretical Computer Science, 138, 3, 153-178 (2005) · Zbl 1272.68290
[23] Stoller, S. D., Model-checking multi-threaded distributed Java programs, (SPIN Model Checking and Software Verification. SPIN Model Checking and Software Verification, Lecture Notes in Computer Science, vol. 1885 (2000), Springer), 224-244 · Zbl 0976.68556
[24] Havelund, K.; Pressburger, T., Model checking Java programs using Java PathFinder, International Journal on Software Tools for Technology Transfer, 2, 4, 366-381 (2000) · Zbl 1059.68585
[25] Yahav, E., Verifying safety properties of concurrent Java programs using 3-valued logic, (POPL (2001), ACM Press), 27-40 · Zbl 1323.68183
[26] Andrews, T.; Qadeer, S.; Rajamani, S. K.; Rehof, J.; Xie, Y., Zing: Exploiting program structure for model checking concurrent software, (CONCUR 04. CONCUR 04, Lecture Notes in Computer Science, vol. 3170 (2004), Springer), 1-15 · Zbl 1099.68583
[27] Ball, T.; Chaki, S.; Rajamani, S. K., Parameterized verification of multithreaded software libraries, (Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science, vol. 2031 (2001), Springer), 158-173 · Zbl 0978.68679
[28] Kahlon, V.; Gupta, A., On the analysis of interacting pushdown systems, (Principles of Programming Languages (POPL) (2007), ACM), 303-314 · Zbl 1295.68159
[29] Clarke, E. M.; Grumberg, O.; Long, D. E., Model checking and abstraction, (Principles of Programming Languages (POPL) (1992), ACM), 343-354
[30] Colón, M. A.; Uribe, T. E., Generating finite-state abstractions of reactive systems using decision procedures, (Computer-Aided Verification (CAV). Computer-Aided Verification (CAV), Lecture Notes in Computer Science, vol. 1427 (1998), Springer), 293-304
[31] T. Ball, S. Rajamani, Boolean programs: A model and process for software analysis, Tech. Rep. 2000-14, Microsoft Research, February 2000; T. Ball, S. Rajamani, Boolean programs: A model and process for software analysis, Tech. Rep. 2000-14, Microsoft Research, February 2000 · Zbl 0976.68540
[32] Kurshan, R., Computer-Aided Verification of Coordinating Processes (1995), Princeton University Press · Zbl 0822.68116
[33] Clarke, E.; Grumberg, O.; Jha, S.; Lu, Y.; Veith, H., Counterexample-guided abstraction refinement, (Computer-Aided Verification (CAV). Computer-Aided Verification (CAV), Lecture Notes in Computer Science (2000), Springer), 154-169 · Zbl 0974.68517
[34] Holzmann, G.; Peled, D., The State of SPIN, (Computer-Aided Verification (CAV). Computer-Aided Verification (CAV), Lecture Notes in Computer Science, vol. 1102 (1996), Springer), 385-389
[35] Jain, P.; Gopalakrishnan, G., Efficient symbolic simulation-based verification using the parametric form of Boolean expressions, IEEE Transactions on CAD of ICs and Systems, 13, 8, 1005-1015 (1994)
[36] Coudert, O.; Madre, J., A unified framework for the formal verification of sequential circuits, (ICCAD (1990), IEEE), 78-82
[37] Aagaard, M. D.; Jones, R. B.; Seger, C.-J. H., Formal verification using parametric representations of boolean constraints, (DAC (1999), ACM Press), 402-407
[38] Clarke, E.; Kroening, D.; Sharygina, N.; Yorav, K., Predicate abstraction of ANSI-C programs using SAT, Formal Methods in System Design, 25, 105-127 (2004) · Zbl 1090.68022
[39] Clarke, E.; Kroening, D.; Sharygina, N.; Yorav, K., SATABS: SAT-based predicate abstraction for ANSI-C, (Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science, vol. 3440 (2005), Springer), 570-574 · Zbl 1087.68586
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.