{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:49:57Z","timestamp":1775868597649,"version":"3.50.1"},"publisher-location":"Cham","reference-count":68,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030816872","type":"print"},{"value":"9783030816889","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,15]],"date-time":"2021-07-15T00:00:00Z","timestamp":1626307200000},"content-version":"vor","delay-in-days":195,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We revisit two well-established verification techniques,<jats:italic>k-induction<\/jats:italic>and<jats:italic>bounded model checking<\/jats:italic>(BMC), in the more general setting of fixed point theory over complete lattices. Our main theoretical contribution is<jats:italic>latticed k-induction<\/jats:italic>, which (i) generalizes classical<jats:italic>k<\/jats:italic>-induction for verifying transition systems, (ii) generalizes Park induction for bounding fixed points of monotonic maps on complete lattices, and (iii) extends from naturals<jats:italic>k<\/jats:italic>to transfinite ordinals<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\kappa $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>\u03ba<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>, thus yielding<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\kappa $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>\u03ba<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula><jats:italic>-induction<\/jats:italic>.<\/jats:p><jats:p>The lattice-theoretic understanding of<jats:italic>k<\/jats:italic>-induction and BMC enables us to apply both techniques to the<jats:italic>fully automatic verification of infinite-state probabilistic programs<\/jats:italic>. Our prototypical implementation manages to automatically verify non-trivial specifications for probabilistic programs taken from the literature that\u2014using existing techniques\u2014cannot be verified without synthesizing a stronger inductive invariant first.<\/jats:p>","DOI":"10.1007\/978-3-030-81688-9_25","type":"book-chapter","created":{"date-parts":[[2021,7,16]],"date-time":"2021-07-16T16:20:47Z","timestamp":1626452447000},"page":"524-549","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Latticed k-Induction with an Application to Probabilistic Programs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8705-2564","authenticated-orcid":false,"given":"Kevin","family":"Batz","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9663-7441","authenticated-orcid":false,"given":"Mingshuai","family":"Chen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5185-2324","authenticated-orcid":false,"given":"Benjamin Lucien","family":"Kaminski","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9151-0441","authenticated-orcid":false,"given":"Christoph","family":"Matheja","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4329-530X","authenticated-orcid":false,"given":"Philipp","family":"Schr\u00f6er","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,15]]},"reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"Abramsky, Jung: Domain theory. In: Handbook of Logic in Computer Science, vol. 3 (1994)","DOI":"10.1093\/oso\/9780198537625.001.0001"},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"Agrawal, Chatterjee, Novotn\u00fd: Lexicographic ranking supermartingales. PACMPL 2(POPL) (2018)","DOI":"10.1145\/3158122"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Amtoft, Banerjee: A theory of slicing for imperative probabilistic programs. TOPLAS 42(2) (2020)","DOI":"10.1145\/3372895"},{"key":"25_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-319-63387-9_8","volume-title":"Computer Aided Verification","author":"C Baier","year":"2017","unstructured":"Baier, C., Klein, J., Leuschner, L., Parker, D., Wunderlich, S.: Ensuring the reliability of your model checker: interval iteration for Markov decision processes. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 160\u2013180. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_8"},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"Baldan, et al.: Fixpoint theory - upside down. In: FoSSaCS (2021)","DOI":"10.1007\/978-3-030-71995-1_4"},{"key":"25_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-319-41528-4_3","volume-title":"Computer Aided Verification","author":"G Barthe","year":"2016","unstructured":"Barthe, G., Espitau, T., Ferrer Fioriti, L.M., Hsu, J.: Synthesizing probabilistic invariants via Doob\u2019s decomposition. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 43\u201361. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_3"},{"key":"25_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/978-3-030-53291-8_27","volume-title":"Computer Aided Verification","author":"K Batz","year":"2020","unstructured":"Batz, K., Junges, S., Kaminski, B.L., Katoen, J.-P., Matheja, C., Schr\u00f6er, P.: PrIC3: property directed reachability for MDPs. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 512\u2013538. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_27"},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"Batz, et al.: Latticed k-induction with an application to probabilistic programs (extended version). arXiv (2021)","DOI":"10.1007\/978-3-030-81688-9_25"},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"Batz, et al.: Relatively complete verification of probabilistic programs. PACMPL 5(POPL) (2021)","DOI":"10.1145\/3434320"},{"key":"25_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"622","DOI":"10.1007\/978-3-319-21690-4_42","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2015","unstructured":"Beyer, D., Dangl, M., Wendler, P.: Boosting k-induction with continuously-refined invariants. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 622\u2013640. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_42"},{"key":"25_CR11","unstructured":"Biere: Bounded model checking. In: Handbook of Satisfiability (2009)"},{"key":"25_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14"},{"key":"25_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/3-540-48683-6_8","volume-title":"Computer Aided Verification","author":"A Biere","year":"1999","unstructured":"Biere, A., Clarke, E., Raimi, R., Zhu, Y.: Verifying safety properties of a PowerPC \u2013 microprocessor using symbolic model checking without BDDs. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 60\u201371. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48683-6_8"},{"key":"25_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7"},{"key":"25_CR15","doi-asserted-by":"crossref","unstructured":"Chadha, Viswanathan: A counterexample-guided abstraction-refinement framework for Markov decision processes. TOCL 12(1) (2010)","DOI":"10.1145\/1838552.1838553"},{"key":"25_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/978-3-642-39799-8_34","volume-title":"Computer Aided Verification","author":"A Chakarov","year":"2013","unstructured":"Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 511\u2013526. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_34"},{"key":"25_CR17","unstructured":"Clarke, et al.: Bounded model checking using satisfiability solving. Formal Methods Syst. Des. 19(1) (2001)"},{"key":"25_CR18","doi-asserted-by":"crossref","unstructured":"Cousot, Cousot: Constructive versions of Tarski\u2019s fixed point theorems. Pacific J. Math. 82(1) (1979)","DOI":"10.2140\/pjm.1979.82.43"},{"key":"25_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/3-540-44804-7_3","volume-title":"Process Algebra and Probabilistic Methods. Performance Modelling and Verification","author":"PR D\u2019Argenio","year":"2001","unstructured":"D\u2019Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reachability analysis of probabilistic systems by successive refinements. In: de Alfaro, L., Gilmore, S. (eds.) PAPM-PROBMIV 2001. LNCS, vol. 2165, pp. 39\u201356. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44804-7_3"},{"key":"25_CR20","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-0-387-35190-2_13","volume-title":"Advances in Hardware Design and Verification","author":"D D\u00e9harbe","year":"1997","unstructured":"D\u00e9harbe, D., Moreira, A.M.: Using induction and BDDs to model check invariants. In: Advances in Hardware Design and Verification. IAICT, vol. 105, pp. 203\u2013213. Springer, Boston, MA (1997). https:\/\/doi.org\/10.1007\/978-0-387-35190-2_13"},{"key":"25_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-642-12002-2_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"AF Donaldson","year":"2010","unstructured":"Donaldson, A.F., Kroening, D., R\u00fcmmer, P.: Automatic analysis of scratch-pad memory code for heterogeneous multicore processors. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 280\u2013295. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_24"},{"key":"25_CR22","doi-asserted-by":"crossref","unstructured":"Donaldson, Kroening, R\u00fcmmer: Automatic analysis of DMA races using model checking and k-induction. Formal Methods Syst. Des. 39(1) (2011)","DOI":"10.1007\/s10703-011-0124-2"},{"key":"25_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-642-23702-7_26","volume-title":"Static Analysis","author":"AF Donaldson","year":"2011","unstructured":"Donaldson, A.F., Haller, L., Kroening, D., R\u00fcmmer, P.: Software verification using k-induction. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 351\u2013368. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-23702-7_26"},{"key":"25_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1007\/978-3-319-68167-2_26","volume-title":"Automated Technology for Verification and Analysis","author":"Y Feng","year":"2017","unstructured":"Feng, Y., Zhang, L., Jansen, D.N., Zhan, N., Xia, B.: Finding polynomial loop invariants for probabilistic programs. In: D\u2019Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 400\u2013416. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_26"},{"key":"25_CR25","unstructured":"Gario, Micheli: PySMT: a solver-agnostic library for fast prototyping of SMT-based algorithms. In: SMT Workshop (2015)"},{"key":"25_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/978-3-319-41528-4_4","volume-title":"Computer Aided Verification","author":"T Gehr","year":"2016","unstructured":"Gehr, T., Misailovic, S., Vechev, M.: PSI: exact symbolic inference for probabilistic programs. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 62\u201383. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_4"},{"key":"25_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72\u201383. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63166-6_10"},{"key":"25_CR28","doi-asserted-by":"crossref","unstructured":"Gretz, Katoen: McIver: operational versus weakest pre-expectation semantics for the probabilistic guarded command language. Perform. Eval. 73 (2014)","DOI":"10.1016\/j.peva.2013.11.004"},{"key":"25_CR29","doi-asserted-by":"crossref","unstructured":"Gurfinkel, Ivrii: K-induction without unrolling. In: FMCAD (2017)","DOI":"10.23919\/FMCAD.2017.8102253"},{"key":"25_CR30","doi-asserted-by":"crossref","unstructured":"Han, Katoen, Damman: Counterexample generation in probabilistic model checking. IEEE Trans. Softw. Eng. 35(2) (2009)","DOI":"10.1109\/TSE.2009.5"},{"key":"25_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1007\/978-3-030-53291-8_26","volume-title":"Computer Aided Verification","author":"A Hartmanns","year":"2020","unstructured":"Hartmanns, A., Kaminski, B.L.: Optimistic value iteration. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 488\u2013511. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_26"},{"key":"25_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-58085-9_75","volume-title":"Types for Proofs and Programs","author":"L Helmink","year":"1994","unstructured":"Helmink, L., Sellink, M.P.A., Vaandrager, F.W.: Proof-checking a data link protocol. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, pp. 127\u2013165. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58085-9_75"},{"key":"25_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-030-01090-4_23","volume-title":"Automated Technology for Verification and Analysis","author":"Z Huang","year":"2018","unstructured":"Huang, Z., Wang, Z., Misailovic, S.: PSense: automatic sensitivity analysis for probabilistic programs. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 387\u2013403. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_23"},{"key":"25_CR34","doi-asserted-by":"crossref","unstructured":"Hurd, McIver, Morgan: Probabilistic guarded commands mechanized in HOL. Theor. Comput. Sci. 346(1) (2005)","DOI":"10.1016\/j.tcs.2005.08.005"},{"key":"25_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-319-46520-3_5","volume-title":"Automated Technology for Verification and Analysis","author":"N Jansen","year":"2016","unstructured":"Jansen, N., Dehnert, C., Kaminski, B.L., Katoen, J.-P., Westhofen, L.: Bounded model checking for probabilistic programs. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 68\u201385. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_5"},{"key":"25_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/11691372_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Jhala","year":"2006","unstructured":"Jhala, R., McMillan, K.L.: A practical and complete approach to predicate refinement. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 459\u2013473. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11691372_33"},{"key":"25_CR37","doi-asserted-by":"crossref","unstructured":"Jovanovi\u0107, Dutertre: Property-directed k-induction. In: FMCAD (2016)","DOI":"10.1109\/FMCAD.2016.7886665"},{"key":"25_CR38","unstructured":"Kaminski: Advanced weakest precondition calculi for probabilistic programs. Ph.D. thesis, RWTH Aachen University, Germany (2019)"},{"key":"25_CR39","doi-asserted-by":"crossref","unstructured":"Kaminski, Katoen, Matheja: On the hardness of analyzing probabilistic programs. Acta Inform. 56(3) (2019)","DOI":"10.1007\/s00236-018-0321-1"},{"key":"25_CR40","doi-asserted-by":"crossref","unstructured":"Kaminski, et al.: Weakest precondition reasoning for expected runtimes of randomized algorithms. J. ACM 65(5) (2018)","DOI":"10.1145\/3208102"},{"key":"25_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/978-3-642-15769-1_24","volume-title":"Static Analysis","author":"J-P Katoen","year":"2010","unstructured":"Katoen, J.-P., McIver, A.K., Meinicke, L.A., Morgan, C.C.: Linear-invariant generation for probabilistic programs: automated support for proof-based methods. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 390\u2013406. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15769-1_24"},{"key":"25_CR42","doi-asserted-by":"crossref","unstructured":"King, Barrett, Tinelli: Leveraging linear and mixed integer programming for SMT. In: SMT (2014)","DOI":"10.1109\/FMCAD.2014.6987606"},{"key":"25_CR43","unstructured":"Knaster: Un th\u00e9or\u00e8me sur les functions d\u2019ensembles. Ann. Soc. Pol. Math. 6 (1928)"},{"key":"25_CR44","doi-asserted-by":"crossref","unstructured":"Kozen: A probabilistic PDL. J. Comput. Syst. Sci. 30(2) (1985)","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"25_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-030-25543-5_21","volume-title":"Computer Aided Verification","author":"HG Vediramana Krishnan","year":"2019","unstructured":"Vediramana Krishnan, H.G., Vizel, Y., Ganesh, V., Gurfinkel, A.: Interpolating strong induction. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 367\u2013385. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_21"},{"key":"25_CR46","doi-asserted-by":"crossref","unstructured":"Kushilevitz, Rabin: Randomized mutual exclusion algorithms revisited. In: PODC (1992)","DOI":"10.1145\/135419.135468"},{"key":"25_CR47","doi-asserted-by":"crossref","unstructured":"Lassez, Nguyen, Sonenberg: Fixed point theorems and semantics. Inf. Process. Lett. 14(3) (1982)","DOI":"10.1016\/0020-0190(82)90065-5"},{"key":"25_CR48","unstructured":"Lumbroso: Optimal discrete uniform generation from coin flips, and applications. arXiv (2013)"},{"key":"25_CR49","doi-asserted-by":"crossref","unstructured":"McIver, Morgan: Abstraction, refinement and proof for probabilistic systems (2005)","DOI":"10.1145\/1059816.1059824"},{"key":"25_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1\u201313. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_1"},{"key":"25_CR51","doi-asserted-by":"crossref","unstructured":"McMillan: An interpolating theorem prover. Theor. Comput. Sci. 345(1) (2005)","DOI":"10.1016\/j.tcs.2005.07.003"},{"key":"25_CR52","doi-asserted-by":"crossref","unstructured":"Meyer, Hark, Giesl: Inferring expected runtimes of probabilistic integer programs using expected sizes. In: TACAS (2021, to appear)","DOI":"10.26226\/morressier.604907f41a80aac83ca25cf4"},{"key":"25_CR53","unstructured":"Milner: Communication and concurrency (1989)"},{"key":"25_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"25_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/978-3-540-45069-6_2","volume-title":"Computer Aided Verification","author":"L de Moura","year":"2003","unstructured":"de Moura, L., Rue\u00df, H., Sorea, M.: Bounded model checking and induction: from refutation to verification. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 14\u201326. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_2"},{"key":"25_CR56","doi-asserted-by":"crossref","unstructured":"Ngo, Carbonneaux, Hoffmann: Bounded expectations: resource analysis for probabilistic programs. In: PLDI (2018)","DOI":"10.1145\/3192366.3192394"},{"key":"25_CR57","unstructured":"Park: Fixpoint induction and proofs of program properties. Mach. Intell. 5 (1969)"},{"key":"25_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-540-76637-7_24","volume-title":"Programming Languages and Systems","author":"D Pous","year":"2007","unstructured":"Pous, D.: Complete lattices and up-to techniques. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 351\u2013366. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-76637-7_24"},{"key":"25_CR59","doi-asserted-by":"crossref","unstructured":"Pous, Sangiorgi: Enhancements of the bisimulation proof method. In: Advanced Topics in Bisimulation and Coinduction, vol. 52 (2012)","DOI":"10.1017\/CBO9780511792588"},{"key":"25_CR60","doi-asserted-by":"crossref","unstructured":"Puterman: Markov Decision Processes (1994)","DOI":"10.1002\/9780470316887"},{"key":"25_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1007\/978-3-319-96145-3_37","volume-title":"Computer Aided Verification","author":"T Quatmann","year":"2018","unstructured":"Quatmann, T., Katoen, J.-P.: Sound value iteration. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 643\u2013661. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_37"},{"key":"25_CR62","doi-asserted-by":"crossref","unstructured":"Rabehaja, Sanders: Refinement algebra with explicit probabilism. In: TASE (2009)","DOI":"10.1109\/TASE.2009.53"},{"key":"25_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/978-3-662-54580-5_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"W Rocha","year":"2017","unstructured":"Rocha, W., Rocha, H., Ismail, H., Cordeiro, L., Fischer, B.: DepthK: a k-induction verifier based on invariant inference for C programs. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 360\u2013364. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_23"},{"key":"25_CR64","doi-asserted-by":"crossref","unstructured":"Sch\u00fcle, Schneider: Bounded model checking of infinite state systems. Formal Methods Syst. Des. 30(1) (2007)","DOI":"10.1007\/s10703-006-0019-9"},{"key":"25_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-40922-X_8","volume-title":"Formal Methods in Computer-Aided Design","author":"M Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a SAT-solver. In: Hunt, W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 127\u2013144. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-40922-X_8"},{"key":"25_CR66","doi-asserted-by":"crossref","unstructured":"Tarski: A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math. 5(2) (1955)","DOI":"10.2140\/pjm.1955.5.285"},{"key":"25_CR67","doi-asserted-by":"crossref","unstructured":"Wang, Hoffmann, Reps: PMAF: an algebraic framework for static analysis of probabilistic programs. In: PLDI (2018)","DOI":"10.1145\/3211994"},{"key":"25_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/978-3-540-93900-9_29","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Wimmer","year":"2008","unstructured":"Wimmer, R., Braitling, B., Becker, B.: Counterexample generation for discrete-time Markov chains using bounded model checking. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 366\u2013380. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-93900-9_29"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-81688-9_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,6]],"date-time":"2023-11-06T04:42:22Z","timestamp":1699245742000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-81688-9_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030816872","9783030816889"],"references-count":68,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-81688-9_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"15 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"290","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"63","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16 tool papers and 5 invited papers are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}