{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,27]],"date-time":"2026-03-27T17:07:04Z","timestamp":1774631224481,"version":"3.50.1"},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2024,12,3]],"date-time":"2024-12-03T00:00:00Z","timestamp":1733184000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,12,3]],"date-time":"2024-12-03T00:00:00Z","timestamp":1733184000000},"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":["Form Methods Syst Des"],"published-print":{"date-parts":[[2025,8]]},"DOI":"10.1007\/s10703-024-00466-x","type":"journal-article","created":{"date-parts":[[2024,12,3]],"date-time":"2024-12-03T09:47:47Z","timestamp":1733219267000},"page":"278-306","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Data-driven invariant learning for probabilistic programs"],"prefix":"10.1007","volume":"66","author":[{"given":"Jialu","family":"Bao","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nitesh","family":"Trivedi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Drashti","family":"Pathak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Justin","family":"Hsu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Subhajit","family":"Roy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,12,3]]},"reference":[{"key":"466_CR1","doi-asserted-by":"publisher","unstructured":"Kozen D (1981) Semantics of probabilistic programs 22(3) https:\/\/doi.org\/10.1016\/0022-0000(81)90036-2","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"466_CR2","doi-asserted-by":"publisher","DOI":"10.1145\/3290352","author":"C Smith","year":"2019","unstructured":"Smith C, Hsu J, Albarghouthi A (2019). Trace abstraction modulo probability In: POPL. https:\/\/doi.org\/10.1145\/3290352","journal-title":"Trace abstraction modulo probability. In: POPL"},{"key":"466_CR3","doi-asserted-by":"publisher","unstructured":"Albarghouthi A, Hsu J (2018) Synthesizing coupling proofs of differential privacy. In: POPL. https:\/\/doi.org\/10.1145\/3158146","DOI":"10.1145\/3158146"},{"key":"466_CR4","doi-asserted-by":"publisher","unstructured":"Carbin M, Misailovic S, Rinard MC (2013) Verifying quantitative reliability for programs that execute on unreliable hardware. In: OOPSLA. https:\/\/doi.org\/10.1145\/2509136.2509546","DOI":"10.1145\/2509136.2509546"},{"key":"466_CR5","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00060","author":"S Roy","year":"2021","unstructured":"Roy S, Hsu J, Albarghouthi A (2021). Learning differentially private mechanisms In: SP. https:\/\/doi.org\/10.1109\/SP40001.2021.00060","journal-title":"Learning differentially private mechanisms. In: SP"},{"key":"466_CR6","doi-asserted-by":"crossref","unstructured":"Baier C, Clarke EM, Hartonas-Garmhausen V, Kwiatkowska MZ, Ryan M (1997) Symbolic model checking for probabilistic processes. In: ICALP","DOI":"10.1007\/3-540-63165-8_199"},{"key":"466_CR7","doi-asserted-by":"publisher","unstructured":"Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: Verification of probabilistic real-time systems. In: CAV. https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"466_CR8","doi-asserted-by":"publisher","unstructured":"Dehnert C, Junges S, Katoen J, Volk M (2017) A storm is coming: A modern probabilistic model checker. In: CAV. https:\/\/doi.org\/10.1007\/978-3-319-63390-9_31","DOI":"10.1007\/978-3-319-63390-9_31"},{"key":"466_CR9","doi-asserted-by":"publisher","unstructured":"Kozen D (1985) A probabilistic PDL 30(2) https:\/\/doi.org\/10.1016\/0022-0000(85)90012-1","DOI":"10.1016\/0022-0000(85)90012-1"},{"issue":"1145\/229542","key":"466_CR10","volume":"10","author":"C Morgan","year":"1996","unstructured":"Morgan C, McIver A, Seidel K (1996) Probabilistic predicate transformers. TOPLAS 10(1145\/229542):229547","journal-title":"Probabilistic predicate transformers. TOPLAS"},{"key":"466_CR11","doi-asserted-by":"publisher","unstructured":"McIver A, Morgan C (2005) Abstraction, Refinement, and Proof for Probabilistic Systems. https:\/\/doi.org\/10.1007\/b138392","DOI":"10.1007\/b138392"},{"key":"466_CR12","doi-asserted-by":"publisher","unstructured":"Dijkstra EW (1975) Guarded commands, non-determinancy and a calculus for the derivation of programs. In: Language Hierarchies and Interfaces. https:\/\/doi.org\/10.1007\/3-540-07994-7_51","DOI":"10.1007\/3-540-07994-7_51"},{"key":"466_CR13","doi-asserted-by":"publisher","unstructured":"Gretz F, Katoen J, McIver A (2013) Prinsys - on a quest for probabilistic loop invariants. In: QEST. https:\/\/doi.org\/10.1007\/978-3-642-40196-1_17","DOI":"10.1007\/978-3-642-40196-1_17"},{"key":"466_CR14","doi-asserted-by":"publisher","unstructured":"Chen Y, Hong C, Wang B, Zhang L (2015) Counterexample-guided polynomial loop invariant generation by Lagrange interpolation. In: CAV. https:\/\/doi.org\/10.1007\/978-3-319-21690-4_44","DOI":"10.1007\/978-3-319-21690-4_44"},{"key":"466_CR15","doi-asserted-by":"publisher","unstructured":"Flanagan C, Leino KRM (2001) Houdini, an annotation assistant for esc\/java. In: FME. https:\/\/doi.org\/10.1007\/3-540-45251-6_29","DOI":"10.1007\/3-540-45251-6_29"},{"key":"466_CR16","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.01.015","author":"MD Ernst","year":"2007","unstructured":"Ernst MD, Perkins JH, Guo PJ, McCamant S, Pacheco C, Tschantz MS, Xiao C (2007) The Daikon system for dynamic detection of likely invariants. Sci Comput Program. https:\/\/doi.org\/10.1016\/j.scico.2007.01.015","journal-title":"Sci. Comput. Program."},{"key":"466_CR17","unstructured":"Quinlan JR (1992) Learning with continuous classes. In: AJCAI, vol. 92"},{"key":"466_CR18","unstructured":"Yang Y, Morillo IG, Hospedales TM (2018) Deep neural decision trees. CoRR arXiv preprint arXiv:1806.06988"},{"key":"466_CR19","doi-asserted-by":"crossref","unstructured":"Chatterjee K, Fu H, Goharshady AK (2016) Termination analysis of probabilistic programs through Positivstellensatz\u2019s. In: CAV","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"466_CR20","doi-asserted-by":"publisher","unstructured":"Chatterjee K, Fu H, Novotn\u00fd P, Hasheminezhad R (2016)Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. In: POPL. https:\/\/doi.org\/10.1145\/2837614.2837639","DOI":"10.1145\/2837614.2837639"},{"key":"466_CR21","doi-asserted-by":"publisher","unstructured":"McIver A, Morgan C, Kaminski BL, Katoen J (2018) A new proof rule for almost-sure termination. In: POPL. https:\/\/doi.org\/10.1145\/3158121","DOI":"10.1145\/3158121"},{"key":"466_CR22","doi-asserted-by":"publisher","unstructured":"Batz K, Kaminski BL, Katoen J, Matheja C (2021) Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning. In: POPL. https:\/\/doi.org\/10.1145\/3434320","DOI":"10.1145\/3434320"},{"key":"466_CR23","doi-asserted-by":"publisher","unstructured":"Kaminski BL, Katoen J, Matheja C, Olmedo F (2016) Weakest precondition reasoning for expected run-times of probabilistic programs. In: ESOP. https:\/\/doi.org\/10.1007\/978-3-662-49498-1_15","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"466_CR24","doi-asserted-by":"publisher","DOI":"10.1145\/3371105","author":"M Hark","year":"2020","unstructured":"Hark M, Kaminski BL, Giesl J, Katoen J (2020). Aiming low is harder: induction for lower bounds in probabilistic program verification. https:\/\/doi.org\/10.1145\/3371105","journal-title":"Aiming low is harder: induction for lower bounds in probabilistic program verification."},{"key":"466_CR25","unstructured":"Park D (1969) Fixpoint induction and proofs of program properties. Machine intelligence 5"},{"key":"466_CR26","doi-asserted-by":"publisher","unstructured":"Kaminski BL, Katoen J-P (2017) A weakest pre-expectation semantics for mixed-sign expectations. In: LICS. https:\/\/doi.org\/10.5555\/3329995.3330088","DOI":"10.5555\/3329995.3330088"},{"key":"466_CR27","unstructured":"Leighton T, Rubinfeld R (2006) Random Walks \u2013 Lecture notes in Mathematics for Computer Science. MIT CS 6.042\/18.062. https:\/\/web.mit.edu\/neboat\/Public\/6.042\/randomwalks.pdf"},{"key":"466_CR28","doi-asserted-by":"crossref","unstructured":"Huang M, Fu H, Chatterjee K, Goharshady AK (2019) Modular verification for almost-sure termination of probabilistic programs. Proceedings of the ACM on Programming Languages 3(OOPSLA), 1\u201329","DOI":"10.1145\/3360555"},{"key":"466_CR29","doi-asserted-by":"crossref","unstructured":"Majumdar R, Sathiyanarayana V (2024) Sound and complete proof rules for probabilistic termination. arXiv preprint arXiv:2404.19724","DOI":"10.1145\/3704899"},{"key":"466_CR30","doi-asserted-by":"publisher","unstructured":"Bartocci E, Kov\u00e1cs L, Stankovi\u010d M (2020) Mora-automatic generation of moment-based invariants. In: TACAS. https:\/\/doi.org\/10.1007\/978-3-030-45190-5_28","DOI":"10.1007\/978-3-030-45190-5_28"},{"key":"466_CR31","doi-asserted-by":"crossref","unstructured":"Feng Y, Zhang L, Jansen DN, Zhan N, Xia B (2017) Finding polynomial loop invariants for probabilistic programs. In: ATVA","DOI":"10.1007\/978-3-319-68167-2_26"},{"key":"466_CR32","doi-asserted-by":"crossref","unstructured":"Batz K, Chen M, Junges S, Kaminski BL, Katoen J-P, Matheja C (2023) Probabilistic program verification via inductive synthesis of inductive invariants. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 410\u2013429. Springer","DOI":"10.1007\/978-3-031-30820-8_25"},{"key":"466_CR33","doi-asserted-by":"publisher","unstructured":"Chakarov A, Sankaranarayanan S (2014) Expectation invariants for probabilistic program loops as fixed points. In: SAS. https:\/\/doi.org\/10.1007\/978-3-319-10936-7_6","DOI":"10.1007\/978-3-319-10936-7_6"},{"key":"466_CR34","doi-asserted-by":"publisher","unstructured":"Wang D, Hoffmann J, Reps TW (2018) PMAF: an algebraic framework for static analysis of probabilistic programs. In: PLDI. https:\/\/doi.org\/10.1145\/3192366.3192408","DOI":"10.1145\/3192366.3192408"},{"key":"466_CR35","doi-asserted-by":"publisher","unstructured":"Chakarov A, Sankaranarayanan S (2013) Probabilistic program analysis with martingales. In: CAV . https:\/\/doi.org\/10.1007\/978-3-642-39799-8_34","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"466_CR36","doi-asserted-by":"publisher","unstructured":"Barthe G, Espitau T, Ferrer\u00a0Fioriti LM, Hsu J (2016) Synthesizing probabilistic invariants via Doob\u2019s decomposition. In: CAV. https:\/\/doi.org\/10.1007\/978-3-319-41528-4_3","DOI":"10.1007\/978-3-319-41528-4_3"},{"key":"466_CR37","doi-asserted-by":"publisher","unstructured":"Bartocci E, Kov\u00e1cs L, Stankovi\u010d M (2019) Automatic generation of moment-based invariants for prob-solvable loops. In: ATVA. https:\/\/doi.org\/10.1007\/978-3-030-31784-3_15","DOI":"10.1007\/978-3-030-31784-3_15"},{"key":"466_CR38","doi-asserted-by":"publisher","unstructured":"Kura S, Urabe N, Hasuo I (2019) Tail probabilities for randomized program runtimes via martingales for higher moments. In: TACAS. https:\/\/doi.org\/10.1007\/978-3-030-17465-1_8","DOI":"10.1007\/978-3-030-17465-1_8"},{"key":"466_CR39","doi-asserted-by":"publisher","unstructured":"Wang D, Hoffmann J, Reps T (2021) Central moment analysis for cost accumulators in probabilistic programs. In: PLDI. https:\/\/doi.org\/10.1145\/3453483.3454062","DOI":"10.1145\/3453483.3454062"},{"key":"466_CR40","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_1","author":"A Abate","year":"2021","unstructured":"Abate A, Giacobbe M, Roy D (2021). Learning probabilistic termination proofs In: CAV. https:\/\/doi.org\/10.1007\/978-3-030-81688-9_1","journal-title":"Learning probabilistic termination proofs. In: CAV"},{"key":"466_CR41","doi-asserted-by":"publisher","unstructured":"Garg P, Neider D, Madhusudan P, Roth D (2016) Learning invariants using decision trees and implication counterexamples. In: POPL. https:\/\/doi.org\/10.1145\/2914770.2837664","DOI":"10.1145\/2914770.2837664"},{"key":"466_CR42","doi-asserted-by":"publisher","unstructured":"Miltner A, Padhi S, Millstein T, Walker D (2020) Data-driven inference of representation invariants. In: PLDI 20. https:\/\/doi.org\/10.1145\/3385412.3385967","DOI":"10.1145\/3385412.3385967"},{"key":"466_CR43","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0249-7","author":"A Solar-Lezama","year":"2013","unstructured":"Solar-Lezama A (2013) Program sketching. Int J Softw Tools Technol Transf. https:\/\/doi.org\/10.1007\/s10009-012-0249-7","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"466_CR44","doi-asserted-by":"publisher","unstructured":"Si X, Dai H, Raghothaman M, Naik M, Song L (2018) Learning loop invariants for program verification. In: NeurIPS. https:\/\/doi.org\/10.5555\/3327757.3327873","DOI":"10.5555\/3327757.3327873"},{"key":"466_CR45","doi-asserted-by":"crossref","unstructured":"Lahiri S, Roy S (2022) Almost correct invariants: Synthesizing inductive invariants by fuzzing proofs. In: ISSTA","DOI":"10.1145\/3533767.3534381"},{"key":"466_CR46","doi-asserted-by":"publisher","unstructured":"Aguirre A, Barthe G, Hsu J, Kaminski BL, Katoen J-P, Matheja C (2021) A pre-expectation calculus for probabilistic sensitivity. In: POPL. https:\/\/doi.org\/10.1145\/3434333","DOI":"10.1145\/3434333"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-024-00466-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-024-00466-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-024-00466-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,13]],"date-time":"2025-08-13T10:21:47Z","timestamp":1755080507000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-024-00466-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,12,3]]},"references-count":46,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,8]]}},"alternative-id":["466"],"URL":"https:\/\/doi.org\/10.1007\/s10703-024-00466-x","relation":{"has-preprint":[{"id-type":"doi","id":"10.21203\/rs.3.rs-3162619\/v1","asserted-by":"object"}]},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,12,3]]},"assertion":[{"value":"12 July 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 November 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 December 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}