{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T12:44:03Z","timestamp":1740141843431,"version":"3.37.3"},"reference-count":51,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2024,3,20]],"date-time":"2024-03-20T00:00:00Z","timestamp":1710892800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,3,20]],"date-time":"2024-03-20T00:00:00Z","timestamp":1710892800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["Cluster of Excellence EXC 2050\/1 (project ID 39069Collaborative Research Center TRR 248 (project ID"],"award-info":[{"award-number":["Cluster of Excellence EXC 2050\/1 (project ID 39069Collaborative Research Center TRR 248 (project ID"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002957","name":"Technische Universit\u00e4t Dresden","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100002957","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2024,4]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p><jats:italic>Recursive state machines (RSMs)<\/jats:italic>are state-based models for procedural programs with wide-ranging applications in program verification and interprocedural analysis. Model-checking algorithms for RSMs and related formalisms have been intensively studied in the literature. In this article, we devise a new model-checking algorithm for RSMs and requirements in<jats:italic>computation tree logic (CTL)<\/jats:italic>that exploits the compositional structure of RSMs by ternary model checking in combination with a lazy evaluation scheme. Specifically, a procedural component is only analyzed in those cases in which it might influence the satisfaction of the CTL requirement. We implemented our model-checking algorithms and evaluate them on randomized scalability benchmarks and on an interprocedural data-flow analysis of<jats:sc>Java<\/jats:sc>programs, showing both practical applicability and significant speedups in comparison to state-of-the-art model-checking tools for procedural programs.<\/jats:p>","DOI":"10.1007\/s10270-024-01159-z","type":"journal-article","created":{"date-parts":[[2024,3,20]],"date-time":"2024-03-20T12:01:37Z","timestamp":1710936097000},"page":"369-401","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Lazy model checking for recursive state machines"],"prefix":"10.1007","volume":"23","author":[{"given":"Clemens","family":"Dubslaff","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Patrick","family":"Wienh\u00f6ft","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ansgar","family":"Fehnker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,3,20]]},"reference":[{"key":"1159_CR1","unstructured":"The Apache\u2122 FOP Project. https:\/\/xmlgraphics.apache.org\/fop\/. Accessed 31 Jan 2024 (2016)"},{"key":"1159_CR2","unstructured":"The AVR Simulation and Analysis Framework . https:\/\/github.com\/avrora-framework\/avrora. Accessed 31 Jan 2024 (2016)"},{"issue":"4","key":"1159_CR3","doi-asserted-by":"publisher","first-page":"786","DOI":"10.1145\/1075382.1075387","volume":"27","author":"R Alur","year":"2005","unstructured":"Alur, R., Benedikt, M., Etessami, K., Godefroid, P., Reps, T., Yannakakis, M.: Analysis of recursive state machines. ACM Trans. Program. Lang. Syst. 27(4), 786\u2013818 (2005)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"1159_CR4","first-page":"541","volume-title":"Model Checking Procedural Programs","author":"R Alur","year":"2018","unstructured":"Alur, R., Bouajjani, A., Esparza, J.: Model Checking Procedural Programs, pp. 541\u2013572. Springer, Cham (2018)"},{"issue":"3","key":"1159_CR5","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1145\/503502.503503","volume":"23","author":"R Alur","year":"2001","unstructured":"Alur, R., Yannakakis, M.: Model checking of hierarchical state machines. ACM Trans. Program. Lang. Syst. 23(3), 273\u2013303 (2001)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"1159_CR6","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"1159_CR7","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-319-66197-1_4","volume-title":"Software Engineering and Formal Methods","author":"A Bernasconi","year":"2017","unstructured":"Bernasconi, A., Menghi, C., Spoletini, P., Zuck, L.D., Ghezzi, C.: From model checking to a temporal proof for partial models. In: Cimatti, A., Sirjani, M. (eds.) Software Engineering and Formal Methods, pp. 54\u201369. Springer, Cham (2017)"},{"key":"1159_CR8","doi-asserted-by":"crossref","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability\u2014Second Edition, Volume 336 of Frontiers in Artificial Intelligence and Applications. IOS Press (2021)","DOI":"10.3233\/FAIA336"},{"key":"1159_CR9","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: Mazurkiewicz, A.W., Winkowski, J. (eds.) Proceedings of the CONCUR\u201997, Volume 1243 of LNCS, pp. 135\u2013150. Springer (1997)","DOI":"10.1007\/3-540-63141-0_10"},{"key":"1159_CR10","doi-asserted-by":"crossref","unstructured":"Brauer, J., Huuck, R., Schlich, B.: Interprocedural pointer analysis in goanna. Electron. Notes Theor. Comput. Sci. 254, 65\u201383 (2009). Proceedings of the 4th International Workshop on Systems Software Verification (SSV 2009)","DOI":"10.1016\/j.entcs.2009.09.060"},{"key":"1159_CR11","unstructured":"Br\u00e1zdil, T.: Verification of Probabilistic Recursive Sequential Programs. Ph.D. thesis, Masaryk University Brno (2007)"},{"key":"1159_CR12","doi-asserted-by":"crossref","unstructured":"Bruns, G., Godefroid, P.: Model checking partial state spaces with 3-valued temporal logics. In: Halbwachs, N., Peled, D.A. (eds.) Proceedings of the CAV\u201999, pp. 274\u2013287. Springer (1999)","DOI":"10.1007\/3-540-48683-6_25"},{"key":"1159_CR13","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/3-540-44618-4_14","volume-title":"CONCUR 2000\u2014Concurrency Theory","author":"G Bruns","year":"2000","unstructured":"Bruns, G., Godefroid, P.: Generalized model checking: reasoning about partial state spaces. In: Palamidessi, C. (ed.) CONCUR 2000\u2014Concurrency Theory, pp. 168\u2013182. Springer, Berlin (2000)"},{"key":"1159_CR14","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35, 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"1159_CR15","doi-asserted-by":"crossref","unstructured":"Burkart, O., Steffen, B.: Model checking for context-free processes. In Cleaveland, W. (ed.) Proceedings of the CONCUR\u201992, pp. 123\u2013137 (1992)","DOI":"10.1007\/BFb0084787"},{"issue":"1\u20132","key":"1159_CR16","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1016\/S0304-3975(99)00034-1","volume":"221","author":"O Burkart","year":"1999","unstructured":"Burkart, O., Steffen, B.: Model checking the full modal mu-calculus for infinite sequential processes. Theor. Comput. Sci. 221(1\u20132), 251\u2013270 (1999)","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"1159_CR17","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1145\/990010.990011","volume":"12","author":"M Chechik","year":"2003","unstructured":"Chechik, M., Devereux, B., Easterbrook, S., Gurfinkel, A.: Multi-valued symbolic model-checking. ACM Trans. Softw. Eng. Methodol. 12(4), 371\u2013408 (2003)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"1159_CR18","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logic of Programs, Volume 131 of LNCS, pp. 52\u201371 (1981)","DOI":"10.1007\/BFb0025774"},{"key":"1159_CR19","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: CAV \u201900: Proceedings of the 12th International Conference on Computer Aided Verification, pp. 154\u2013169. Springer, London (2000)","DOI":"10.1007\/10722167_15"},{"key":"1159_CR20","volume-title":"Model Checking","author":"EM Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (2000)"},{"key":"1159_CR21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8","volume-title":"Handbook of Model Checking. Incorporated","author":"EM Clarke","year":"2018","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R.: Handbook of Model Checking. Incorporated, 1st edn. Springer, New York (2018)","edition":"1"},{"key":"1159_CR22","volume-title":"Principles of Abstract Interpretation","author":"P Cousot","year":"2021","unstructured":"Cousot, P.: Principles of Abstract Interpretation. The MIT Press, Cambridge (2021)"},{"key":"1159_CR23","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Los Angeles, California, pp. 238\u2013252. ACM Press, New York (1977)","DOI":"10.1145\/512950.512973"},{"key":"1159_CR24","first-page":"385","volume-title":"Abstraction and Abstraction Refinement","author":"D Dams","year":"2018","unstructured":"Dams, D., Grumberg, O.: Abstraction and Abstraction Refinement, pp. 385\u2013419. Springer, Cham (2018)"},{"key":"1159_CR25","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-030-92124-8_19","volume-title":"Software Engineering and Formal Methods","author":"C Dubslaff","year":"2021","unstructured":"Dubslaff, C., Wienh\u00f6ft, P., Fehnker, A.: Be lazy and don\u2019t care: faster CTL model checking for recursive state machines. In: Calinescu, R., P\u0103s\u0103reanu, C.S. (eds.) Software Engineering and Formal Methods, pp. 332\u2013350. Springer, Cham (2021)"},{"key":"1159_CR26","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 21st International Conference on Software Engineering, ICSE \u201999, pp. 411\u2013420. Association for Computing Machinery, New York (1999)","DOI":"10.1145\/302405.302672"},{"issue":"1","key":"1159_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1462153.1462154","volume":"56","author":"K Etessami","year":"2009","unstructured":"Etessami, K., Yannakakis, M.: Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations. J. ACM 56(1), 1\u201366 (2009)","journal-title":"J. ACM"},{"key":"1159_CR28","unstructured":"Fehnker, A., Dubslaff, C.: Inter-procedural analysis of computer programs. US Patent 8,296,735 (2012)"},{"key":"1159_CR29","unstructured":"Gmytrasiewicz, P.J., Durfee, E.H.: A logic of knowledge and belief for recursive modeling: a preliminary report. In: Swartout, W.R. (ed.) Proceedings of the 10th National Conference on Artificial Intelligence, San Jose, CA, USA, July 12\u201316, 1992, pp. 628\u2013634. AAAI Press\/The MIT Press (1992)"},{"key":"1159_CR30","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/3-540-44685-0_29","volume-title":"CONCUR 2001\u2014Concurrency Theory","author":"P Godefroid","year":"2001","unstructured":"Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based model checking using modal transition systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001\u2014Concurrency Theory, pp. 426\u2013440. Springer, Berlin (2001)"},{"key":"1159_CR31","doi-asserted-by":"crossref","unstructured":"G\u00f6ller, S., Lohrey, M.: Branching-time model checking of one-counter processes and timed automata. SIAM J. Comput. 42(3), 884\u2013923 (2013)","DOI":"10.1137\/120876435"},{"key":"1159_CR32","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) Proceedings of the Computer Aided Verification, 9th International Conference, CAV \u201997, Haifa, Israel, June 22\u201325, 1997, Volume 1254 of Lecture Notes in Computer Science, pp. 72\u201383. Springer (1997)"},{"issue":"5","key":"1159_CR33","doi-asserted-by":"publisher","first-page":"799","DOI":"10.1016\/j.ic.2010.12.004","volume":"209","author":"M Hague","year":"2011","unstructured":"Hague, M., Ong, C.-H.: A saturation method for the modal $$\\mu $$-calculus over pushdown systems. Inf. Comput. 209(5), 799\u2013821 (2011)","journal-title":"Inf. Comput."},{"key":"1159_CR34","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201902, pp. 58\u201370, New York, NY, USA. Association for Computing Machinery (2002)","DOI":"10.1145\/503272.503279"},{"key":"1159_CR35","doi-asserted-by":"crossref","unstructured":"Horwitz, S., Reps, T., Sagiv, M.: Demand interprocedural dataflow analysis. In: Kaiser, G.E. (ed.) Proceedings of the SIGSOFT\u201995, pp. 104\u2013115. ACM (1995)","DOI":"10.1145\/222132.222146"},{"key":"1159_CR36","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/3-540-47813-2_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M Huth","year":"2002","unstructured":"Huth, M.: Model checking modal transition systems using Kripke structures. In: Cortesi, A. (ed.) Verification, Model Checking, and Abstract Interpretation, pp. 302\u2013316. Springer, Berlin (2002)"},{"key":"1159_CR37","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/3-540-45309-1_11","volume-title":"Programming Languages and Systems","author":"M Huth","year":"2001","unstructured":"Huth, M., Jagadeesan, R., Schmidt, D.: Modal transition systems: a foundation for three-valued program analysis. In: Sands, D. (ed.) Programming Languages and Systems, pp. 155\u2013169. Springer, Berlin (2001)"},{"key":"1159_CR38","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/978-3-642-15769-1_20","volume-title":"Static Analysis","author":"SH Jensen","year":"2010","unstructured":"Jensen, S.H., M\u00f8ller, A., Thiemann, P.: Interprocedural analysis with lazy propagation. In: Cousot, R., Martel, M. (eds.) Static Analysis, pp. 320\u2013339. Springer, Berlin (2010)"},{"key":"1159_CR39","unstructured":"Kozen, D.: Results on the propositional $$\\mu $$-calculus. Theor. Comput. Sci. 27(3), 333\u2013354 (1983). Special Issue Ninth International Colloquium on Automata, Languages and Programming (ICALP) Aarhus, Summer 1982"},{"key":"1159_CR40","first-page":"36","volume-title":"30 Years of Modal Transition Systems: Survey of Extensions and Analysis","author":"J K\u0159et\u00ednsk\u00fd","year":"2017","unstructured":"K\u0159et\u00ednsk\u00fd, J.: 30 Years of Modal Transition Systems: Survey of Extensions and Analysis, pp. 36\u201374. Springer, Cham (2017)"},{"key":"1159_CR41","doi-asserted-by":"crossref","unstructured":"Larsen, K., Thomsen, B.: A modal process logic. In: [1988] Proceedings. Third Annual Symposium on Logic in Computer Science, pp. 203\u2013210 (1988)","DOI":"10.1109\/LICS.1988.5119"},{"key":"1159_CR42","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) Computer Aided Verification, pp. 123\u2013136. Springer, Berlin (2006)"},{"issue":"6","key":"1159_CR43","doi-asserted-by":"publisher","first-page":"1039","DOI":"10.1007\/s00165-021-00564-1","volume":"33","author":"C Menghi","year":"2021","unstructured":"Menghi, C., Rizzi, A.M., Bernasconi, A., Spoletini, P.: Torpedo: witnessing model correctness with topological proofs. Form. Asp. Comput. 33(6), 1039\u20131066 (2021)","journal-title":"Form. Asp. Comput."},{"key":"1159_CR44","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1007\/978-3-319-48989-6_32","volume-title":"FM 2016: Formal Methods","author":"C Menghi","year":"2016","unstructured":"Menghi, C., Spoletini, P., Ghezzi, C.: Dealing with incompleteness in automata-based model checking. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016: Formal Methods, pp. 531\u2013550. Springer, Cham (2016)"},{"issue":"1\u20132","key":"1159_CR45","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1016\/j.scico.2005.02.009","volume":"58","author":"TW Reps","year":"2005","unstructured":"Reps, T.W., Schwoon, S., Jha, S., Melski, D.: Weighted pushdown systems and their application to interprocedural dataflow analysis. Sci. Comput. Program. 58(1\u20132), 206\u2013263 (2005)","journal-title":"Sci. Comput. Program."},{"key":"1159_CR46","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/3-540-49727-7_22","volume-title":"Static Analysis","author":"D Schmidt","year":"1998","unstructured":"Schmidt, D., Steffen, B.: Program analysis as model checking of abstract interpretations. In: Levi, G. (ed.) Static Analysis, pp. 351\u2013380. Springer, Berlin (1998)"},{"key":"1159_CR47","unstructured":"Schwoon, S.: Model checking pushdown systems. Ph.D. thesis, Technical University Munich, Germany (2002)"},{"key":"1159_CR48","unstructured":"Sharir, M., Pnueli, A.: Two Approaches to Interprocedural Data Flow analysis, Chapter 7, pp. 189\u2013234. Prentice-Hall, Englewood Cliffs (1981)"},{"key":"1159_CR49","doi-asserted-by":"crossref","unstructured":"Song, F., Touili, T.: PuMoC: a CTL model-checker for sequential programs. In: Goedicke, M., Menzies, T., Saeki, M. (eds.) Proceedings of the ASE\u201912, pp. 346\u2013349. ACM (2012)","DOI":"10.1145\/2351676.2351743"},{"issue":"4","key":"1159_CR50","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s00450-012-0233-1","volume":"28","author":"S Uchitel","year":"2013","unstructured":"Uchitel, S., Alrajeh, D., Ben-David, S., Braberman, V., Chechik, M., De Caso, G., D\u2019Ippolito, N., Fischbein, D., Garbervetsky, D., Kramer, J., Russo, A., Sibay, G.: Supporting incremental behaviour model elaboration. Comput. Sci. Res. Dev. 28(4), 279\u2013293 (2013)","journal-title":"Comput. Sci. Res. Dev."},{"key":"1159_CR51","unstructured":"Vizel, Y., Grumberg, O., Shoham, S.: Lazy abstraction and sat-based reachability in hardware model checking. In: 2012 Formal Methods in Computer-Aided Design (FMCAD), pp. 173\u2013181 (2012)"}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-024-01159-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-024-01159-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-024-01159-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,14]],"date-time":"2024-11-14T18:08:56Z","timestamp":1731607736000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-024-01159-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,3,20]]},"references-count":51,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,4]]}},"alternative-id":["1159"],"URL":"https:\/\/doi.org\/10.1007\/s10270-024-01159-z","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"type":"print","value":"1619-1366"},{"type":"electronic","value":"1619-1374"}],"subject":[],"published":{"date-parts":[[2024,3,20]]},"assertion":[{"value":"30 June 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"31 January 2024","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 February 2024","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 March 2024","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}