{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:11:58Z","timestamp":1775873518325,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":88,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,6,11]],"date-time":"2018-06-11T00:00:00Z","timestamp":1528675200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-15-C-0082"],"award-info":[{"award-number":["FA8750-15-C-0082"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Eric and Wendy Schmidt Fund"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,6,11]]},"DOI":"10.1145\/3192366.3192394","type":"proceedings-article","created":{"date-parts":[[2018,6,12]],"date-time":"2018-06-12T08:16:01Z","timestamp":1528791361000},"page":"496-512","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":60,"title":["Bounded expectations: resource analysis for probabilistic programs"],"prefix":"10.1145","author":[{"given":"Van Chan","family":"Ngo","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, USA"}]},{"given":"Quentin","family":"Carbonneaux","sequence":"additional","affiliation":[{"name":"Yale University, USA"}]},{"given":"Jan","family":"Hoffmann","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}]}],"member":"320","published-online":{"date-parts":[[2018,6,11]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_6"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33125-1_27"},{"key":"e_1_3_2_2_3_1","unstructured":"R. B. Ash and C. Dol\u00e9ans-Dade. 2000. Probability and Measure Theory. Academic Press.  R. B. Ash and C. Dol\u00e9ans-Dade. 2000. Probability and Measure Theory. Academic Press."},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_6"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784753"},{"key":"e_1_3_2_2_6_1","volume-title":"24th International Conference on Rewriting Techniques and Applications (RTA\u201913)","author":"Avanzini Martin","year":"2013","unstructured":"Martin Avanzini and Georg Moser . 2013 . A Combination Framework for Complexity . In 24th International Conference on Rewriting Techniques and Applications (RTA\u201913) . Martin Avanzini and Georg Moser. 2013. A Combination Framework for Complexity. In 24th International Conference on Rewriting Techniques and Applications (RTA\u201913)."},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2014.36"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_3_2_2_10_1","unstructured":"K. Batz B. L. Kaminski J.-P. Katoen and C. Matheja. 2018. How long O Bayesian network will I sample thee? A program analysis perspective on expected sampling times. ArXiv e-prints (Feb. 2018). arXiv: cs.PL\/1802.10433 To appear at ESOP\u201918.  K. Batz B. L. Kaminski J.-P. Katoen and C. Matheja. 2018. How long O Bayesian network will I sample thee? A program analysis perspective on expected sampling times. ArXiv e-prints (Feb. 2018). arXiv: cs.PL\/1802.10433 To appear at ESOP\u201918."},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.10.022"},{"key":"e_1_3_2_2_12_1","volume-title":"Conf. (LPAR\u201910)","author":"Blanc R\u00e9gis","year":"2010","unstructured":"R\u00e9gis Blanc , Thomas A. Henzinger , Thibaud Hottelier , and Laura Kov\u00e1cs . 2010 . ABC: Algebraic Bound Computation for Loops. In Logic for Prog., AI., and Reasoning - 16th Int . Conf. (LPAR\u201910) . R\u00e9gis Blanc, Thomas A. Henzinger, Thibaud Hottelier, and Laura Kov\u00e1cs. 2010. ABC: Algebraic Bound Computation for Loops. In Logic for Prog., AI., and Reasoning - 16th Int. Conf. (LPAR\u201910)."},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594329"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2014.06.005"},{"key":"e_1_3_2_2_15_1","volume-title":"Alternating Runtime and Size Complexity Analysis of Integer Programs. In 20th Int. Conf. on Tools and Alg. for the Constr. and Anal. of Systems (TACAS\u201914)","author":"Brockschmidt Marc","year":"2014","unstructured":"Marc Brockschmidt , Fabian Emmes , Stephan Falke , Carsten Fuhs , and J\u00fcrgen Giesl . 2014 . Alternating Runtime and Size Complexity Analysis of Integer Programs. In 20th Int. Conf. on Tools and Alg. for the Constr. and Anal. of Systems (TACAS\u201914) . Marc Brockschmidt, Fabian Emmes, Stephan Falke, Carsten Fuhs, and J\u00fcrgen Giesl. 2014. Alternating Runtime and Size Complexity Analysis of Integer Programs. In 20th Int. Conf. on Tools and Alg. for the Constr. and Anal. of Systems (TACAS\u201914)."},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594301"},{"key":"e_1_3_2_2_17_1","volume-title":"Automated Resource Analysis with Coq Proof Objects. In 29th International Conference on Computer-Aided Verification (CAV\u201917)","author":"Carbonneaux Quentin","year":"2017","unstructured":"Quentin Carbonneaux , Jan Hoffmann , Thomas Reps , and Zhong Shao . 2017 . Automated Resource Analysis with Coq Proof Objects. In 29th International Conference on Computer-Aided Verification (CAV\u201917) . Quentin Carbonneaux, Jan Hoffmann, Thomas Reps, and Zhong Shao. 2017. Automated Resource Analysis with Coq Proof Objects. In 29th International Conference on Computer-Aided Verification (CAV\u201917)."},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737955"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/11526841_9"},{"key":"e_1_3_2_2_20_1","volume-title":"Segment Abstraction for WorstCase Execution Time Analysis. In 24th European Symposium on Programming (ESOP\u201915)","author":"Cern\u00fd Pavol","year":"2015","unstructured":"Pavol Cern\u00fd , Thomas A. Henzinger , Laura Kov\u00e1cs , Arjun Radhakrishna , and Jakob Zwirchmayr . 2015 . Segment Abstraction for WorstCase Execution Time Analysis. In 24th European Symposium on Programming (ESOP\u201915) . Pavol Cern\u00fd, Thomas A. Henzinger, Laura Kov\u00e1cs, Arjun Radhakrishna, and Jakob Zwirchmayr. 2015. Segment Abstraction for WorstCase Execution Time Analysis. In 24th European Symposium on Programming (ESOP\u201915)."},{"key":"e_1_3_2_2_21_1","volume-title":"Computer-Aided Verification (CAV\u201913) (Lecture Notes in Computer Science)","author":"Chakarov Aleksandar","unstructured":"Aleksandar Chakarov and Sriram Sankaranarayanan . 2013. Probabilistic Program Analysis using Martingales . In Computer-Aided Verification (CAV\u201913) (Lecture Notes in Computer Science) , Vol. 8044 . SpringerVerlag . Aleksandar Chakarov and Sriram Sankaranarayanan. 2013. Probabilistic Program Analysis using Martingales. In Computer-Aided Verification (CAV\u201913) (Lecture Notes in Computer Science), Vol. 8044. SpringerVerlag."},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10936-7_6"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"crossref","unstructured":"Arthur Chargu\u00e9raud and Fran\u00e7ois Pottier. 2015. Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation. In Interactive Theorem Proving -6th International Conference (ITP\u201915).  Arthur Chargu\u00e9raud and Fran\u00e7ois Pottier. 2015. Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation. In Interactive Theorem Proving -6th International Conference (ITP\u201915).","DOI":"10.1007\/978-3-319-22102-1_9"},{"key":"e_1_3_2_2_24_1","volume-title":"28th International Conference (CAV\u201916)","author":"Chatterjee Krishnendu","year":"2016","unstructured":"Krishnendu Chatterjee , Hongfei Fu , and Amir Kafshdar Goharshady . 2016 . Termination Analysis of Probabilistic Programs Through Positivstellensatz\u2019s. In Computer Aided Verification - 28th International Conference (CAV\u201916) . Krishnendu Chatterjee, Hongfei Fu, and Amir Kafshdar Goharshady. 2016. Termination Analysis of Probabilistic Programs Through Positivstellensatz\u2019s. In Computer Aided Verification - 28th International Conference (CAV\u201916)."},{"key":"e_1_3_2_2_25_1","volume-title":"Conf. (CAV\u201917)","author":"Chatterjee Krishnendu","year":"2017","unstructured":"Krishnendu Chatterjee , Hongfei Fu , and Amir Kafshdar Goharshady . 2017 . Non-polynomial Worst-Case Analysis of Recursive Programs. In Computer Aided Verification - 29th Int . Conf. (CAV\u201917) . Krishnendu Chatterjee, Hongfei Fu, and Amir Kafshdar Goharshady. 2017. Non-polynomial Worst-Case Analysis of Recursive Programs. In Computer Aided Verification - 29th Int. Conf. (CAV\u201917)."},{"key":"e_1_3_2_2_26_1","volume-title":"Conf. (CAV\u201917)","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 Int . Conf. (CAV\u201917) . Krishnendu Chatterjee, Hongfei Fu, and Aniket Murhekar. 2017. Automated Recurrence Analysis for Almost-Linear Expected-Runtime Bounds. In Computer Aided Verification - 29th Int. Conf. (CAV\u201917)."},{"key":"e_1_3_2_2_27_1","volume-title":"Refinement Types for Incremental Computational Complexity. In 24th European Symposium on Programming (ESOP\u201915)","author":"\u00c7i\u00e7ek Ezgi","unstructured":"Ezgi \u00c7i\u00e7ek , Deepak Garg , and Umut A. Acar . 2015 . Refinement Types for Incremental Computational Complexity. In 24th European Symposium on Programming (ESOP\u201915) . Ezgi \u00c7i\u00e7ek, Deepak Garg, and Umut A. Acar. 2015. Refinement Types for Incremental Computational Complexity. In 24th European Symposium on Programming (ESOP\u201915)."},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_9"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325716"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328457"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784749"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"crossref","unstructured":"D. Dubhashi and A. Panconesi. 2009. Concentration of Measure for the Analysis of Randomized Algorithms. Cambridge University Press (2009).   D. Dubhashi and A. Panconesi. 2009. Concentration of Measure for the Analysis of Randomized Algorithms. Cambridge University Press (2009).","DOI":"10.1017\/CBO9780511581274"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.39"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677001"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90145-R"},{"key":"e_1_3_2_2_36_1","volume-title":"Programming Languages and Systems - 12th Asian Symposiu (APLAS\u201914).","author":"Flores-Montoya Antonio","unstructured":"Antonio Flores-Montoya and Reiner H\u00e4hnle . 2014. Resource Analysis of Complex Programs with Cost Equations . In Programming Languages and Systems - 12th Asian Symposiu (APLAS\u201914). Antonio Flores-Montoya and Reiner H\u00e4hnle. 2014. Resource Analysis of Complex Programs with Cost Equations. In Programming Languages and Systems - 12th Asian Symposiu (APLAS\u201914)."},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_37"},{"key":"e_1_3_2_2_38_1","volume-title":"CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I.","author":"Gehr Timon","unstructured":"Timon Gehr , Sasa Misailovic , and Martin T. Vechev . 2016. PSI: Exact Symbolic Inference for Probabilistic Programs. In Computer Aided Verification - 28th International Conference , CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I. Timon Gehr, Sasa Misailovic, and Martin T. Vechev. 2016. PSI: Exact Symbolic Inference for Probabilistic Programs. In Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I."},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2338965.2336773"},{"key":"e_1_3_2_2_40_1","volume-title":"Probabilistic machine learning and artificial intelligence. Nature 521","author":"Ghahramani Zoubin","year":"2015","unstructured":"Zoubin Ghahramani . 2015. Probabilistic machine learning and artificial intelligence. Nature 521 ( 2015 ). Zoubin Ghahramani. 2015. Probabilistic machine learning and artificial intelligence. Nature 521 (2015)."},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2593882.2593900"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.peva.2013.11.004"},{"key":"e_1_3_2_2_43_1","unstructured":"G. Grimmett and D. Stirzaker. 1992. Probability and Random Processes. Oxford University Press.  G. Grimmett and D. Stirzaker. 1992. Probability and Random Processes. Oxford University Press."},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/507635.507666"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480898"},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.5555\/2028067.2028100"},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926427"},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2362389.2362393"},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009842"},{"key":"e_1_3_2_2_50_1","volume-title":"Amortized Resource Analysis with Polynomial Potential. In 19th European Symposium on Programming (ESOP\u201910)","author":"Hoffmann Jan","year":"2010","unstructured":"Jan Hoffmann and Martin Hofmann . 2010 . Amortized Resource Analysis with Polynomial Potential. In 19th European Symposium on Programming (ESOP\u201910) . Jan Hoffmann and Martin Hofmann. 2010. Amortized Resource Analysis with Polynomial Potential. In 19th European Symposium on Programming (ESOP\u201910)."},{"key":"e_1_3_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_3"},{"key":"e_1_3_2_2_52_1","doi-asserted-by":"crossref","unstructured":"Jan Hoffmann and Zhong Shao. 2015. Type-Based Amortized Resource Analysis with Integers and Arrays. J. Funct. Program. (2015).  Jan Hoffmann and Zhong Shao. 2015. Type-Based Amortized Resource Analysis with Integers and Arrays. J. Funct. Program. (2015).","DOI":"10.1017\/S0956796815000192"},{"key":"e_1_3_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604148"},{"key":"e_1_3_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_3"},{"key":"e_1_3_2_2_55_1","doi-asserted-by":"crossref","unstructured":"Martin Hofmann and Georg Moser. 2014. Amortised Resource Analysis and Typed Polynomial Interpretations. In Rewriting and Typed Lambda Calculi (RTA-TLCA;14).  Martin Hofmann and Georg Moser. 2014. Amortised Resource Analysis and Typed Polynomial Interpretations. In Rewriting and Typed Lambda Calculi (RTA-TLCA;14).","DOI":"10.1007\/978-3-319-08918-8_19"},{"key":"e_1_3_2_2_56_1","volume-title":"Multivariate Amortised Resource Analysis for Term Rewrite Systems. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA\u201915)","author":"Hofmann Martin","year":"2015","unstructured":"Martin Hofmann and Georg Moser . 2015 . Multivariate Amortised Resource Analysis for Term Rewrite Systems. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA\u201915) . Martin Hofmann and Georg Moser. 2015. Multivariate Amortised Resource Analysis for Term Rewrite Systems. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA\u201915)."},{"key":"e_1_3_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_32"},{"key":"e_1_3_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_52"},{"key":"e_1_3_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706327"},{"key":"e_1_3_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_23"},{"key":"e_1_3_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"e_1_3_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934574"},{"key":"e_1_3_2_2_63_1","volume-title":"Morgan","author":"Katoen Joost-Pieter","year":"2010","unstructured":"Joost-Pieter Katoen , Annabelle McIver , Larissa Meinicke , and Carroll C . Morgan . 2010 . Linear-Invariant Generation for Probabilistic Programs: - Automated Support for Proof-Based Methods. In Static Analysis - 17th International Symposium (SAS\u2019 10). Joost-Pieter Katoen, Annabelle McIver, Larissa Meinicke, and Carroll C. Morgan. 2010. Linear-Invariant Generation for Probabilistic Programs: - Automated Support for Proof-Based Methods. In Static Analysis - 17th International Symposium (SAS\u201910)."},{"key":"e_1_3_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062373"},{"key":"e_1_3_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"e_1_3_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.22"},{"key":"e_1_3_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429090"},{"key":"e_1_3_2_2_68_1","volume-title":"Arrays and References in Resource Aware ML. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD\u201917)","author":"Lichtman Benjamin","year":"2017","unstructured":"Benjamin Lichtman and Jan Hoffmann . 2017 . Arrays and References in Resource Aware ML. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD\u201917) . Benjamin Lichtman and Jan Hoffmann. 2017. Arrays and References in Resource Aware ML. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD\u201917)."},{"key":"e_1_3_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009874"},{"key":"e_1_3_2_2_70_1","volume-title":"Refinement and Proof For Probabilistic Systems (Monographs in Computer Science)","author":"McIver Annabelle","unstructured":"Annabelle McIver and Carroll Morgan . 2004. Abstraction , Refinement and Proof For Probabilistic Systems (Monographs in Computer Science) . Springer Verlag . Annabelle McIver and Carroll Morgan. 2004. Abstraction, Refinement and Proof For Probabilistic Systems (Monographs in Computer Science). Springer Verlag."},{"key":"e_1_3_2_2_71_1","volume-title":"10th European Symposium on Programming (ESOP\u201901)","author":"Monniaux David","year":"2001","unstructured":"David Monniaux . 2001 . Backwards Abstract Interpretation of Probabilistic Programs. In Programming Languages and Systems , 10th European Symposium on Programming (ESOP\u201901) . David Monniaux. 2001. Backwards Abstract Interpretation of Probabilistic Programs. In Programming Languages and Systems, 10th European Symposium on Programming (ESOP\u201901)."},{"key":"e_1_3_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2005.02.008"},{"key":"e_1_3_2_2_73_1","volume-title":"Bounded Expectations: Resource Analysis for Probabilistic Programs. CoRR abs\/1711.08847","author":"Ngo Van Chan","year":"2017","unstructured":"Van Chan Ngo , Quentin Carbonneaux , and Jan Hoffmann . 2017 . Bounded Expectations: Resource Analysis for Probabilistic Programs. CoRR abs\/1711.08847 (2017). arXiv: 1711.08847 http:\/\/arxiv.org\/abs\/ 1711.08847 Van Chan Ngo, Quentin Carbonneaux, and Jan Hoffmann. 2017. Bounded Expectations: Resource Analysis for Probabilistic Programs. CoRR abs\/1711.08847 (2017). arXiv: 1711.08847 http:\/\/arxiv.org\/abs\/ 1711.08847"},{"key":"e_1_3_2_2_74_1","volume-title":"Verifying and Synthesizing Constant-Resource Implementations with Types. In 38th IEEE Symposium on Security and Privacy (S&P \u201917)","author":"Ngo Van Chan","year":"2017","unstructured":"Van Chan Ngo , Mario Dehesa-Azuara , Matthew Fredrikson , and Jan Hoffmann . 2017 . Verifying and Synthesizing Constant-Resource Implementations with Types. In 38th IEEE Symposium on Security and Privacy (S&P \u201917) . Van Chan Ngo, Mario Dehesa-Azuara, Matthew Fredrikson, and Jan Hoffmann. 2017. Verifying and Synthesizing Constant-Resource Implementations with Types. In 38th IEEE Symposium on Security and Privacy (S&P \u201917)."},{"key":"e_1_3_2_2_75_1","volume-title":"PSCV: A Runtime Verification Tool for Probabilistic SystemC Models. J. of Software: Evolution and Process","author":"Ngo Van Chan","year":"2018","unstructured":"Van Chan Ngo and Axel Legay . 2018 . PSCV: A Runtime Verification Tool for Probabilistic SystemC Models. J. of Software: Evolution and Process (2018). Van Chan Ngo and Axel Legay. 2018. PSCV: A Runtime Verification Tool for Probabilistic SystemC Models. J. of Software: Evolution and Process (2018)."},{"key":"e_1_3_2_2_76_1","volume-title":"PSCV: A Runtime Verification Tool for Probabilistic SystemC Models. In 28th International Conference on Computer Aided Verification (CAV\u201916)","author":"Ngo Van Chan","year":"2016","unstructured":"Van Chan Ngo , Axel Legay , and Vania Joloboff . 2016 . PSCV: A Runtime Verification Tool for Probabilistic SystemC Models. In 28th International Conference on Computer Aided Verification (CAV\u201916) . Van Chan Ngo, Axel Legay, and Vania Joloboff. 2016. PSCV: A Runtime Verification Tool for Probabilistic SystemC Models. In 28th International Conference on Computer Aided Verification (CAV\u201916)."},{"key":"e_1_3_2_2_77_1","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.2016.24"},{"key":"e_1_3_2_2_78_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90029-3"},{"key":"e_1_3_2_2_79_1","volume-title":"Interactive Theorem Proving - 6th International Conference (ITP\u201915).","author":"Nipkow Tobias","unstructured":"Tobias Nipkow . 2015. Amortized Complexity Verified . In Interactive Theorem Proving - 6th International Conference (ITP\u201915). Tobias Nipkow. 2015. Amortized Complexity Verified. In Interactive Theorem Proving - 6th International Conference (ITP\u201915)."},{"key":"e_1_3_2_2_80_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-013-9277-6"},{"key":"e_1_3_2_2_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935317"},{"key":"e_1_3_2_2_82_1","unstructured":"Avi Pfeffer. 2016. Practical Probabilistic Programming. Manning. https: \/\/books.google.com\/books?id=qyfksgEACAAJ   Avi Pfeffer. 2016. Practical Probabilistic Programming. Manning. https: \/\/books.google.com\/books?id=qyfksgEACAAJ"},{"key":"e_1_3_2_2_83_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462179"},{"key":"e_1_3_2_2_84_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364575"},{"key":"e_1_3_2_2_85_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_50"},{"key":"e_1_3_2_2_86_1","unstructured":"The CLP Team. 2018. CLP. https:\/\/projects.coin-or.org\/Clp . (2018).  The CLP Team. 2018. CLP. https:\/\/projects.coin-or.org\/Clp . (2018)."},{"key":"e_1_3_2_2_88_1","volume-title":"Type-Based Allocation Analysis for Co-recursion in Lazy Functional Languages. In 24th European Symposium on Programming (ESOP\u201915)","author":"Vasconcelos Pedro B.","year":"2015","unstructured":"Pedro B. Vasconcelos , Steffen Jost , M\u00e1rio Florido , and Kevin Hammond . 2015 . Type-Based Allocation Analysis for Co-recursion in Lazy Functional Languages. In 24th European Symposium on Programming (ESOP\u201915) . Pedro B. Vasconcelos, Steffen Jost, M\u00e1rio Florido, and Kevin Hammond. 2015. Type-Based Allocation Analysis for Co-recursion in Lazy Functional Languages. In 24th European Symposium on Programming (ESOP\u201915)."},{"key":"e_1_3_2_2_89_1","volume-title":"Bound Analysis of Imperative Programs with the Size-change Abstraction. In 18th Int. Static Analysis Symp. (SAS\u201911)","author":"Zuleger Florian","year":"2011","unstructured":"Florian Zuleger , Moritz Sinn , Sumit Gulwani , and Helmut Veith . 2011 . Bound Analysis of Imperative Programs with the Size-change Abstraction. In 18th Int. Static Analysis Symp. (SAS\u201911) . Florian Zuleger, Moritz Sinn, Sumit Gulwani, and Helmut Veith. 2011. Bound Analysis of Imperative Programs with the Size-change Abstraction. In 18th Int. Static Analysis Symp. (SAS\u201911)."},{"key":"e_1_3_2_2_90_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009858"}],"event":{"name":"PLDI '18: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Philadelphia PA USA","acronym":"PLDI '18","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3192366.3192394","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3192366.3192394","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3192366.3192394","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:07:53Z","timestamp":1750198073000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3192366.3192394"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,6,11]]},"references-count":88,"alternative-id":["10.1145\/3192366.3192394","10.1145\/3192366"],"URL":"https:\/\/doi.org\/10.1145\/3192366.3192394","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3296979.3192394","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2018,6,11]]},"assertion":[{"value":"2018-06-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}