{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:16:07Z","timestamp":1784837767488,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":78,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,6,11]],"date-time":"2020-06-11T00:00:00Z","timestamp":1591833600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100012659","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61802254"],"award-info":[{"award-number":["61802254"]}],"id":[{"id":"10.13039\/501100012659","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"}]},{"name":"\u00d6sterreichischen Akademie der Wissenschaften","award":["DOC 24956"],"award-info":[{"award-number":["DOC 24956"]}]},{"DOI":"10.13039\/100005801","name":"Facebook","doi-asserted-by":"publisher","award":["PhD Fellowship Program"],"award-info":[{"award-number":["PhD Fellowship Program"]}],"id":[{"id":"10.13039\/100005801","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["NFN S11407-N23 (RiSE\/SHiNE)"],"award-info":[{"award-number":["NFN S11407-N23 (RiSE\/SHiNE)"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,6,11]]},"DOI":"10.1145\/3385412.3385969","type":"proceedings-article","created":{"date-parts":[[2020,6,7]],"date-time":"2020-06-07T01:40:10Z","timestamp":1591494010000},"page":"672-687","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":38,"title":["Polynomial invariant generation for non-deterministic recursive programs"],"prefix":"10.1145","author":[{"given":"Krishnendu","family":"Chatterjee","sequence":"first","affiliation":[{"name":"IST Austria, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hongfei","family":"Fu","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Amir Kafshdar","family":"Goharshady","sequence":"additional","affiliation":[{"name":"IST Austria, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ehsan Kafshdar","family":"Goharshady","sequence":"additional","affiliation":[{"name":"Ferdowsi University of Mashhad, Iran"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2020,6,11]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"crossref","unstructured":"Assal\u00e9 Adj\u00e9 Pierre-Lo\u00efc Garoche and Victor Magron. 2015. Propertybased polynomial invariant generation using sums-of-squares optimization. In SAS. 235\u2013251.","DOI":"10.1007\/978-3-662-48288-9_14"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Assal\u00e9 Adj\u00e9 St\u00e9phane Gaubert and Eric Goubault. 2010. Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis. In ESOP. 23\u201342.","DOI":"10.1007\/978-3-642-11957-6_3"},{"key":"e_1_3_2_1_3_1","volume-title":"Ufo: A framework for abstraction-and interpolation-based software verification","author":"Albarghouthi Aws","year":"2012","unstructured":"Aws Albarghouthi, Yi Li, Arie Gurfinkel, and Marsha Chechik. 2012. Ufo: A framework for abstraction-and interpolation-based software verification. In CAV. Springer, 672\u2013678."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/800028.808479"},{"key":"e_1_3_2_1_5_1","volume-title":"Predicate abstraction for reachability analysis of hybrid systems. ACM transactions on embedded computing systems (TECS) 5, 1","author":"Alur Rajeev","year":"2006","unstructured":"Rajeev Alur, Thao Dang, and Franjo Ivan\u010di\u0107. 2006. Predicate abstraction for reachability analysis of hybrid systems. ACM transactions on embedded computing systems (TECS) 5, 1 (2006), 152\u2013199."},{"key":"e_1_3_2_1_6_1","volume-title":"Andersen","author":"Andersen Erling D.","year":"2018","unstructured":"Erling D. Andersen and Knud D. Andersen. 2018. MOSEK Optimization Suite. (2018)."},{"key":"e_1_3_2_1_7_1","unstructured":"https:\/\/www.mosek.com\/"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Roberto Bagnara Enric Rodr\u00edguez-Carbonell and Enea Zaffanella. 2005. Generation of Basic Semi-algebraic Invariants Using Convex Polyhedra. In SAS. 19\u201334.","DOI":"10.1007\/11547662_4"},{"key":"e_1_3_2_1_9_1","volume-title":"Algorithms in real algebraic geometry","author":"Basu Saugata","unstructured":"Saugata Basu, Richard Pollack, and Marie-Fran\u00e7oise Coste-Roy. 2007. Algorithms in real algebraic geometry. Springer."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1093\/imamci\/dnv003"},{"key":"e_1_3_2_1_11_1","volume-title":"Linear ranking with reachability","author":"Bradley Aaron R","unstructured":"Aaron R Bradley, Zohar Manna, and Henny B Sipma. 2005. Linear ranking with reachability. In CAV. Springer, 491\u2013504."},{"key":"e_1_3_2_1_12_1","unstructured":"Christopher W Brown. 2019. QEPCAD - Quantifier Elimination by Partial Cylindrical Algebraic Decomposition. (2019)."},{"key":"e_1_3_2_1_13_1","unstructured":"https:\/\/www. usna.edu\/CS\/qepcadweb\/B\/QEPCAD.html"},{"key":"e_1_3_2_1_14_1","volume-title":"Probabilistic program analysis with martingales","author":"Chakarov Aleksandar","unstructured":"Aleksandar Chakarov and Sriram Sankaranarayanan. 2013. Probabilistic program analysis with martingales. In CAV. Springer, 511\u2013526."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","unstructured":"Aleksandar Chakarov and Sriram Sankaranarayanan. 2014. Expectation Invariants for Probabilistic Program Loops as Fixed Points. In SAS. 85\u2013100.","DOI":"10.1007\/978-3-319-10936-7_6"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Krishnendu Chatterjee Hongfei Fu and Amir Kafshdar Goharshady. 2016. Termination Analysis of Probabilistic Programs Through Positivstellensatz\u2019s. In CAV. 3\u201322.","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Krishnendu Chatterjee Hongfei Fu and Amir Kafshdar Goharshady. 2017. Non-polynomial Worst-Case Analysis of Recursive Programs. In CAV. 41\u201363.","DOI":"10.1007\/978-3-319-63390-9_3"},{"key":"e_1_3_2_1_18_1","volume-title":"Amir Kafshdar Goharshady, and Ehsan Kafshdar Goharshady","author":"Chatterjee Krishnendu","year":"2020","unstructured":"Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, and Ehsan Kafshdar Goharshady. 2020. Polynomial invariant generation for non-deterministic recursive programs. arXiv preprint arXiv:1902.04373 (2020)."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Krishnendu Chatterjee Petr Novotn\u00fd and Dorde Zikelic. 2017. Stochastic invariants for probabilistic termination. In POPL. 145\u2013160.","DOI":"10.1145\/3009837.3009873"},{"key":"e_1_3_2_1_20_1","volume-title":"Discovering non-linear ranking functions by solving semialgebraic systems","author":"Chen Yinghua","unstructured":"Yinghua Chen, Bican Xia, Lu Yang, Naijun Zhan, and Chaochen Zhou. 2007. Discovering non-linear ranking functions by solving semialgebraic systems. In ICTAC. Springer, 34\u201349."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Yu-Fang Chen Chih-Duo Hong Bow-Yaw Wang and Lijun Zhang. 2015. Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation. In CAV. 658\u2013674.","DOI":"10.1007\/978-3-319-21690-4_44"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Michael Col\u00f3n Sriram Sankaranarayanan and Henny Sipma. 2003. Linear Invariant Generation Using Non-linear Constraint Solving. In CAV. 420\u2013432.","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"e_1_3_2_1_23_1","volume-title":"Synthesis of linear ranking functions","author":"Col\u00f3n Michael A","unstructured":"Michael A Col\u00f3n and Henny B Sipma. 2001. Synthesis of linear ranking functions. In TACAS. Springer, 67\u201381."},{"key":"e_1_3_2_1_24_1","volume-title":"Introduction to algorithms","author":"Cormen Thomas H","unstructured":"Thomas H Cormen, Charles E Leiserson, Ronald L Rivest, and Clifford Stein. 2009. Introduction to algorithms. MIT press."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Patrick Cousot. 2005. Proving Program Invariance and Termination by Parametric Abstraction Lagrangian Relaxation and Semidefinite Programming. In VMCAI. 1\u201324.","DOI":"10.1007\/978-3-540-30579-8_1"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"crossref","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. ACM 238\u2013252.","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Patrick Cousot Radhia Cousot J\u00e9r\u00f4me Feret Laurent Mauborgne Antoine Min\u00e9 David Monniaux and Xavier Rival. 2005. The ASTRE\u00c9 Analyzer. In ESOP. 21\u201330.","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","unstructured":"Patrick Cousot and Nicolas Halbwachs. 1978. Automatic discovery of linear restraints among variables of a program. In POPL. ACM 84\u201396.","DOI":"10.1145\/512760.512770"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"crossref","unstructured":"Christoph Csallner Nikolai Tillmann and Yannis Smaragdakis. 2008. DySy: dynamic symbolic execution for invariant inference. In ICSE. 281\u2013290.","DOI":"10.1145\/1368088.1368127"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"crossref","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An efficient SMT solver. In TACAS. 337\u2013340.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"crossref","unstructured":"Steven de Oliveira Saddek Bensalem and Virgile Prevosto. 2016. Polynomial Invariants by Linear Algebra. In ATVA. 479\u2013494.","DOI":"10.1007\/978-3-319-46520-3_30"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Isil Dillig Thomas Dillig Boyang Li and Ken McMillan. 2013. Inductive invariant generation via abductive inference. In OOPSLA.","DOI":"10.1145\/2509136.2509511"},{"key":"e_1_3_2_1_33_1","volume-title":"McMillan","author":"Dillig Isil","year":"2013","unstructured":"Isil Dillig, Thomas Dillig, Boyang Li, and Kenneth L. McMillan. 2013. Inductive invariant generation via abductive inference. In OOPSLA. 443\u2013456."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"crossref","unstructured":"Azadeh Farzan and Zachary Kincaid. 2015. Compositional Recurrence Analysis. In FMCAD. 57\u201364.","DOI":"10.1109\/FMCAD.2015.7542253"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"crossref","unstructured":"Yijun Feng Lijun Zhang David N. Jansen Naijun Zhan and Bican Xia. 2017. Finding Polynomial Loop Invariants for Probabilistic Programs. In ATVA. 400\u2013416.","DOI":"10.1007\/978-3-319-68167-2_26"},{"key":"e_1_3_2_1_36_1","volume-title":"Program Verification","author":"Floyd Robert W","unstructured":"Robert W Floyd. 1993. Assigning meanings to programs. In Program Verification. Springer, 65\u201381."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3186898"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"crossref","unstructured":"Pranav Garg Daniel Neider P. Madhusudan and Dan Roth. 2016. Learning invariants using decision trees and implication counterexamples. In POPL. 499\u2013512.","DOI":"10.1145\/2837614.2837664"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"crossref","unstructured":"Roberto Giacobazzi and Francesco Ranzato. 1997. Completeness in abstract interpretation: A domain perspective. In AMAST. 231\u2013245.","DOI":"10.1007\/BFb0000474"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(88)80005-1"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"crossref","unstructured":"Sumit Gulwani Saurabh Srivastava and Ramarathnam Venkatesan. 2009. Constraint-Based Invariant Inference over Predicate Abstraction. In VMCAI. 120\u2013135.","DOI":"10.1007\/978-3-540-93900-9_13"},{"key":"e_1_3_2_1_42_1","volume-title":"Navas","author":"Gurfinkel Arie","year":"2015","unstructured":"Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A. Navas. 2015. The SeaHorn Verification Framework. In CAV. 343\u2013361."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008678014487"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"crossref","unstructured":"Matthias Heizmann J\u00fcrgen Christ Daniel Dietsch Evren Ermis Jochen Hoenicke Markus Lindenmann Alexander Nutz Christian Schilling and Andreas Podelski. 2013. Ultimate Automizer with SMTInterpol. In TACAS. 641\u2013643.","DOI":"10.1007\/978-3-642-36742-7_53"},{"key":"e_1_3_2_1_45_1","unstructured":"Thomas Henzinger and Pei-Hsin Ho. 1994. Model checking strategies for linear hybrid systems. (1994)."},{"key":"e_1_3_2_1_46_1","unstructured":"Hoon Hong. 1991. Comparison of several decision algorithms for the existential theory of the reals. (1991)."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"crossref","unstructured":"Ehud Hrushovski Jo\u00ebl Ouaknine Amaury Pouly and James Worrell. 2018. Polynomial Invariants for Affine Programs. In LICS. 530\u2013539.","DOI":"10.1145\/3209108.3209142"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"crossref","unstructured":"Mingzhang Huang Hongfei Fu Krishnendu Chatterjee and Amir Kafshdar Goharshady. 2019. Modular verification for almost-sure termination of probabilistic programs. In OOPSLA. 1\u201329.","DOI":"10.1145\/3360555"},{"key":"e_1_3_2_1_49_1","volume-title":"ISSAC. 221\u2013228. PLDI \u201920, June 15\u201320","author":"Humenberger Andreas","year":"2020","unstructured":"Andreas Humenberger, Maximilian Jaroschek, and Laura Kov\u00e1cs. 2017. Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences. In ISSAC. 221\u2013228. PLDI \u201920, June 15\u201320, 2020, London, UK K. Chatterjee, H. Fu, A.K. Goharshady, and E.K. Goharshady"},{"key":"e_1_3_2_1_50_1","unstructured":"Deepak Kapur. 2004. Automatically generating loop invariants using quantifier elimination preliminary report. In ACA."},{"key":"e_1_3_2_1_51_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 SAS. 390\u2013406."},{"key":"e_1_3_2_1_52_1","volume-title":"Ashkan Forouhi Boroujeni, and Thomas W. Reps","author":"Kincaid Zachary","year":"2017","unstructured":"Zachary Kincaid, Jason Breck, Ashkan Forouhi Boroujeni, and Thomas W. Reps. 2017. Compositional recurrence analysis revisited. In PLDI. 248\u2013262."},{"key":"e_1_3_2_1_53_1","first-page":"1","article-title":"Non-linear reasoning for invariant synthesis","volume":"54","author":"Kincaid Zachary","year":"2018","unstructured":"Zachary Kincaid, John Cyphert, Jason Breck, and Thomas W. Reps. 2018. Non-linear reasoning for invariant synthesis. In POPL. 54:1\u2013 54:33.","journal-title":"POPL."},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11704-014-3150-6"},{"key":"e_1_3_2_1_55_1","volume-title":"Temporal verification of reactive systems: Safety","author":"Manna Zohar","unstructured":"Zohar Manna and Amir Pnueli. 1995. Temporal verification of reactive systems: Safety. Springer."},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"crossref","unstructured":"Kenneth L. McMillan. 2008. Quantified Invariant Generation Using an Interpolating Saturation Prover. In TACAS. 413\u2013427.","DOI":"10.1007\/978-3-540-78800-3_31"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2004.05.004"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"crossref","unstructured":"Van Chan Ngo Quentin Carbonneaux and Jan Hoffmann. 2018. Bounded expectations: resource analysis for probabilistic programs. In PLDI. ACM 496\u2013512.","DOI":"10.1145\/3192366.3192394"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"crossref","unstructured":"ThanhVu Nguyen Deepak Kapur Westley Weimer and Stephanie Forrest. 2012. Using dynamic analysis to discover polynomial and array invariants. In ICSE. 683\u2013693.","DOI":"10.1109\/ICSE.2012.6227149"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1109\/LCSYS.2019.2916256"},{"key":"e_1_3_2_1_61_1","volume-title":"Ivy: safety verification by interactive generalization. PLDI","author":"Padon Oded","year":"2016","unstructured":"Oded Padon, Kenneth L McMillan, Aurojit Panda, Mooly Sagiv, and Sharon Shoham. 2016. Ivy: safety verification by interactive generalization. PLDI (2016), 614\u2013630."},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1512\/iumj.1993.42.42045"},{"key":"e_1_3_2_1_63_1","volume-title":"https: \/\/www.wolfram.com\/mathematica","author":"Research Wolfram","year":"2019","unstructured":"Wolfram Research. 2019. Mathematica, Version 12.0. (2019). https: \/\/www.wolfram.com\/mathematica"},{"key":"e_1_3_2_1_64_1","unstructured":"Enric Rodr\u00edguez-Carbonell. 2018. Some programs that need polynomial invariants in order to be verified. (2018). http:\/\/www.cs.upc.edu\/ ~erodri\/webpage\/polynomial_invariants\/list.html"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"crossref","unstructured":"Enric Rodr\u00edguez-Carbonell and Deepak Kapur. 2004. Automatic generation of polynomial loop invariants: Algebraic foundations. In ISSAC. ACM 266\u2013273.","DOI":"10.1145\/1005285.1005324"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.03.003"},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"crossref","unstructured":"Sriram Sankaranarayanan. 2011. Automatic abstraction of non-linear systems using change of bases transformations. In HSCC. 143\u2013152.","DOI":"10.1145\/1967701.1967723"},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"crossref","unstructured":"Sriram Sankaranarayanan Henny Sipma and Zohar Manna. 2004. Non-linear loop invariant generation using Gr\u00f6bner bases. In POPL. 318\u2013329.","DOI":"10.1145\/982962.964028"},{"key":"e_1_3_2_1_69_1","volume-title":"Constraint-based linear-relations analysis","author":"Sankaranarayanan Sriram","unstructured":"Sriram Sankaranarayanan, Henny B Sipma, and Zohar Manna. 2004. Constraint-based linear-relations analysis. In SAS. Springer, 53\u201368."},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0248-5"},{"key":"e_1_3_2_1_71_1","doi-asserted-by":"crossref","unstructured":"Gagandeep Singh Markus P\u00fcschel and Martin Vechev. 2015. Making numerical program analysis fast. In PLDI. ACM 303\u2013313.","DOI":"10.1145\/2737924.2738000"},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"crossref","unstructured":"Gagandeep Singh Markus P\u00fcschel and Martin Vechev. 2017. Fast polyhedra abstract domain. In POPL. 46\u201359.","DOI":"10.1145\/3009837.3009885"},{"key":"e_1_3_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01362149"},{"key":"e_1_3_2_1_74_1","volume-title":"Solving systems of polynomial equations","author":"Sturmfels Bernd","unstructured":"Bernd Sturmfels. 2002. Solving systems of polynomial equations. American Mathematical Society."},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1997.2697"},{"key":"e_1_3_2_1_77_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. In PLDI. 204\u2013220."},{"key":"e_1_3_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11704-009-0074-7"},{"key":"e_1_3_2_1_79_1","unstructured":"Ian En-Hsu Yen Kai Zhong Cho-Jui Hsieh Pradeep K Ravikumar and Inderjit S Dhillon. 2015. Sparse linear programming via primal and dual augmented coordinate descent. In NIPS. 2368\u20132376."}],"event":{"name":"PLDI '20: 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation","location":"London UK","acronym":"PLDI '20","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3385412.3385969","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3385412.3385969","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:14Z","timestamp":1750200074000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3385412.3385969"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6,11]]},"references-count":78,"alternative-id":["10.1145\/3385412.3385969","10.1145\/3385412"],"URL":"https:\/\/doi.org\/10.1145\/3385412.3385969","relation":{},"subject":[],"published":{"date-parts":[[2020,6,11]]},"assertion":[{"value":"2020-06-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}