{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T03:10:12Z","timestamp":1725937812769},"publisher-location":"New York, NY, USA","reference-count":82,"publisher":"ACM","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"],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Austrian Academy of Sciences","award":["DOC 24956"]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["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-24T12:58:49Z","timestamp":1624539529000},"page":"772-787","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Polynomial reachability witnesses via Stellens\u00e4tze"],"prefix":"10.1145","author":[{"given":"Ali","family":"Asadi","sequence":"first","affiliation":[{"name":"Sharif University of Technology, Iran"}]},{"ORCID":"http:\/\/orcid.org\/0000-0002-4561-241X","authenticated-orcid":false,"given":"Krishnendu","family":"Chatterjee","sequence":"additional","affiliation":[{"name":"IST Austria, Austria"}]},{"given":"Hongfei","family":"Fu","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, China"}]},{"ORCID":"http:\/\/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"}]},{"given":"Mohammad","family":"Mahdavi","sequence":"additional","affiliation":[{"name":"Sharif University of Technology, Iran"}]}],"member":"320","published-online":{"date-parts":[[2021,6,18]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_3_2_1_1_1","DOI":"10.1007\/978-3-030-45237-7_25"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_2_1","DOI":"10.1007\/978-3-642-28756-5_12"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_3_1","DOI":"10.1007\/978-3-642-31424-7_48"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_4_1","DOI":"10.1007\/978-3-642-15769-1_8"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_5_1","DOI":"10.1007\/BFb0032042"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_6_1","DOI":"10.1006\/inco.1995.1059"},{"volume-title":"Amir Kafshdar Goharshady, and Mohammad Mahdavi","year":"2021","author":"Asadi Ali","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_7_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_8_1","DOI":"10.4230\/LIPIcs.FSTTCS.2011.152"},{"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_9_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_10_1","DOI":"10.1007\/3-540-44898-5_19"},{"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_11_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_12_1","DOI":"10.1007\/978-3-662-49674-9_2"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_13_1","DOI":"10.1007\/3-540-56922-7_4"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_14_1","DOI":"10.1145\/1965724.1965743"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_15_1","DOI":"10.1145\/503272.503274"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_16_1","DOI":"10.1007\/978-3-319-21668-3_18"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_17_1","DOI":"10.1007\/978-3-319-63390-9_32"},{"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_18_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_19_1","DOI":"10.1007\/978-3-642-39799-8_61"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_20_1","DOI":"10.1007\/978-3-030-45237-7_21"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_21_1","DOI":"10.1007\/s10009-007-0044-z"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_22_1","DOI":"10.1007\/978-3-642-22110-1_16"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_23_1","DOI":"10.1007\/11513988_48"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_24_1","DOI":"10.1007\/978-3-540-30579-8_8"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_25_1","DOI":"10.1145\/2408776.2408795"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_26_1","DOI":"10.1007\/978-3-319-08867-9_22"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_27_1","DOI":"10.24963\/ijcai.2018\/653"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_28_1","DOI":"10.1007\/978-3-319-41528-4_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_29_1","DOI":"10.1145\/3339984"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_30_1","DOI":"10.1145\/3385412.3385969"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_31_1","DOI":"10.1007\/978-3-642-54862-8_11"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_32_1","DOI":"10.1007\/10722167_15"},{"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_33_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_34_1","DOI":"10.1007\/978-3-540-45069-6_39"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_35_1","DOI":"10.1007\/3-540-45319-9_6"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_36_1","DOI":"10.1007\/978-3-540-30579-8_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_37_1","DOI":"10.1007\/978-3-030-45260-5_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_38_1","DOI":"10.1145\/512950.512973"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_39_1","DOI":"10.1145\/3313276.3316369"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_40_1","DOI":"10.2168\/LMCS-8(4:9)2012"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_41_1","DOI":"10.1007\/978-3-319-48989-6_12"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_42_1","DOI":"10.1007\/978-3-540-78800-3_24"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_43_1","DOI":"10.1007\/978-3-642-24690-6_12"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_44_1","DOI":"10.1145\/2509136.2509511"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_45_1","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."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_47_1","DOI":"10.1007\/978-3-319-68167-2_26"},{"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.","key":"e_1_3_2_1_48_1","DOI":"10.1007\/978-94-011-1793-7_4"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_49_1","DOI":"10.1007\/978-3-642-36742-7_18"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_50_1","DOI":"10.1007\/BFb0000474"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_51_1","DOI":"10.1145\/333979.333989"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_52_1","DOI":"10.1145\/1190216.1190226"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_54_1","DOI":"10.1007\/11817963_18"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_55_1","DOI":"10.1007\/s10817-019-09535-x"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_56_1","DOI":"10.1145\/503272.503279"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_57_1","DOI":"10.1145\/363235.363259"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_58_1","DOI":"10.1109\/32.588521"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_59_1","DOI":"10.1145\/3360555"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_60_1","DOI":"10.1007\/978-3-642-31424-7_61"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_61_1","DOI":"10.1007\/s10703-015-0228-1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_62_1","DOI":"10.1007\/978-3-319-68167-2_12"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_63_1","DOI":"10.1109\/ICSE.2007.41"},{"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_64_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_65_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_66_1","DOI":"10.1145\/800076.802477"},{"volume-title":"SymPy: symbolic computing in Python. PeerJ Computer Science, 3","year":"2017","author":"Meurer Aaron","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_67_1"},{"volume-title":"Basel","year":"1933","author":"Motzkin TS","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_68_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_69_1","DOI":"10.1145\/3371078"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_70_1","DOI":"10.1109\/SFCS.1977.32"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_71_1","DOI":"10.1007\/978-3-540-24622-0_20"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_72_1","DOI":"10.1109\/LICS.2004.1319598"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_73_1","DOI":"10.1512\/iumj.1993.42.42045"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_74_1","DOI":"10.1007\/978-3-642-35873-9_3"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_75_1","DOI":"10.1090\/S0002-9947-1953-0053041-6"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_76_1","DOI":"10.1007\/11547662_21"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_77_1","DOI":"10.1145\/964001.964028"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_78_1","DOI":"10.1007\/978-3-540-27864-1_7"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_79_1","DOI":"10.1016\/j.scico.2006.03.008"},{"volume-title":"Vechev","year":"2017","author":"Singh Gagandeep","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_80_1"},{"volume-title":"A nullstellensatz and a positivstellensatz in semialgebraic geometry. Math. Ann., 207, 2","year":"1974","author":"Stengle Gilbert","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_81_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_82_1","DOI":"10.1007\/978-3-319-99725-4_24"},{"volume-title":"LOQO: An interior point code for quadratic programming. Optimization methods and software, 11, 1-4","year":"1999","author":"Vanderbei Robert J","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).","key":"e_1_3_2_1_83_1"}],"event":{"sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"acronym":"PLDI '21","name":"PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation","location":"Virtual Canada"},"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\/pdf\/10.1145\/3453483.3454076","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,6]],"date-time":"2023-01-06T23:40:19Z","timestamp":1673048419000},"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"}}]}}
