{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:16:48Z","timestamp":1784837808504,"version":"3.55.0"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032262035","type":"print"},{"value":"9783032262042","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"vor","delay-in-days":137,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>We present a one-fits-all programmatic approach to reason about a plethora of objectives on probabilistic programs. The first ingredient is to add a reward-statement to the language. We then define a program transformation applying a monotone function to the cumulative reward of the program. The key idea is that this transformation uses incremental differences in the reward. This simple, elegant approach enables to express e.g., higher moments, threshold probabilities of rewards, the expected excess over a budget, and moment-generating functions. All these objectives can now be analyzed using a single existing approach: probabilistic wp-reasoning. We automated verification using the Caesar deductive verifier and report on the application of the transformation to some examples.<\/jats:p>","DOI":"10.1007\/978-3-032-26204-2_29","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T15:51:13Z","timestamp":1779033073000},"page":"559-577","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Highly Incremental: A Simple Programmatic Approach for\u00a0Many Objectives"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4329-530X","authenticated-orcid":false,"given":"Philipp","family":"Schr\u00f6er","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"29_CR1","doi-asserted-by":"publisher","unstructured":"Ajdar\u00f3w, M., Ku\u010dcera, A., Novotn\u00fd, P.: Asymptotic analysis of probabilistic programs: when expectations do not meet our expectations. In: Jansen, N., et al. (eds) Principles of Verification: Cycling the Probabilistic Landscape: Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part I, pp. 85\u201397. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-75783-9_4","DOI":"10.1007\/978-3-031-75783-9_4"},{"key":"29_CR2","unstructured":"Amazon Web Services: AWS Lambda Pricing. https:\/\/aws.amazon.com\/lambda\/pricing\/. Accessed 1 Dec 2025"},{"key":"29_CR3","doi-asserted-by":"publisher","unstructured":"Avanzini, M., Moser, G., Schaper, M.: A modular cost analysis for probabilistic programs. Proc. ACM Program. Lang. 4(OOPSLA), 172:1\u2013172:30 (2020). https:\/\/doi.org\/10.1145\/3428240","DOI":"10.1145\/3428240"},{"key":"29_CR4","doi-asserted-by":"publisher","unstructured":"Batz, K., Chen, M., Kaminski, B.L., Katoen, JP., Matheja, C., Schr\u00f6er, P.: Latticed k-induction with an application to probabilistic programs. In: A. Silva and K.R.M. Leino. Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20\u201323, 2021, Proceedings, Part II. LNCS, vol. 12760, pp. 524\u2013549. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_25","DOI":"10.1007\/978-3-030-81688-9_25"},{"key":"29_CR5","doi-asserted-by":"publisher","unstructured":"Batz, K., Kaminski, B.L., Katoen, JP., Matheja, C.: How long, \u2013O Bayesian network, will \u2013I sample thee? \u2013A program analysis perspective on expected sampling times. In: Ahmed, A. (ed.) Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14\u201320, 2018, Proceedings. LNCS, vol. 10801, pp. 186\u2013213. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_7","DOI":"10.1007\/978-3-319-89884-1_7"},{"key":"29_CR6","doi-asserted-by":"publisher","unstructured":"Batz, K., Kaminski, B.L., Katoen, J., Matheja, C.: Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning. Proc. ACM Program. Lang. 5(POPL), 1\u201330 (2021). https:\/\/doi.org\/10.1145\/3434320","DOI":"10.1145\/3434320"},{"key":"29_CR7","doi-asserted-by":"publisher","unstructured":"Batz, K., Kaminski, B.L., Katoen, J., Matheja, C., Verscht, L.: A calculus for amortized expected runtimes. Proc. ACM Program. Lang. 7(POPL), 1957\u20131986 (2023). https:\/\/doi.org\/10.1145\/3571260","DOI":"10.1145\/3571260"},{"key":"29_CR8","doi-asserted-by":"publisher","unstructured":"Batz, K., Kaminski, B.L., Matheja, C., Winkler, T.: J-P: MDP. FP. PP: characterizing total expected rewards in Markov decision processes as least fixed points with an application to operational semantics of probabilistic programs. In: Jansen, N., et al. (eds.) Principles of Verification: Cycling the Probabilistic Landscape - Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part I. LNCS, vol. 15260, pp. 255\u2013302. Springer, Heidelberg (2024). https:\/\/doi.org\/10.1007\/978-3-031-75783-9_11","DOI":"10.1007\/978-3-031-75783-9_11"},{"key":"29_CR9","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Goharshady, A.K., Meggendorfer, T., \u017dikeli\u0107, U.: Quantitative bounds on resource usage of probabilistic programs. Proc. ACM Program. Lang. 8(OOPSLA1) (2024). https:\/\/doi.org\/10.1145\/3649824","DOI":"10.1145\/3649824"},{"key":"29_CR10","doi-asserted-by":"publisher","unstructured":"Chen, M., Katoen, J., Klinkenberg, L., Winkler, T.: Does a program yield the right distribution? - verifying probabilistic programs via generating functions. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7\u201310, 2022, Proceedings, Part I. LNCS, vol. 13371, pp. 79\u2013101. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_5","DOI":"10.1007\/978-3-031-13185-1_5"},{"issue":"OOPSLA1","key":"29_CR11","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1145\/3586051","volume":"7","author":"S Feng","year":"2023","unstructured":"Feng, S., Chen, M., Su, H., Kaminski, B.L., Katoen, J., Zhan, N.: Lower bounds for possibly divergent probabilistic programs. Proc. ACM Program. Lang. 7(OOPSLA1), 696\u2013726 (2023). https:\/\/doi.org\/10.1145\/3586051","journal-title":"Proc. ACM Program. Lang."},{"key":"29_CR12","unstructured":"Fristedt, B., and Gray, L.: A Modern Introduction to Probability Theory. In: Probability and Its Applications. Birkhauser Verlag AG, Basel, Switzerland (1996)"},{"key":"29_CR13","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1016\/J.PEVA.2013.11.004","volume":"73","author":"F Gretz","year":"2014","unstructured":"Gretz, F., Katoen, J., McIver, A.: Operational versus weakest pre-expectation semantics for the probabilistic guarded command language. Perform. Eval. 73, 110\u2013132 (2014). https:\/\/doi.org\/10.1016\/J.PEVA.2013.11.004","journal-title":"Perform. Eval."},{"key":"29_CR14","doi-asserted-by":"publisher","unstructured":"Hark, M., Kaminski, B.L., Giesl, J., Katoen, J.: Aiming low is harder: induction for lower bounds in probabilistic program verification. Proc. ACM Program. Lang. 4(POPL), 37:1\u201337:28 (2020). https:\/\/doi.org\/10.1145\/3371105","DOI":"10.1145\/3371105"},{"issue":"4","key":"29_CR15","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/S10009-021-00633-Z","volume":"24","author":"C Hensel","year":"2022","unstructured":"Hensel, C., Junges, S., Katoen, J., Quatmann, T., Volk, M.: The probabilistic model checker Storm. Int. J. Softw. Tools Technol. Transf. 24(4), 589\u2013610 (2022). https:\/\/doi.org\/10.1007\/S10009-021-00633-Z","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"29_CR16","doi-asserted-by":"publisher","unstructured":"Hurd, J., McIver, A., Morgan, C.: Probabilistic guarded commands mechanized in HOL. Theor. Comput. Sci. 346(1), 96\u2013112 (2005). https:\/\/doi.org\/10.1016\/J.TCS.2005.08.005","DOI":"10.1016\/J.TCS.2005.08.005"},{"key":"29_CR17","doi-asserted-by":"publisher","unstructured":"Kaminski, B.L.: Advanced weakest precondition calculi for probabilistic programs. Ph. D. thesis, RWTH Aachen University, Germany (2019). https:\/\/doi.org\/10.18154\/RWTH-2019-01829","DOI":"10.18154\/RWTH-2019-01829"},{"key":"29_CR18","doi-asserted-by":"publisher","unstructured":"Kaminski, B.L., Katoen, J.: On the hardness of almost-sure termination. In: Italiano, G.F., Pighizzini, G., Sannella, D. (eds.) Mathematical Foundations of Computer Science 2015 - 40th International Symposium, MFCS 2015, Milan, Italy, August 24\u201328, 2015, Proceedings, Part I. LNCS, vol. 9234, pp. 307\u2013318. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48057-1_24","DOI":"10.1007\/978-3-662-48057-1_24"},{"key":"29_CR19","doi-asserted-by":"publisher","unstructured":"Kaminski, B.L., Katoen, J., Matheja, C.: Expected runtime analyis by program verification. In: Barthe, G., Katoen, J., Silva, A. (eds.) Foundations of Probabilistic Programming, pp. 185\u2013220. Cambridge University Press (2020). https:\/\/doi.org\/10.1017\/9781108770750.007","DOI":"10.1017\/9781108770750.007"},{"key":"29_CR20","doi-asserted-by":"publisher","unstructured":"Kaminski, B.L., Katoen, J. Matheja, C.: Inferring covariances for probabilistic programs. In: Agha, G., Houdt, B.V.(eds.) Quantitative Evaluation of Systems - 13th International Conference, QEST 2016, Quebec City, QC, Canada, August 23\u201325, 2016, Proceedings. LNCS, vol. 9826, pp. 191\u2013206. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-319-43425-4_14","DOI":"10.1007\/978-3-319-43425-4_14"},{"key":"29_CR21","doi-asserted-by":"publisher","unstructured":"Kaminski, B.L., Katoen, J., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected run-times of probabilistic programs. In: Thiemann, P.(ed.) Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2\u20138, 2016, Proceedings. LNCS, vol. 9632, pp. 364\u2013389. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49498-1_15","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"29_CR22","doi-asserted-by":"publisher","unstructured":"Kaminski, B.L., Katoen, J., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected runtimes of randomized algorithms. J. ACM 65(5), 30:1\u201330:68 (2018). https:\/\/doi.org\/10.1145\/3208102","DOI":"10.1145\/3208102"},{"key":"29_CR23","doi-asserted-by":"publisher","unstructured":"Kura, S., Urabe, N., Hasuo, I.: Tail probabilities for randomized program runtimes via martingales for higher moments. In: Vojnar, T., Zhang, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6\u201311, 2019, Proceedings, Part II. LNCS, vol. 11428, pp. 135\u2013153. Springer, Heidelberg (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_8","DOI":"10.1007\/978-3-030-17465-1_8"},{"key":"29_CR24","doi-asserted-by":"publisher","unstructured":"Li, J., Zhang, Y.: Compiling with generating functions. Proc. ACM Program. Lang. 9(ICFP) (2025). https:\/\/doi.org\/10.1145\/3747534","DOI":"10.1145\/3747534"},{"key":"29_CR25","doi-asserted-by":"publisher","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Springer (2005). https:\/\/doi.org\/10.1007\/0-387-27006-X_2","DOI":"10.1007\/0-387-27006-X_2"},{"key":"29_CR26","doi-asserted-by":"publisher","unstructured":"McIver, A., Morgan, C., Kaminski, B.L., Katoen, J.: A new proof rule for almost-sure termination. Proc. ACM Program. Lang. 2(POPL), 33:1\u201333:28 (2018). https:\/\/doi.org\/10.1145\/3158121","DOI":"10.1145\/3158121"},{"issue":"3","key":"29_CR27","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/S10817-025-09736-7","volume":"69","author":"H Mertens","year":"2025","unstructured":"Mertens, H., Katoen, J., Quatmann, T., Winkler, T.: Computing expected visiting times and stationary distributions in markov chains: fast and accurate. J. Autom. Reason. 69(3), 23 (2025). https:\/\/doi.org\/10.1007\/S10817-025-09736-7","journal-title":"J. Autom. Reason."},{"key":"29_CR28","doi-asserted-by":"publisher","unstructured":"Moosbrugger, M., Stankovic, M., Bartocci, E., Kov\u00e1cs, L.: This is the moment for probabilistic loops. Proc. ACM Program. Lang. 6(OOPSLA2), 1497\u20131525 (2022). https:\/\/doi.org\/10.1145\/3563341","DOI":"10.1145\/3563341"},{"key":"29_CR29","doi-asserted-by":"publisher","unstructured":"M\u00fcllner, J., Moosbrugger, M., Kov\u00e1cs, L.: Strong invariants are hard: on the hardness of strongest polynomial invariants for (probabilistic) Programs. Proc. ACM Program. Lang. 8(POPL), 882\u2013910 (2024). https:\/\/doi.org\/10.1145\/3632872","DOI":"10.1145\/3632872"},{"key":"29_CR30","doi-asserted-by":"publisher","unstructured":"Ngo, V.C., Carbonneaux, Q., Hoffmann, J.: Bounded expectations: resource analysis for probabilistic programs. In: Foster, J.S., Grossman, D. (eds.) Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18\u201322, 2018, pp. 496\u2013512. ACM (2018). https:\/\/doi.org\/10.1145\/3192366.3192394","DOI":"10.1145\/3192366.3192394"},{"key":"29_CR31","unstructured":"Park, D.: Fixpoint induction and proofs of program properties. Mach. Intell. 5 (1969)"},{"key":"29_CR32","doi-asserted-by":"publisher","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics. Wiley (1994). https:\/\/doi.org\/10.1002\/9780470316887","DOI":"10.1002\/9780470316887"},{"issue":"OOPSLA2","key":"29_CR33","doi-asserted-by":"publisher","first-page":"2052","DOI":"10.1145\/3622870","volume":"7","author":"P Schr\u00f6er","year":"2023","unstructured":"Schr\u00f6er, P., Batz, K., Kaminski, B.L., Katoen, J., Matheja, C.: A deductive verification infrastructure for probabilistic programs. Proc. ACM Program. Lang. 7(OOPSLA2), 2052\u20132082 (2023). https:\/\/doi.org\/10.1145\/3622870","journal-title":"Proc. ACM Program. Lang."},{"key":"29_CR34","doi-asserted-by":"crossref","unstructured":"Schr\u00f6er, P., Katoen, J.-P.: Highly incremental: a simple programmatic approach for many objectives (extended version) (2026)","DOI":"10.1007\/978-3-032-26204-2_29"},{"issue":"2","key":"29_CR35","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1137\/0213021","volume":"13","author":"M Sharir","year":"1984","unstructured":"Sharir, M., Pnueli, A., Hart, S.: Verification of probabilistic programs. SIAM J. Comput. 13(2), 292\u2013314 (1984). https:\/\/doi.org\/10.1137\/0213021","journal-title":"SIAM J. Comput."},{"key":"29_CR36","doi-asserted-by":"publisher","unstructured":"Wang, D., Hoffmann, J., Reps, T.W.: Central moment analysis for cost accumulators in probabilistic programs. In: Freund, S.N., Yahav, E. (eds.) PLDI 2021: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20\u201325, 2021, pp. 559\u2013573. ACM (2021). https:\/\/doi.org\/10.1145\/3453483.3454062","DOI":"10.1145\/3453483.3454062"},{"key":"29_CR37","doi-asserted-by":"publisher","unstructured":"Wang, P., Fu, H., Goharshady, A.K., Chatterjee, K., Qin, X., Shi, W.: Cost analysis of nondeterministic probabilistic programs. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI 2019, pp. 204\u2013220. Association for Computing Machinery, Phoenix, AZ, USA (2019). https:\/\/doi.org\/10.1145\/3314221.3314581","DOI":"10.1145\/3314221.3314581"},{"key":"29_CR38","unstructured":"Winkler, T.: A Note on the Expected Runtime of Discrete Probabilistic While Loops (Personal Note) (2023)"},{"key":"29_CR39","doi-asserted-by":"crossref","unstructured":"Zaiser, F., Murawski, A.S., Ong, C.L.: Exact bayesian inference on discrete models via probability generating functions: a probabilistic programming approach. In: Oh, A., Naumann, T., Globerson, A., Saenko, K., Hardt, M., Levine, S. (eds.) Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 \u2013 16, 2023 (2023)","DOI":"10.52202\/075280-0113"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26204-2_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T18:00:41Z","timestamp":1783015241000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26204-2_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262035","9783032262042"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26204-2_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"18 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/fm-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}