{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T05:29:15Z","timestamp":1743139755550,"version":"3.40.3"},"publisher-location":"Cham","reference-count":52,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031757822"},{"type":"electronic","value":"9783031757839"}],"license":[{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-75783-9_1","type":"book-chapter","created":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T06:27:09Z","timestamp":1731392829000},"page":"3-40","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Automatic Compositional Checking of\u00a0Multi-object TypeState Properties of\u00a0Software"],"prefix":"10.1007","author":[{"given":"Radu","family":"Grigore","sequence":"first","affiliation":[]},{"given":"Dino","family":"Distefano","sequence":"additional","affiliation":[]},{"given":"Nikos","family":"Tzevelekos","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,11,13]]},"reference":[{"key":"1_CR1","unstructured":"CodeQL website. https:\/\/codeql.github.com\/docs\/"},{"issue":"1","key":"1_CR2","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/j.entcs.2007.10.013","volume":"197","author":"I Aktug","year":"2008","unstructured":"Aktug, I., Naliuka, K.: ConSpec \u2013 a formal language for policy specification. Electr. Notes Theor. Comput. Sci. 197(1), 45\u201358 (2008)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Allan, C., et al.: Adding trace matching with free variables to AspectJ. In: Johnson, R.E., Gabriel, R.P. (eds.) OOPSLA, pp. 345\u2013364. ACM (2005)","DOI":"10.1145\/1094811.1094839"},{"issue":"10","key":"1_CR4","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/1449955.1449776","volume":"43","author":"M Arnold","year":"2008","unstructured":"Arnold, M., Vechev, M., Yahav, E.: QVM: an efficient runtime for detecting defects in deployed systems. SIGPLAN Not. 43(10), 143\u2013162 (2008). https:\/\/doi.org\/10.1145\/1449955.1449776","journal-title":"SIGPLAN Not."},{"key":"1_CR5","doi-asserted-by":"publisher","unstructured":"Avgustinov, P., de\u00a0Moor, O., Jones, M.P., Sch\u00e4fer, M.: QL: object-oriented queries on relational data. In: Krishnamurthi, S., Lerner, B.S. (eds.) 30th European Conference on Object-Oriented Programming, ECOOP 2016, Rome, Italy, 18\u201322 July 2016. LIPIcs, vol.\u00a056, pp. 2:1\u20132:25. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2016). https:\/\/doi.org\/10.4230\/LIPICS.ECOOP.2016.2","DOI":"10.4230\/LIPICS.ECOOP.2016.2"},{"issue":"5","key":"1_CR6","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1109\/MS.2008.130","volume":"25","author":"N Ayewah","year":"2008","unstructured":"Ayewah, N., Hovemeyer, D., Morgenthaler, J.D., Penix, J., Pugh, W.: Using static analysis to find bugs. IEEE Softw. 25(5), 22\u201329 (2008). https:\/\/doi.org\/10.1109\/MS.2008.130","journal-title":"IEEE Softw."},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/3-540-44585-4_25","volume-title":"Computer Aided Verification","author":"T Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 260\u2013264. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_25"},{"issue":"6","key":"1_CR8","doi-asserted-by":"publisher","first-page":"27","DOI":"10.5381\/jot.2004.3.6.a2","volume":"3","author":"M Barnett","year":"2004","unstructured":"Barnett, M., DeLine, R., F\u00e4hndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. J. Object Technol. 3(6), 27\u201356 (2004)","journal-title":"J. Object Technol."},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-75632-5_1","volume-title":"Lectures on Runtime Verification","author":"E Bartocci","year":"2018","unstructured":"Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 1\u201333. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_1"},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-319-95582-7_18","volume-title":"Formal Methods","author":"P Berger","year":"2018","unstructured":"Berger, P., Katoen, J.-P., \u00c1brah\u00e1m, E., Waez, M.T.B., Rambow, T.: Verifying auto-generated C code from simulink. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 312\u2013328. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-95582-7_18"},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-27864-1_2","volume-title":"Static Analysis","author":"D Beyer","year":"2004","unstructured":"Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: The Blast query language for software verification. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 2\u201318. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27864-1_2"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184\u2013190. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Bierhoff, K., Aldrich, J.: Lightweight object specification with typestates. In: Wermelinger, M., Gall, H. (eds.) ESEC\/SIGSOFT FSE, pp. 217\u2013226. ACM (2005)","DOI":"10.1145\/1095430.1081741"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Bierhoff, K., Aldrich, J.: Modular typestate checking of aliased objects. In: Gabriel, R.P., Bacon, D.F., Lopes, C.V., Jr., G.L.S. (eds.) OOPSLA, pp. 301\u2013320. ACM (2007)","DOI":"10.1145\/1297105.1297050"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Blanchet, B., et al.: A static analyzer for large safety-critical software. In: PLDI, pp. 196\u2013207. ACM (2003)","DOI":"10.1145\/781131.781153"},{"key":"1_CR16","unstructured":"Bunk, T.: LTL Software model checking in CPAchecker. Master\u2019s thesis, Institut f\u00fcr Informatik Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen (2019)"},{"key":"1_CR17","doi-asserted-by":"publisher","unstructured":"Calcagno, C., Distefano, D.: Infer: an automatic program verifier for memory safety of c programs. In: Bobaru, M.G., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NASA Formal Methods. Lecture Notes in Computer Science, vol.\u00a06617, pp. 459\u2013465. Springer, Heidelberg (2011).https:\/\/doi.org\/10.1007\/978-3-642-20398-5","DOI":"10.1007\/978-3-642-20398-5"},{"key":"1_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-17524-9_1","volume-title":"NASA Formal Methods","author":"C Calcagno","year":"2015","unstructured":"Calcagno, C., et al.: Moving fast with software verification. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 3\u201311. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-17524-9_1"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. In: Shao, Z., Pierce, B.C. (eds.) POPL, pp. 289\u2013300. ACM (2009)","DOI":"10.1145\/1594834.1480917"},{"key":"1_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15"},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/978-3-540-24851-4_21","volume-title":"ECOOP 2004 \u2013 Object-Oriented Programming","author":"R DeLine","year":"2004","unstructured":"DeLine, R., F\u00e4hndrich, M.: Typestates for objects. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 465\u2013490. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24851-4_21"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Demri, S., Lazic, R.: LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log. 10(3) (2009)","DOI":"10.1145\/1507244.1507246"},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-319-21690-4_4","volume-title":"Computer Aided Verification","author":"D Dietsch","year":"2015","unstructured":"Dietsch, D., Heizmann, M., Langenfeld, V., Podelski, A.: Fairness modulo theory: a new approach to LTL software model checking. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 49\u201366. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_4"},{"key":"1_CR24","unstructured":"Distefano, D.: The facebook infer static analyzer. In: TACAS 2017, Invited Talk (2017)"},{"issue":"8","key":"1_CR25","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1145\/3338112","volume":"62","author":"D Distefano","year":"2019","unstructured":"Distefano, D., F\u00e4hndrich, M., Logozzo, F., O\u2019Hearn, P.W.: Scaling static analyses at facebook. Commun. ACM 62(8), 62\u201370 (2019). https:\/\/doi.org\/10.1145\/3338112","journal-title":"Commun. ACM"},{"key":"1_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-319-68690-5_8","volume-title":"Formal Methods and Software Engineering","author":"Z Duan","year":"2017","unstructured":"Duan, Z., Tian, C., Duan, Z.: Verifying temporal properties of C programs via lazy abstraction. In: Duan, Z., Ong, L. (eds.) ICFEM 2017. LNCS, vol. 10610, pp. 122\u2013139. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68690-5_8"},{"key":"1_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/978-3-642-54862-8_36","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Ermis","year":"2014","unstructured":"Ermis, E., Nutz, A., Dietsch, D., Hoenicke, J., Podelski, A.: Ultimate Kojak. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 421\u2013423. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_36"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Fink, S.J., Yahav, E., Dor, N., Ramalingam, G., Geay, E.: Effective typestate verification in the presence of aliasing. In: Pollock, L.L., Pezz\u00e8, M. (eds.) ISSTA, pp. 133\u2013144. ACM (2006)","DOI":"10.1145\/1146238.1146254"},{"key":"1_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-642-36742-7_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Grigore","year":"2013","unstructured":"Grigore, R., Distefano, D., Petersen, R.L., Tzevelekos, N.: Runtime verification based on register automata. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 260\u2013276. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_19"},{"issue":"4","key":"1_CR30","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model checking java programs using java pathfinder. STTT 2(4), 366\u2013381 (2000)","journal-title":"STTT"},{"key":"1_CR31","doi-asserted-by":"crossref","unstructured":"Havelund, K., Rosu, G.: Monitoring programs using rewriting. In: ASE, pp. 135\u2013143. IEEE Computer Society (2001)","DOI":"10.1109\/ASE.2001.989799"},{"key":"1_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-642-39799-8_2","volume-title":"Computer Aided Verification","author":"M Heizmann","year":"2013","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 36\u201352. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_2"},{"key":"1_CR33","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Launchbury, J., Mitchell, J.C. (eds.) Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, OR, USA, 16\u201318 January 2002, pp. 58\u201370. ACM (2002). https:\/\/doi.org\/10.1145\/503272.503279","DOI":"10.1145\/503272.503279"},{"issue":"5","key":"1_CR34","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker spin. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"1_CR35","unstructured":"Jackson, D.: Software Abstractions - Logic, Language, and Analysis. MIT Press (2006). http:\/\/mitpress.mit.edu\/catalog\/item\/default.asp?ttype=2&tid=10928"},{"key":"1_CR36","doi-asserted-by":"crossref","unstructured":"Jin, D., Meredith, P.O., Lee, C., Rosu, G.: JavaMOP: efficient parametric runtime monitoring framework. In: Glinz, M., Murphy, G.C., Pezz\u00e8, M. (eds.) ICSE, pp. 1427\u20131430. IEEE (2012)","DOI":"10.1109\/ICSE.2012.6227231"},{"key":"1_CR37","unstructured":"http:\/\/www.eecs.ucf.edu\/~leavens\/JML"},{"issue":"2","key":"1_CR38","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1016\/0304-3975(94)90242-9","volume":"134","author":"M Kaminski","year":"1994","unstructured":"Kaminski, M., Francez, N.: Finite-memory automata. Theor. Comput. Sci. 134(2), 329\u2013363 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"553","DOI":"10.1007\/3-540-36577-X_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Khurshid","year":"2003","unstructured":"Khurshid, S., P\u0102s\u0102reanu, C.S., Visser, W.: Generalized symbolic execution for model checking and testing. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 553\u2013568. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36577-X_40"},{"issue":"4","key":"1_CR40","doi-asserted-by":"publisher","first-page":"795","DOI":"10.1007\/s10515-019-00267-1","volume":"26","author":"O Legunsen","year":"2019","unstructured":"Legunsen, O., Awar, N.A., Xu, X., Hassan, W.U., Rosu, G., Marinov, D.: How effective are existing Java API specifications for finding bugs during runtime verification? Autom. Softw. Eng. 26(4), 795\u2013837 (2019). https:\/\/doi.org\/10.1007\/s10515-019-00267-1","journal-title":"Autom. Softw. Eng."},{"key":"1_CR41","doi-asserted-by":"crossref","unstructured":"Mao, K., et al.: PrivacyCAT: privacy-aware code analysis at scale. In: ICSE 2024 Software Engineering in Practice (2024)","DOI":"10.1145\/3639477.3639742"},{"issue":"3","key":"1_CR42","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1145\/1013560.1013562","volume":"5","author":"F Neven","year":"2004","unstructured":"Neven, F., Schwentick, T., Vianu, V.: Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Log. 5(3), 403\u2013435 (2004)","journal-title":"ACM Trans. Comput. Log."},{"key":"1_CR43","doi-asserted-by":"publisher","unstructured":"O\u2019Hearn, P.W.: A primer on separation logic (and automatic program verification and analysis). In: Nipkow, T., Grumberg, O., Hauptmann, B. (eds.) Software Safety and Security - Tools for Analysis and Verification, NATO Science for Peace and Security Series - D: Information and Communication Security, vol.\u00a033, pp. 286\u2013318. IOS Press (2012). https:\/\/doi.org\/10.3233\/978-1-61499-028-4-286","DOI":"10.3233\/978-1-61499-028-4-286"},{"key":"1_CR44","doi-asserted-by":"crossref","unstructured":"Raad, A., Berdine, J., Dang, H.H., Dreyer, D., O\u2019Hearn, P., Villard, J.: Local reasoning about the presence of bugs: incorrectness separation logic. In: CAV (2020)","DOI":"10.1007\/978-3-030-53291-8_14"},{"key":"1_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/978-3-319-08867-9_7","volume-title":"Computer Aided Verification","author":"Z Rakamari\u0107","year":"2014","unstructured":"Rakamari\u0107, Z., Emmi, M.: SMACK: decoupling source language details from verifier implementations. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 106\u2013113. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_7"},{"key":"1_CR46","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55\u201374. IEEE Computer Society (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"1_CR47","doi-asserted-by":"publisher","unstructured":"Scholz, B., Jordan, H., Subotic, P., Westmann, T.: On fast large-scale program analysis in Datalog. In: Zaks, A., Hermenegildo, M.V. (eds.) Proceedings of the 25th International Conference on Compiler Construction, CC 2016, Barcelona, Spain, 12\u201318 March 2016, pp. 196\u2013206. ACM (2016).https:\/\/doi.org\/10.1145\/2892208.2892226","DOI":"10.1145\/2892208.2892226"},{"key":"1_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-642-24206-9_14","volume-title":"Datalog Reloaded","author":"Y Smaragdakis","year":"2011","unstructured":"Smaragdakis, Y., Bravenboer, M.: Using datalog for fast and easy program analysis. In: de Moor, O., Gottlob, G., Furche, T., Sellers, A. (eds.) Datalog 2.0 2010. LNCS, vol. 6702, pp. 245\u2013251. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24206-9_14"},{"issue":"1","key":"1_CR49","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1109\/TSE.1986.6312929","volume":"12","author":"RE Strom","year":"1986","unstructured":"Strom, R.E., Yemini, S.: Typestate: a programming language concept for enhancing software reliability. IEEE Trans. Softw. Eng. 12(1), 157\u2013171 (1986). https:\/\/doi.org\/10.1109\/TSE.1986.6312929","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"2","key":"1_CR50","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G.P., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. 10(2), 203\u2013232 (2003)","journal-title":"Autom. Softw. Eng."},{"key":"1_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/11575467_8","volume-title":"Programming Languages and Systems","author":"J Whaley","year":"2005","unstructured":"Whaley, J., Avots, D., Carbin, M., Lam, M.S.: Using datalog with binary decision diagrams for program analysis. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 97\u2013118. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11575467_8"},{"key":"1_CR52","doi-asserted-by":"publisher","unstructured":"Zhang, X., Mangal, R., Grigore, R., Naik, M., Yang, H.: On abstraction refinement for program analyses in Datalog. In: O\u2019Boyle, M.F.P., Pingali, K. (eds.) ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201914, Edinburgh, United Kingdom, 09\u201311 June 2014, pp. 239\u2013248. ACM (2014). https:\/\/doi.org\/10.1145\/2594291.2594327","DOI":"10.1145\/2594291.2594327"}],"container-title":["Lecture Notes in Computer Science","Principles of Verification: Cycling the Probabilistic Landscape"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-75783-9_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T07:02:09Z","timestamp":1731394929000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-75783-9_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,13]]},"ISBN":["9783031757822","9783031757839"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-75783-9_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,11,13]]},"assertion":[{"value":"13 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}