{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:45:35Z","timestamp":1770284735832,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":99,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,6,8]],"date-time":"2019-06-08T00:00:00Z","timestamp":1559952000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100004316","name":"International Business Machines Corporation","doi-asserted-by":"publisher","award":["IBM PhD Fellowship"],"award-info":[{"award-number":["IBM PhD Fellowship"]}],"id":[{"id":"10.13039\/100004316","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61802254"],"award-info":[{"award-number":["61802254"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001821","name":"Vienna Science and Technology Fund","doi-asserted-by":"publisher","award":["ICT15-003"],"award-info":[{"award-number":["ICT15-003"]}],"id":[{"id":"10.13039\/501100001821","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["S11407-N23"],"award-info":[{"award-number":["S11407-N23"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100011199","name":"European Research Council","doi-asserted-by":"publisher","award":["279307: Graph Games"],"award-info":[{"award-number":["279307: Graph Games"]}],"id":[{"id":"10.13039\/100011199","id-type":"DOI","asserted-by":"publisher"}]},{"name":"\u00d6sterreichischen Akademie der Wissenschaften","award":["DOC"],"award-info":[{"award-number":["DOC"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,6,8]]},"DOI":"10.1145\/3314221.3314581","type":"proceedings-article","created":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T21:02:18Z","timestamp":1559941338000},"page":"204-220","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":38,"title":["Cost analysis of nondeterministic probabilistic programs"],"prefix":"10.1145","author":[{"given":"Peixin","family":"Wang","sequence":"first","affiliation":[{"name":"Shanghai Jiao Tong University, China \/ East China Normal University, China"}]},{"given":"Hongfei","family":"Fu","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, China \/ East China Normal University, China"}]},{"given":"Amir Kafshdar","family":"Goharshady","sequence":"additional","affiliation":[{"name":"IST Austria, Austria"}]},{"given":"Krishnendu","family":"Chatterjee","sequence":"additional","affiliation":[{"name":"IST Austria, Austria"}]},{"given":"Xudong","family":"Qin","sequence":"additional","affiliation":[{"name":"East China Normal University, China"}]},{"given":"Wenjun","family":"Shi","sequence":"additional","affiliation":[{"name":"East China Normal University, China"}]}],"member":"320","published-online":{"date-parts":[[2019,6,8]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158122"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.12.008"},{"key":"e_1_3_2_2_3_1","first-page":"221","article-title":"Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis","volume":"2008","author":"Albert Elvira","year":"2008","unstructured":"Elvira Albert , Puri Arenas , Samir Genaim , and German Puebla . 2008 . Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis . In SAS 2008. 221 - 237 . Elvira Albert, Puri Arenas, Samir Genaim, and German Puebla. 2008. Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis. In SAS 2008. 221-237.","journal-title":"SAS"},{"key":"e_1_3_2_2_4_1","first-page":"157","article-title":"Cost Analysis of Java Bytecode","volume":"2007","author":"Albert Elvira","year":"2007","unstructured":"Elvira Albert , Puri Arenas , Samir Genaim , German Puebla , and Damiano Zanardini . 2007 . Cost Analysis of Java Bytecode . In ESOP 2007. 157 - 172 . Elvira Albert, Puri Arenas, Samir Genaim, German Puebla, and Damiano Zanardini. 2007. Cost Analysis of Java Bytecode. In ESOP 2007. 157-172.","journal-title":"ESOP"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/1882094.1882102"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/390013.808479"},{"key":"e_1_3_2_2_7_1","volume-title":"Effective Divergence Analysis for Linear Recurrence Sequences. In CONCUR","author":"Almagor Shaull","year":"2018","unstructured":"Shaull Almagor , Brynmor Chapman , Mehran Hosseini , Jo\u00ebl Ouaknine , and James Worrell . 2018 . Effective Divergence Analysis for Linear Recurrence Sequences. In CONCUR 2018. 42:1-42:15. Shaull Almagor, Brynmor Chapman, Mehran Hosseini, Jo\u00ebl Ouaknine, and James Worrell. 2018. Effective Divergence Analysis for Linear Recurrence Sequences. In CONCUR 2018. 42:1-42:15."},{"key":"e_1_3_2_2_8_1","first-page":"174","volume-title":"HEALTHINF","author":"Almomen Serene","year":"2012","unstructured":"Serene Almomen and Daniel A Menasc\u00e9 . 2012 . The Design of an Autonomic Controller for Self-managed Emergency Departments . In HEALTHINF 2012. Citeseer , 174 - 182 . Serene Almomen and Daniel A Menasc\u00e9. 2012. The Design of an Autonomic Controller for Self-managed Emergency Departments. In HEALTHINF 2012. Citeseer, 174-182."},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/SERE.2012.15"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2013.70"},{"key":"e_1_3_2_2_11_1","first-page":"45","article-title":"Temporal Reasoning for Procedural Programs","volume":"2010","author":"Alur Rajeev","year":"2010","unstructured":"Rajeev Alur and Swarat Chaudhuri . 2010 . Temporal Reasoning for Procedural Programs . In VMCAI 2010. 45 - 60 . Rajeev Alur and Swarat Chaudhuri. 2010. Temporal Reasoning for Procedural Programs. In VMCAI 2010. 45-60.","journal-title":"VMCAI"},{"key":"e_1_3_2_2_12_1","volume-title":"Understanding blockchain consensus models. Persistent","author":"Baliga Arati","year":"2017","unstructured":"Arati Baliga . 2017. Understanding blockchain consensus models. Persistent ( 2017 ). Arati Baliga. 2017. Understanding blockchain consensus models. Persistent (2017)."},{"key":"e_1_3_2_2_13_1","first-page":"323","article-title":"Proving Positive Almost-Sure Termination","author":"Bournez Olivier","year":"2005","unstructured":"Olivier Bournez and Florent Garnier . 2005 . Proving Positive Almost-Sure Termination . In RTA. 323 - 337 . Olivier Bournez and Florent Garnier. 2005. Proving Positive Almost-Sure Termination. In RTA. 323-337.","journal-title":"RTA."},{"key":"e_1_3_2_2_14_1","first-page":"491","article-title":"Linear Ranking with Reachability","volume":"2005","author":"Bradley Aaron R.","year":"2005","unstructured":"Aaron R. Bradley , Zohar Manna , and Henny B. Sipma . 2005 . Linear Ranking with Reachability . In CAV 2005. 491 - 504 . Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. 2005. Linear Ranking with Reachability. In CAV 2005. 491-504.","journal-title":"CAV"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2866575"},{"key":"e_1_3_2_2_16_1","first-page":"511","article-title":"Probabilistic Program Analysis with Martingales","volume":"2013","author":"Chakarov Aleksandar","year":"2013","unstructured":"Aleksandar Chakarov and Sriram Sankaranarayanan . 2013 . Probabilistic Program Analysis with Martingales . In CAV 2013. 511 - 526 . Aleksandar Chakarov and Sriram Sankaranarayanan. 2013. Probabilistic Program Analysis with Martingales. In CAV 2013. 511-526.","journal-title":"CAV"},{"key":"e_1_3_2_2_17_1","volume-title":"Termination of Nondeterministic Recursive Probabilistic Programs. CoRR abs\/1701.02944","author":"Chatterjee Krishnendu","year":"2017","unstructured":"Krishnendu Chatterjee and Hongfei Fu. 2017. Termination of Nondeterministic Recursive Probabilistic Programs. CoRR abs\/1701.02944 ( 2017 ). Krishnendu Chatterjee and Hongfei Fu. 2017. Termination of Nondeterministic Recursive Probabilistic Programs. CoRR abs\/1701.02944 (2017)."},{"key":"e_1_3_2_2_18_1","first-page":"3","volume-title":"CAV","author":"Chatterjee Krishnendu","year":"2016","unstructured":"Krishnendu Chatterjee , Hongfei Fu , and Amir Kafshdar Goharshady . 2016 . Termination Analysis of Probabilistic Programs Through Positivstellensatz's . In CAV 2016. 3 - 22 . Krishnendu Chatterjee, Hongfei Fu, and Amir Kafshdar Goharshady. 2016. Termination Analysis of Probabilistic Programs Through Positivstellensatz's. In CAV 2016. 3-22."},{"key":"e_1_3_2_2_19_1","first-page":"41","article-title":"Non-polynomial Worst-Case Analysis of Recursive Programs","volume":"2017","author":"Chatterjee Krishnendu","year":"2017","unstructured":"Krishnendu Chatterjee , Hongfei Fu , and Amir Kafshdar Goharshady . 2017 . Non-polynomial Worst-Case Analysis of Recursive Programs . In CAV 2017. 41 - 63 . Krishnendu Chatterjee, Hongfei Fu, and Amir Kafshdar Goharshady. 2017. Non-polynomial Worst-Case Analysis of Recursive Programs. In CAV 2017. 41-63.","journal-title":"CAV"},{"key":"e_1_3_2_2_20_1","first-page":"4700","article-title":"Computational Approaches for Stochastic Shortest Path on Succinct MDPs","volume":"2018","author":"Chatterjee Krishnendu","year":"2018","unstructured":"Krishnendu Chatterjee , Hongfei Fu , Amir Kafshdar Goharshady , and Nastaran Okati . 2018 . Computational Approaches for Stochastic Shortest Path on Succinct MDPs . In IJCAI 2018. 4700 - 4707 . Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, and Nastaran Okati. 2018. Computational Approaches for Stochastic Shortest Path on Succinct MDPs. In IJCAI 2018. 4700-4707.","journal-title":"IJCAI"},{"key":"e_1_3_2_2_21_1","volume-title":"CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I. 118-139","author":"Chatterjee Krishnendu","year":"2017","unstructured":"Krishnendu Chatterjee , Hongfei Fu , and Aniket Murhekar . 2017 . Automated Recurrence Analysis for Almost-Linear Expected-Runtime Bounds. In Computer Aided Verification - 29th International Conference , CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I. 118-139 . Krishnendu Chatterjee, Hongfei Fu, and Aniket Murhekar. 2017. Automated Recurrence Analysis for Almost-Linear Expected-Runtime Bounds. In Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I. 118-139."},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837639"},{"key":"e_1_3_2_2_23_1","volume-title":"Ergodic Mean-Payoff Games for the Analysis of Attacks in Crypto-Currencies. In CONCUR","author":"Chatterjee Krishnendu","year":"2018","unstructured":"Krishnendu Chatterjee , Amir Kafshdar Goharshady , Rasmus Ibsen-Jensen , and Yaron Velner . 2018 . Ergodic Mean-Payoff Games for the Analysis of Attacks in Crypto-Currencies. In CONCUR 2018. 11:1-11:17. Krishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, and Yaron Velner. 2018. Ergodic Mean-Payoff Games for the Analysis of Attacks in Crypto-Currencies. In CONCUR 2018. 11:1-11:17."},{"key":"e_1_3_2_2_24_1","first-page":"145","article-title":"Stochastic invariants for probabilistic termination","volume":"2017","author":"Chatterjee Krishnendu","year":"2017","unstructured":"Krishnendu Chatterjee , Petr Novotn?, and ?or?e ?ikeli?. 2017 . Stochastic invariants for probabilistic termination . In POPL 2017. 145 - 160 . Krishnendu Chatterjee, Petr Novotn?, and ?or?e ?ikeli?. 2017. Stochastic invariants for probabilistic termination. In POPL 2017. 145-160.","journal-title":"POPL"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1012996816178"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491423"},{"key":"e_1_3_2_2_27_1","first-page":"67","article-title":"Synthesis of Linear Ranking Functions","volume":"2001","author":"Colon Michael","year":"2001","unstructured":"Michael Colon and Henny Sipma . 2001 . Synthesis of Linear Ranking Functions . In TACAS 2001. 67 - 81 . Michael Colon and Henny Sipma. 2001. Synthesis of Linear Ranking Functions. In TACAS 2001. 67-81.","journal-title":"TACAS"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1145\/1133981.1134029","article-title":"Termination proofs for systems code","volume":"2006","author":"Cook Byron","year":"2006","unstructured":"Byron Cook , Andreas Podelski , and Andrey Rybalchenko . 2006 . Termination proofs for systems code . In PLDI 2006. 415 - 426 . Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2006. Termination proofs for systems code. In PLDI 2006. 415-426.","journal-title":"PLDI"},{"key":"e_1_3_2_2_29_1","volume-title":"Summarization for termination: no return! Formal Methods in System Design 35, 3","author":"Cook Byron","year":"2009","unstructured":"Byron Cook , Andreas Podelski , and Andrey Rybalchenko . 2009. Summarization for termination: no return! Formal Methods in System Design 35, 3 ( 2009 ), 369-387. Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2009. Summarization for termination: no return! Formal Methods in System Design 35, 3 (2009), 369-387."},{"key":"e_1_3_2_2_30_1","first-page":"47","article-title":"Ramsey vs","volume":"2013","author":"Zuleger Florian","year":"2013","unstructured":"Byron Cook, Abigail See, and Florian Zuleger . 2013 . Ramsey vs . Lexicographic Termination Proving. In TACAS 2013. 47 - 61 . Byron Cook, Abigail See, and Florian Zuleger. 2013. Ramsey vs. Lexicographic Termination Proving. In TACAS 2013. 47-61.","journal-title":"Lexicographic Termination Proving. In TACAS"},{"key":"e_1_3_2_2_31_1","first-page":"1","article-title":"Proving Program Invariance and Termination by Parametric Abstraction","volume":"2005","author":"Cousot Patrick","year":"2005","unstructured":"Patrick Cousot . 2005 . Proving Program Invariance and Termination by Parametric Abstraction , Lagrangian Relaxation and Semidefinite Programming. In VMCAI 2005. 1 - 24 . Patrick Cousot. 2005. Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming. In VMCAI 2005. 1-24.","journal-title":"Lagrangian Relaxation and Semidefinite Programming. In VMCAI"},{"key":"e_1_3_2_2_32_1","first-page":"238","article-title":"Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL 1977","author":"Cousot Patrick","year":"1977","unstructured":"Patrick Cousot and Radhia Cousot . 1977 . Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL 1977 . ACM , 238 - 252 . Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL 1977. ACM, 238-252.","journal-title":"ACM"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103687"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.joule.2018.04.016"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1327452.1327492"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1080\/00029890.1971.11992788"},{"key":"e_1_3_2_2_37_1","first-page":"123","article-title":"Proving Termination of Probabilistic Programs Using Patterns","volume":"2012","author":"Esparza Javier","year":"2012","unstructured":"Javier Esparza , Andreas Gaiser , and Stefan Kiefer . 2012 . Proving Termination of Probabilistic Programs Using Patterns . In CAV 2012. 123 - 138 . Javier Esparza, Andreas Gaiser, and Stefan Kiefer. 2012. Proving Termination of Probabilistic Programs Using Patterns. In CAV 2012. 123-138.","journal-title":"CAV"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677001"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90145-R"},{"key":"e_1_3_2_2_40_1","first-page":"282","volume-title":"Probabilistic NetKAT. In ESOP","author":"Foster Nate","year":"2016","unstructured":"Nate Foster , Dexter Kozen , Konstantinos Mamouras , Mark Reitblatt , and Alexandra Silva . 2016 . Probabilistic NetKAT. In ESOP 2016. Springer , 282 - 309 . Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt, and Alexandra Silva. 2016. Probabilistic NetKAT. In ESOP 2016. Springer, 282-309."},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837646"},{"key":"e_1_3_2_2_42_1","volume-title":"UAI","author":"Goodman Noah D","year":"2008","unstructured":"Noah D Goodman , Vikash K Mansinghka , Daniel Roy , Keith Bonawitz , and Joshua B Tenenbaum . 2008. Church: a language for generative models . In UAI 2008 . AUAI Press , 220-229. Noah D Goodman, Vikash K Mansinghka, Daniel Roy, Keith Bonawitz, and Joshua B Tenenbaum. 2008. Church: a language for generative models. In UAI 2008. AUAI Press, 220-229."},{"key":"e_1_3_2_2_43_1","unstructured":"Noah D Goodman and Andreas Stuhlmuller. 2014. The Design and Implementation of Probabilistic Programming Languages. http:\/\/dippl.org. (2014).  Noah D Goodman and Andreas Stuhlmuller. 2014. The Design and Implementation of Probabilistic Programming Languages. http:\/\/dippl.org. (2014)."},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2480359.2429119"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2593882.2593900"},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/507635.507666"},{"key":"e_1_3_2_2_47_1","first-page":"370","volume-title":"CAV","author":"Bhargav","year":"2008","unstructured":"Bhargav S. Gulavani and Sumit Gulwani. 2008. A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis . In CAV 2008 . 370 - 384 . Bhargav S. Gulavani and Sumit Gulwani. 2008. A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis. In CAV 2008. 370-384."},{"key":"e_1_3_2_2_48_1","first-page":"51","article-title":"SPEED","volume":"2009","author":"Gulwani Sumit","year":"2009","unstructured":"Sumit Gulwani . 2009 . SPEED : Symbolic Complexity Bound Analysis. In CAV 2009. 51 - 62 . Sumit Gulwani. 2009. SPEED: Symbolic Complexity Bound Analysis. In CAV 2009. 51-62.","journal-title":"Symbolic Complexity Bound Analysis. In CAV"},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1145\/1480881.1480898","article-title":"SPEED: precise and efficient static estimation of program computational complexity","volume":"2009","author":"Gulwani Sumit","year":"2009","unstructured":"Sumit Gulwani , Krishna K. Mehra , and Trishul M. Chilimbi . 2009 . SPEED: precise and efficient static estimation of program computational complexity . In POPL 2009. 127 - 139 . Sumit Gulwani, Krishna K. Mehra, and Trishul M. Chilimbi. 2009. SPEED: precise and efficient static estimation of program computational complexity. In POPL 2009. 127-139.","journal-title":"POPL"},{"key":"e_1_3_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1988.132.35"},{"key":"e_1_3_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211249"},{"key":"e_1_3_2_2_52_1","volume-title":"Amdahl's law in the multicore era. Computer 41, 7","author":"Hill Mark D","year":"2008","unstructured":"Mark D Hill and Michael R Marty . 2008. Amdahl's law in the multicore era. Computer 41, 7 ( 2008 ). Mark D Hill and Michael R Marty. 2008. Amdahl's law in the multicore era. Computer 41, 7 (2008)."},{"key":"e_1_3_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2362389.2362393"},{"key":"e_1_3_2_2_54_1","first-page":"781","volume-title":"Resource Aware ML. In CAV","author":"Hoffmann Jan","year":"2012","unstructured":"Jan Hoffmann , Klaus Aehlig , and Martin Hofmann . 2012 . Resource Aware ML. In CAV 2012. 781 - 786 . Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. 2012. Resource Aware ML. In CAV 2012. 781-786."},{"key":"e_1_3_2_2_55_1","first-page":"172","volume-title":"Amortized Resource Analysis with Polymorphic Recursion and Partial Big-Step Operational Semantics. In APLAS","author":"Hoffmann Jan","year":"2010","unstructured":"Jan Hoffmann and Martin Hofmann . 2010 . Amortized Resource Analysis with Polymorphic Recursion and Partial Big-Step Operational Semantics. In APLAS 2010. 172 - 187 . Jan Hoffmann and Martin Hofmann. 2010. Amortized Resource Analysis with Polymorphic Recursion and Partial Big-Step Operational Semantics. In APLAS 2010. 172-187."},{"key":"e_1_3_2_2_56_1","first-page":"287","volume-title":"Amortized Resource Analysis with Polynomial Potential. In ESOP","author":"Hoffmann Jan","year":"2010","unstructured":"Jan Hoffmann and Martin Hofmann . 2010 . Amortized Resource Analysis with Polynomial Potential. In ESOP 2010. 287 - 306 . Jan Hoffmann and Martin Hofmann. 2010. Amortized Resource Analysis with Polynomial Potential. In ESOP 2010. 287-306."},{"key":"e_1_3_2_2_57_1","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1145\/604131.604148","article-title":"Static prediction of heap space usage for first-order functional programs","volume":"2003","author":"Hofmann Martin","year":"2003","unstructured":"Martin Hofmann and Steffen Jost . 2003 . Static prediction of heap space usage for first-order functional programs . In POPL 2003. 185 - 197 . Martin Hofmann and Steffen Jost. 2003. Static prediction of heap space usage for first-order functional programs. In POPL 2003. 185-197.","journal-title":"POPL"},{"key":"e_1_3_2_2_58_1","first-page":"22","article-title":"Type-Based Amortised Heap-Space Analysis","volume":"2006","author":"Hofmann Martin","year":"2006","unstructured":"Martin Hofmann and Steffen Jost . 2006 . Type-Based Amortised Heap-Space Analysis . In ESOP 2006. 22 - 37 . Martin Hofmann and Steffen Jost. 2006. Type-Based Amortised Heap-Space Analysis. In ESOP 2006. 22-37.","journal-title":"ESOP"},{"key":"e_1_3_2_2_59_1","first-page":"317","article-title":"Efficient Type-Checking for Amortised Heap-Space Analysis","volume":"2009","author":"Hofmann Martin","year":"2009","unstructured":"Martin Hofmann and Dulma Rodriguez . 2009 . Efficient Type-Checking for Amortised Heap-Space Analysis . In CSL 2009. 317 - 331 . Martin Hofmann and Dulma Rodriguez. 2009. Efficient Type-Checking for Amortised Heap-Space Analysis. In CSL 2009. 317-331.","journal-title":"CSL"},{"key":"e_1_3_2_2_60_1","first-page":"70","article-title":"Recursion and Dynamic Data-structures in Bounded Space","volume":"1999","author":"Hughes John","year":"1999","unstructured":"John Hughes and Lars Pareto . 1999 . Recursion and Dynamic Data-structures in Bounded Space : Towards Embedded ML Programming. In ICFP 1999. 70 - 81 . John Hughes and Lars Pareto. 1999. Recursion and Dynamic Data-structures in Bounded Space: Towards Embedded ML Programming. In ICFP 1999. 70-81.","journal-title":"Towards Embedded ML Programming. In ICFP"},{"key":"e_1_3_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.240882"},{"key":"e_1_3_2_2_62_1","unstructured":"Claire Jones. 1989. Probabilistic Non-Determinism. Ph.D. Dissertation. The University of Edinburgh.   Claire Jones. 1989. Probabilistic Non-Determinism . Ph.D. Dissertation. The University of Edinburgh."},{"key":"e_1_3_2_2_63_1","first-page":"223","article-title":"Static determination of quantitative resource usage for higher-order programs","volume":"2010","author":"Jost Steffen","year":"2010","unstructured":"Steffen Jost , Kevin Hammond , Hans-Wolfgang Loidl , and Martin Hofmann . 2010 . Static determination of quantitative resource usage for higher-order programs . In POPL 2010. 223 - 236 . Steffen Jost, Kevin Hammond, Hans-Wolfgang Loidl, and Martin Hofmann. 2010. Static determination of quantitative resource usage for higher-order programs. In POPL 2010. 223-236.","journal-title":"POPL"},{"key":"e_1_3_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_23"},{"key":"e_1_3_2_2_65_1","volume-title":"Undecidable Problems for Probabilistic Network Programming. In MFCS","author":"Kahn David M.","year":"2017","unstructured":"David M. Kahn . 2017 . Undecidable Problems for Probabilistic Network Programming. In MFCS 2017. 68:1-68:17. David M. Kahn. 2017. Undecidable Problems for Probabilistic Network Programming. In MFCS 2017. 68:1-68:17."},{"key":"e_1_3_2_2_66_1","first-page":"364","article-title":"Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs","volume":"2016","author":"Kaminski Benjamin Lucien","year":"2016","unstructured":"Benjamin Lucien Kaminski , Joost-Pieter Katoen , Christoph Matheja , and Federico Olmedo . 2016 . Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs . In ESOP 2016. 364 - 389 . Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo. 2016. Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs. In ESOP 2016. 364-389.","journal-title":"ESOP"},{"key":"e_1_3_2_2_67_1","volume-title":"On the hardness of analyzing probabilistic programs. Acta Informatica","author":"Kaminski Benjamin Lucien","year":"2018","unstructured":"Benjamin Lucien Kaminski , Joost-Pieter Katoen , and Christoph Matheja . 2018. On the hardness of analyzing probabilistic programs. Acta Informatica ( 2018 ), 1-31. Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2018. On the hardness of analyzing probabilistic programs. Acta Informatica (2018), 1-31."},{"key":"e_1_3_2_2_68_1","first-page":"392","article-title":"Automatic Termination Verification for Higher-Order Functional Programs","volume":"2014","author":"Kuwahara Takuya","year":"2014","unstructured":"Takuya Kuwahara , Tachio Terauchi , Hiroshi Unno , and Naoki Kobayashi . 2014 . Automatic Termination Verification for Higher-Order Functional Programs . In ESOP 2014. 392 - 411 . Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, and Naoki Kobayashi. 2014. Automatic Termination Verification for Higher-Order Functional Programs. In ESOP 2014. 392-411.","journal-title":"ESOP"},{"key":"e_1_3_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/1498926.1498928"},{"key":"e_1_3_2_2_70_1","first-page":"81","article-title":"The size-change principle for program termination","volume":"2001","author":"Lee Chin Soon","year":"2001","unstructured":"Chin Soon Lee , Neil D. Jones , and Amir M. Ben-Amram . 2001 . The size-change principle for program termination . In POPL 2001. 81 - 92 . Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. 2001. The size-change principle for program termination. In POPL 2001. 81-92.","journal-title":"POPL"},{"key":"e_1_3_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158121"},{"key":"e_1_3_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1109\/MIC.2004.1260710"},{"key":"e_1_3_2_2_73_1","volume-title":"Bitcoin: A peer-to-peer electronic cash system.","author":"Nakamoto Satoshi","year":"2008","unstructured":"Satoshi Nakamoto . 2008 . Bitcoin: A peer-to-peer electronic cash system. (2008). Satoshi Nakamoto. 2008. Bitcoin: A peer-to-peer electronic cash system. (2008)."},{"key":"e_1_3_2_2_74_1","first-page":"496","article-title":"Bounded expectations: resource analysis for probabilistic programs","volume":"2018","author":"Ngo Van Chan","year":"2018","unstructured":"Van Chan Ngo , Quentin Carbonneaux , and Jan Hoffmann . 2018 . Bounded expectations: resource analysis for probabilistic programs . In PLDI 2018. 496 - 512 . Van Chan Ngo, Quentin Carbonneaux, and Jan Hoffmann. 2018. Bounded expectations: resource analysis for probabilistic programs. In PLDI 2018. 496-512.","journal-title":"PLDI"},{"key":"e_1_3_2_2_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/3156018"},{"key":"e_1_3_2_2_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935317"},{"key":"e_1_3_2_2_77_1","doi-asserted-by":"publisher","DOI":"10.5555\/2406808.2406811"},{"key":"e_1_3_2_2_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/2766189.2766191"},{"key":"e_1_3_2_2_79_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"e_1_3_2_2_80_1","volume-title":"Analysis of bitcoin pooled mining reward systems. arXiv preprint arXiv:1112.4980","author":"Rosenfeld Meni","year":"2011","unstructured":"Meni Rosenfeld . 2011. Analysis of bitcoin pooled mining reward systems. arXiv preprint arXiv:1112.4980 ( 2011 ). Meni Rosenfeld. 2011. Analysis of bitcoin pooled mining reward systems. arXiv preprint arXiv:1112.4980 (2011)."},{"key":"e_1_3_2_2_81_1","volume-title":"Nonparametric Bayesian Workshop, Int. Conf. on Machine Learning","volume":"22","author":"Roy DM","year":"2008","unstructured":"DM Roy , VK Mansinghka , ND Goodman , and JB Tenenbaum . 2008 . A stochastic programming perspective on nonparametric Bayes . In Nonparametric Bayesian Workshop, Int. Conf. on Machine Learning , Vol. 22 . 26. DM Roy, VK Mansinghka, ND Goodman, and JB Tenenbaum. 2008. A stochastic programming perspective on nonparametric Bayes. In Nonparametric Bayesian Workshop, Int. Conf. on Machine Learning, Vol. 22. 26."},{"key":"e_1_3_2_2_82_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27864-1_7"},{"key":"e_1_3_2_2_83_1","first-page":"165","volume-title":"ACM SIGPLAN Notices","volume":"50","author":"Adam","year":"2015","unstructured":"Adam ?cibior, Zoubin Ghahramani , and Andrew D Gordon . 2015 . Practical probabilistic programming with monads . In ACM SIGPLAN Notices , Vol. 50 . ACM, 165 - 176 . Adam ?cibior, Zoubin Ghahramani, and Andrew D Gordon. 2015. Practical probabilistic programming with monads. In ACM SIGPLAN Notices, Vol. 50. ACM, 165-176."},{"key":"e_1_3_2_2_84_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11424-013-1004-1"},{"key":"e_1_3_2_2_85_1","first-page":"351","article-title":"Polynomial Size Analysis of First-Order Functions","volume":"2007","author":"Shkaravska Olha","year":"2007","unstructured":"Olha Shkaravska , Ron van Kesteren , and Marko C. J. D. van Eekelen . 2007 . Polynomial Size Analysis of First-Order Functions . In TLCA 2007. 351 - 365 . Olha Shkaravska, Ron van Kesteren, and Marko C. J. D. van Eekelen. 2007. Polynomial Size Analysis of First-Order Functions. In TLCA 2007. 351-365.","journal-title":"TLCA"},{"key":"e_1_3_2_2_86_1","first-page":"745","volume-title":"CAV","author":"Sinn Moritz","year":"2014","unstructured":"Moritz Sinn , Florian Zuleger , and Helmut Veith . 2014 . A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis . In CAV 2014. 745 - 761 . Moritz Sinn, Florian Zuleger, and Helmut Veith. 2014. A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis. In CAV 2014. 745-761."},{"key":"e_1_3_2_2_87_1","volume-title":"Hash Rate: The estimated number of tera hashes per second (trillions of hashes per second) the Bitcoin network is performing. https:\/\/www.blockchain.com\/charts\/hashrate?scale=1&timespan=all. (Sept.","author":"Peter Smith","year":"2018","unstructured":"Peter Smith et al. 2018 . Hash Rate: The estimated number of tera hashes per second (trillions of hashes per second) the Bitcoin network is performing. https:\/\/www.blockchain.com\/charts\/hashrate?scale=1&timespan=all. (Sept. 2018). Peter Smith et al. 2018. Hash Rate: The estimated number of tera hashes per second (trillions of hashes per second) the Bitcoin network is performing. https:\/\/www.blockchain.com\/charts\/hashrate?scale=1&timespan=all. (Sept. 2018)."},{"key":"e_1_3_2_2_88_1","first-page":"557","article-title":"Cantor meets Scott: semantic foundations for probabilistic networks","volume":"2017","author":"Smolka Steffen","year":"2017","unstructured":"Steffen Smolka , Praveen Kumar , Nate Foster , Dexter Kozen , and Alexandra Silva . 2017 . Cantor meets Scott: semantic foundations for probabilistic networks . In POPL 2017. 557 - 571 . Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, and Alexandra Silva. 2017. Cantor meets Scott: semantic foundations for probabilistic networks. In POPL 2017. 557-571.","journal-title":"POPL"},{"key":"e_1_3_2_2_89_1","first-page":"216","volume-title":"PODS","author":"Sohn Kirack","year":"1991","unstructured":"Kirack Sohn and Allen Van Gelder . 1991 . Termination Detection in Logic Programs using Argument Sizes . In PODS 1991. 216 - 226 . Kirack Sohn and Allen Van Gelder. 1991. Termination Detection in Logic Programs using Argument Sizes. In PODS 1991. 216-226."},{"key":"e_1_3_2_2_90_1","first-page":"639","article-title":"Complexity verification using guided theorem enumeration","volume":"2017","author":"Srikanth Akhilesh","year":"2017","unstructured":"Akhilesh Srikanth , Burak Sahin , and William R. Harris . 2017 . Complexity verification using guided theorem enumeration . In POPL 2017. 639 - 652 . Akhilesh Srikanth, Burak Sahin, and William R. Harris. 2017. Complexity verification using guided theorem enumeration. In POPL 2017. 639-652.","journal-title":"POPL"},{"key":"e_1_3_2_2_91_1","first-page":"93","article-title":"Probabilistic algorithms in robotics","volume":"21","author":"Thrun Sebastian","year":"2000","unstructured":"Sebastian Thrun . 2000 . Probabilistic algorithms in robotics . Ai Magazine 21 , 4 (2000), 93 . Sebastian Thrun. 2000. Probabilistic algorithms in robotics. Ai Magazine 21, 4 (2000), 93.","journal-title":"Ai Magazine"},{"key":"e_1_3_2_2_92_1","doi-asserted-by":"publisher","DOI":"10.1145\/504729.504754"},{"key":"e_1_3_2_2_93_1","first-page":"1","article-title":"Design and Implementation of Probabilistic Programming Language Anglican. In IFL 2016","volume":"6","author":"Tolpin David","year":"2016","unstructured":"David Tolpin , Jan-Willem van de Meent , Hongseok Yang , and Frank Wood . 2016 . Design and Implementation of Probabilistic Programming Language Anglican. In IFL 2016 . ACM , 6 : 1 - 6 :12. David Tolpin, Jan-Willem van de Meent, Hongseok Yang, and Frank Wood. 2016. Design and Implementation of Probabilistic Programming Language Anglican. In IFL 2016. ACM, 6:1-6:12.","journal-title":"ACM"},{"key":"e_1_3_2_2_94_1","first-page":"43","article-title":"The Abstract Domain of Segmented Ranking Functions","volume":"2013","author":"Urban Caterina","year":"2013","unstructured":"Caterina Urban . 2013 . The Abstract Domain of Segmented Ranking Functions . In SAS 2013. 43 - 62 . Caterina Urban. 2013. The Abstract Domain of Segmented Ranking Functions. In SAS 2013. 43-62.","journal-title":"SAS"},{"key":"e_1_3_2_2_95_1","unstructured":"Fabian Vogelsteller Vitalik Buterin etal 2014. Ethereum whitepaper. (2014).  Fabian Vogelsteller Vitalik Buterin et al. 2014. Ethereum whitepaper. (2014)."},{"key":"e_1_3_2_2_96_1","first-page":"513","article-title":"PMAF: an algebraic framework for static analysis of probabilistic programs","volume":"2018","author":"Wang Di","year":"2018","unstructured":"Di Wang , Jan Hoffmann , and Thomas W. Reps . 2018 . PMAF: an algebraic framework for static analysis of probabilistic programs . In PLDI 2018. 513 - 528 . Di Wang, Jan Hoffmann, and Thomas W. Reps. 2018. PMAF: an algebraic framework for static analysis of probabilistic programs. In PLDI 2018. 513-528.","journal-title":"PLDI"},{"key":"e_1_3_2_2_97_1","volume-title":"Krishnendu Chatterjee, Xudong Qin, and Wenjun Shi.","author":"Wang Peixin","year":"2019","unstructured":"Peixin Wang , Hongfei Fu , Amir Kafshdar Goharshady , Krishnendu Chatterjee, Xudong Qin, and Wenjun Shi. 2019 . Cost Analysis of Nondeterministic Probabilistic Programs . arXiv preprint arXiv:1902.04659 (2019). Peixin Wang, Hongfei Fu, Amir Kafshdar Goharshady, Krishnendu Chatterjee, Xudong Qin, and Wenjun Shi. 2019. Cost Analysis of Nondeterministic Probabilistic Programs. arXiv preprint arXiv:1902.04659 (2019)."},{"key":"e_1_3_2_2_98_1","volume-title":"Probability with martingales","author":"Williams David","unstructured":"David Williams . 1991. Probability with martingales . Cambridge university press . David Williams. 1991. Probability with martingales. Cambridge university press."},{"key":"e_1_3_2_2_99_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11704-009-0074-7"}],"event":{"name":"PLDI '19: 40th ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Phoenix AZ USA","acronym":"PLDI '19","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314581","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3314221.3314581","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:53:22Z","timestamp":1750204402000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314581"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6,8]]},"references-count":99,"alternative-id":["10.1145\/3314221.3314581","10.1145\/3314221"],"URL":"https:\/\/doi.org\/10.1145\/3314221.3314581","relation":{},"subject":[],"published":{"date-parts":[[2019,6,8]]},"assertion":[{"value":"2019-06-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}