Abstract
Boolean programs are a popular abstract domain for static-analysis-based software model checking. Yet little is known about the complexity of model checking for this model of computation. This paper aims to fill this void by providing a comprehensive study of the worst-case complexity of several basic analyses of Boolean programs, including reachability analysis, cycle detection, LTL, CTL, and CTL* model checking. We present algorithms for these problems and show that our algorithms are all optimal by providing matching lower bounds. We also identify particular classes of Boolean programs which are easier to analyse, and compare our results to prior work on pushdown model checking.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alur, R., Benedikt, M., Etessami, K., Godefroid, P., Reps, T., Yannakakis, M.: Analysis of Recursive State Machines. ACM Trans. on Programming Languages and Systems (TOPLAS) 27(4), 786–818 (2005)
Alur, R., Kannan, S., Yannakakis, M.: Communicating Hierarchical State Machines. In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644, pp. 169–178. Springer, Heidelberg (1999)
Alur, R., Yannakakis, M.: Model Checking of Hierarchical State Machines. ACM TOPLAS 23(3), 273–303 (2001)
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)
Ball, T., Rajamani, S.K.: The SLAM Toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 260–264. Springer, Heidelberg (2001)
Barnett, M., Leino, K.R.M.: Weakest Precondition of Unstructured Programs. In: Proc. PASTE (Program Analysis For Software Tools and Engineering), pp. 82–87 (2005)
Basler, G., Kroening, D., Weissenbacher, G.: SAT-Based Summarization for Boolean Programs. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 131–148. Springer, Heidelberg (2007)
Bouajjani, A., Esparza, J., Maler, O.: Reachability Analysis of Pushdown Automata: Application to Model-Checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997)
Burkart, O., Steffen, B.: Model Checking for Context-Free Processes. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 123–137. Springer, Heidelberg (1992)
Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. Journal of the ACM 28(1), 114–133 (1981)
Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded Model Checking Using Satisfiability Solving. Formal Methods in System Design 19(1), 7–34 (2001)
Clarke, E.M., Emerson, E.A.: Design and Synthesis of Synchronization Skeletons using Branching-Time Temporal Logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (1999)
Clarke, E.M., Kroening, D., Yorav, K.: Behavioral Consistency of C and Verilog Programs using Bounded Model Checking. In: Design Automation Conference (DAC), pp. 368–371. ACM (2003)
Cook, B., Podelski, A., Rybalchenko, A.: Termination Proofs for Systems Code. In: Proceedings of PLDI 2006, pp. 415–426 (2006)
Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Comm. of the ACM 18, 453–457 (1975)
Esparza, J., Schwoon, S.: A BDD-Based Model Checker for Recursive Programs. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 324–336. Springer, Heidelberg (2001)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended Static Checking for Java. In: Proceedings of PLDI 2002, pp. 234–245 (2002)
Godefroid, P., Nori, A., Rajamani, S., Tetali, S.: Compositional May-Must Program Analysis: Unleashing the Power of Alternation. In: Proc. POPL, pp. 43–55 (2010)
Goller, S., Lohrey, M.: Fixpoint Logics over Hierarchical Structures. Theory Comp. Sys. 48(1), 93–131 (2011)
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)
Gurfinkel, A., Wei, O., Chechik, M.: Yasm: A Software Model-Checker for Verification and Refutation. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 170–174. Springer, Heidelberg (2006)
Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy Abstraction. In: Proceedings of POPL 2002, Portland, pp. 58–70 (January 2002)
Kupferman, O., Vardi, M.Y., Wolper, P.: An Automata-Theoretic Approach to Branching-Time Model Checking. Journal of the ACM 47(2), 312–360 (2000)
Leino, K.R.M.: A SAT Characterization of Boolean-Program Correctness. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 104–120. Springer, Heidelberg (2003)
Lohrey, M.: Model-checking hierarchical structures. J. Comp. Sys. Sc. 78(2), 461–490 (2012)
Papadimitriou, C.H., Yannakakis, M.: A Note on Succinct Representation of Graphs. Inf. and Comp. 71(3), 181–185 (1986)
Walukiewicz, I.: Model Checking CTL Properties of Pushdown Systems. In: Kapoor, S., Prasad, S. (eds.) FST TCS 2000. LNCS, vol. 1974, pp. 127–138. Springer, Heidelberg (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Godefroid, P., Yannakakis, M. (2013). Analysis of Boolean Programs. In: Piterman, N., Smolka, S.A. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2013. Lecture Notes in Computer Science, vol 7795. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-36742-7_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-36742-7_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-36741-0
Online ISBN: 978-3-642-36742-7
eBook Packages: Computer ScienceComputer Science (R0)