{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:12:17Z","timestamp":1784837537641,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":82,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,6,18]],"date-time":"2021-06-18T00:00:00Z","timestamp":1623974400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100003816","name":"Huawei Technologies","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100003816","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100005801","name":"Facebook","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100005801","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"}]},{"name":"Austrian Academy of Sciences","award":["DOC 24956"],"award-info":[{"award-number":["DOC 24956"]}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["CoG 863818"],"award-info":[{"award-number":["CoG 863818"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,6,19]]},"DOI":"10.1145\/3453483.3454076","type":"proceedings-article","created":{"date-parts":[[2021,6,24]],"date-time":"2021-06-24T16:58:49Z","timestamp":1624553929000},"page":"772-787","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":29,"title":["Polynomial reachability witnesses via Stellens\u00e4tze"],"prefix":"10.1145","author":[{"given":"Ali","family":"Asadi","sequence":"first","affiliation":[{"name":"Sharif University of Technology, Iran"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4561-241X","authenticated-orcid":false,"given":"Krishnendu","family":"Chatterjee","sequence":"additional","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"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1702-6584","authenticated-orcid":false,"given":"Amir Kafshdar","family":"Goharshady","sequence":"additional","affiliation":[{"name":"Hong Kong University of Science and Technology, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mohammad","family":"Mahdavi","sequence":"additional","affiliation":[{"name":"Sharif University of Technology, Iran"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,6,18]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45237-7_25"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_12"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_48"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15769-1_8"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0032042"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1059"},{"key":"e_1_3_2_1_7_1","volume-title":"Amir Kafshdar Goharshady, and Mohammad Mahdavi","author":"Asadi Ali","year":"2021","unstructured":"Ali Asadi , Krishnendu Chatterjee , Hongfei Fu , Amir Kafshdar Goharshady, and Mohammad Mahdavi . 2021 . Polynomial Reachability Witnesses via Stellens\u00e4tze. HAL , 03183862 (2021). Ali Asadi, Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, and Mohammad Mahdavi. 2021. Polynomial Reachability Witnesses via Stellens\u00e4tze. HAL, 03183862 (2021)."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSTTCS.2011.152"},{"key":"e_1_3_2_1_9_1","volume-title":"Introduction to Commutative Algebra","author":"Atiyah Michael Francis","unstructured":"Michael Francis Atiyah and Ian Grant Macdonald . 1969. Introduction to Commutative Algebra . Taylor and Francis . Michael Francis Atiyah and Ian Grant Macdonald. 1969. Introduction to Commutative Algebra. Taylor and Francis."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_19"},{"key":"e_1_3_2_1_11_1","volume-title":"Principles of model checking","author":"Baier Christel","unstructured":"Christel Baier and Joost-Pieter Katoen . 2008. Principles of model checking . MIT Press . Christel Baier and Joost-Pieter Katoen. 2008. Principles of model checking. MIT Press."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_2"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56922-7_4"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1965724.1965743"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503274"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_18"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_32"},{"key":"e_1_3_2_1_18_1","volume-title":"Motzkin transposition theorem. Encyclopedia of Mathematics","author":"Ben-Israel Adi","unstructured":"Adi Ben-Israel . 2017. Motzkin transposition theorem. Encyclopedia of Mathematics , http:\/\/encyclopediaofmath.org\/index.php?title=Motzkin_transposition_theorem Adi Ben-Israel. 2017. Motzkin transposition theorem. Encyclopedia of Mathematics, http:\/\/encyclopediaofmath.org\/index.php?title=Motzkin_transposition_theorem"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_61"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45237-7_21"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0044-z"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_48"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_8"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2408776.2408795"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2018\/653"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3339984"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385969"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_11"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"e_1_3_2_1_33_1","volume-title":"Handbook of model checking","author":"Clarke Edmund M","unstructured":"Edmund M Clarke , Thomas A Henzinger , Helmut Veith , and Roderick Bloem . 2018. Handbook of model checking . Springer . Edmund M Clarke, Thomas A Henzinger, Helmut Veith, and Roderick Bloem. 2018. Handbook of model checking. Springer."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45319-9_6"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_1"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45260-5_1"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3313276.3316369"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(4:9)2012"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_12"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24690-6_12"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509511"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338112"},{"key":"e_1_3_2_1_46_1","article-title":"Theorie der einfachen Ungleichungen","author":"Farkas Julius","year":"1902","unstructured":"Julius Farkas . 1902 . Theorie der einfachen Ungleichungen . Journal f\u00fcr die reine und angewandte Mathematik. Julius Farkas. 1902. Theorie der einfachen Ungleichungen. Journal f\u00fcr die reine und angewandte Mathematik.","journal-title":"Journal f\u00fcr die reine und angewandte Mathematik."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68167-2_26"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"crossref","unstructured":"Robert W Floyd. 1993. Assigning meanings to programs. In Program Verification.  Robert W Floyd. 1993. Assigning meanings to programs. In Program Verification.","DOI":"10.1007\/978-94-011-1793-7_4"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_18"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0000474"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333989"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190226"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_18"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09535-x"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360555"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_61"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-015-0228-1"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68167-2_12"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2007.41"},{"key":"e_1_3_2_1_64_1","volume-title":"Temporal verification of reactive systems: Safety","author":"Manna Zohar","unstructured":"Zohar Manna and Amir Pnueli . 2012. Temporal verification of reactive systems: Safety . Springer . Zohar Manna and Amir Pnueli. 2012. Temporal verification of reactive systems: Safety. Springer."},{"key":"e_1_3_2_1_65_1","volume-title":"Understanding and using linear programming","author":"Matousek Jiri","unstructured":"Jiri Matousek and Bernd G\u00e4rtner . 2007. Understanding and using linear programming . Springer . Jiri Matousek and Bernd G\u00e4rtner. 2007. Understanding and using linear programming. Springer."},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/800076.802477"},{"key":"e_1_3_2_1_67_1","volume-title":"SymPy: symbolic computing in Python. PeerJ Computer Science, 3","author":"Meurer Aaron","year":"2017","unstructured":"Aaron Meurer , Christopher P Smith , Mateusz Paprocki , Ond\u0159ej \u010cert\u00edk , Sergey B Kirpichev , Matthew Rocklin , Amit Kumar , Sergiu Ivanov , Jason K Moore , and Sartaj Singh . 2017. SymPy: symbolic computing in Python. PeerJ Computer Science, 3 ( 2017 ). Aaron Meurer, Christopher P Smith, Mateusz Paprocki, Ond\u0159ej \u010cert\u00edk, Sergey B Kirpichev, Matthew Rocklin, Amit Kumar, Sergiu Ivanov, Jason K Moore, and Sartaj Singh. 2017. SymPy: symbolic computing in Python. PeerJ Computer Science, 3 (2017)."},{"key":"e_1_3_2_1_68_1","volume-title":"Basel","author":"Motzkin TS","year":"1933","unstructured":"TS Motzkin . 1936. Beitrage zur Theorie der linearen Ungleichungen (Dissertation , Basel 1933 ). TS Motzkin. 1936. Beitrage zur Theorie der linearen Ungleichungen (Dissertation, Basel 1933)."},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2004.1319598"},{"key":"e_1_3_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1512\/iumj.1993.42.42045"},{"key":"e_1_3_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_3"},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1953-0053041-6"},{"key":"e_1_3_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_21"},{"key":"e_1_3_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964028"},{"key":"e_1_3_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27864-1_7"},{"key":"e_1_3_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.03.008"},{"key":"e_1_3_2_1_80_1","volume-title":"Vechev","author":"Singh Gagandeep","year":"2017","unstructured":"Gagandeep Singh , Markus P\u00fcschel , and Martin T . Vechev . 2017 . Fast polyhedra abstract domain. In POPL. https:\/\/doi.org\/citation.cfm?id=3009885 Gagandeep Singh, Markus P\u00fcschel, and Martin T. Vechev. 2017. Fast polyhedra abstract domain. In POPL. https:\/\/doi.org\/citation.cfm?id=3009885"},{"key":"e_1_3_2_1_81_1","volume-title":"A nullstellensatz and a positivstellensatz in semialgebraic geometry. Math. Ann., 207, 2","author":"Stengle Gilbert","year":"1974","unstructured":"Gilbert Stengle . 1974. A nullstellensatz and a positivstellensatz in semialgebraic geometry. Math. Ann., 207, 2 ( 1974 ). Gilbert Stengle. 1974. A nullstellensatz and a positivstellensatz in semialgebraic geometry. Math. Ann., 207, 2 (1974)."},{"key":"e_1_3_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99725-4_24"},{"key":"e_1_3_2_1_83_1","volume-title":"LOQO: An interior point code for quadratic programming. Optimization methods and software, 11, 1-4","author":"Vanderbei Robert J","year":"1999","unstructured":"Robert J Vanderbei . 1999 . LOQO: An interior point code for quadratic programming. Optimization methods and software, 11, 1-4 (1999). Robert J Vanderbei. 1999. LOQO: An interior point code for quadratic programming. Optimization methods and software, 11, 1-4 (1999)."}],"event":{"name":"PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation","location":"Virtual Canada","acronym":"PLDI '21","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3453483.3454076","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3453483.3454076","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:47:47Z","timestamp":1750193267000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3453483.3454076"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,18]]},"references-count":82,"alternative-id":["10.1145\/3453483.3454076","10.1145\/3453483"],"URL":"https:\/\/doi.org\/10.1145\/3453483.3454076","relation":{},"subject":[],"published":{"date-parts":[[2021,6,18]]},"assertion":[{"value":"2021-06-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}