{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T09:59:03Z","timestamp":1740131943160,"version":"3.37.3"},"reference-count":72,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"10","license":[{"start":{"date-parts":[[2022,10,1]],"date-time":"2022-10-01T00:00:00Z","timestamp":1664582400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2022,10,1]],"date-time":"2022-10-01T00:00:00Z","timestamp":1664582400000},"content-version":"am","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2022,10,1]],"date-time":"2022-10-01T00:00:00Z","timestamp":1664582400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2022,10,1]],"date-time":"2022-10-01T00:00:00Z","timestamp":1664582400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"name":"UNL Faculty Award"},{"DOI":"10.13039\/501100008982","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1948536","1617916","1901769"],"award-info":[{"award-number":["1948536","1617916","1901769"]}],"id":[{"id":"10.13039\/501100008982","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000183","name":"Army Research Office","doi-asserted-by":"publisher","award":["W911NF-19-1-0054"],"award-info":[{"award-number":["W911NF-19-1-0054"]}],"id":[{"id":"10.13039\/100000183","id-type":"DOI","asserted-by":"publisher"}]},{"name":"DARPA ARCOS program","award":["FA8750-20-C-0507"],"award-info":[{"award-number":["FA8750-20-C-0507"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IIEEE Trans. Software Eng."],"published-print":{"date-parts":[[2022,10,1]]},"DOI":"10.1109\/tse.2021.3106964","type":"journal-article","created":{"date-parts":[[2021,8,24]],"date-time":"2021-08-24T20:24:47Z","timestamp":1629836687000},"page":"3877-3899","source":"Crossref","is-referenced-by-count":3,"title":["Using Symbolic States to Infer Numerical Invariants"],"prefix":"10.1109","volume":"48","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4255-4592","authenticated-orcid":false,"given":"ThanhVu","family":"Nguyen","sequence":"first","affiliation":[{"name":"Department of Computer Science, George Mason University, Fairfax, VA, USA"}]},{"given":"KimHao","family":"Nguyen","sequence":"additional","affiliation":[{"name":"University of Nebraska-Lincoln, Lincoln, NE, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1937-1544","authenticated-orcid":false,"given":"Matthew B.","family":"Dwyer","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Virginia, Charlottesville, VA, USA"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"volume-title":"Introduction to Algorithms","year":"2009","author":"Cormen","key":"ref2"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/362452.362489"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629585"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349342"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2019.00046"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0223-4"},{"year":"2021","key":"ref8","article-title":"Coverity scanner"},{"year":"2021","key":"ref9","article-title":"The infer static analyzer"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512538"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/ICSM.2001.972767"},{"key":"ref13","first-page":"281","article-title":"Dysy","volume-title":"Proc. Int. Conf. Softw. Eng.","author":"Csallner"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/32.908957"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/2931037.2931049"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/3428257"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/2610384.2610389"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908099"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837664"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106281"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385986"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1090\/gsm\/161"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69166-2_13"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71209-1_12"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/2807591.2807635"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2012.6227149"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568275"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/2556782"},{"key":"ref30","first-page":"209","article-title":"KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs","volume-title":"Proc. 8th USENIX Conf. Operating Syst. Des. Implementation","author":"Cadar"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2017.8115691"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.53"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1145\/3140587.3062378"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1145\/3416507.3423189"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542518"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_14"},{"volume-title":"Introduction to Linear Algebra","year":"1993","author":"Strang","key":"ref37"},{"article-title":"Weakly relational numerical abstract domains","year":"2004","author":"Min\u00e9","key":"ref38"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36675-8_11"},{"article-title":"Sage mathematics software","year":"2021","author":"Stein","key":"ref40"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54580-5_20"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2007.01.002"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_31"},{"key":"ref45","first-page":"127","article-title":"SPEED: Precise and efficient static estimation of program computational complexity","volume-title":"Principles of Programming Languages","author":"Gulwani","year":"2009"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_7"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0044-z"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_48"},{"article-title":"Interproc analyzer for recursive programs with numerical variables","year":"2014","author":"Jeannet","key":"ref49"},{"year":"2021","key":"ref50","article-title":"SyGuS: Syntax-guided synthesis competition"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_24"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_7"},{"year":"2021","key":"ref53","article-title":"HOLA programs in SMT-LIB"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.4.511"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1145\/234528.234740"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8609-1"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1145\/1005285.1005324"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2017.8102247"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2018.8603011"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89960-2_14"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99725-4_20"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_10"},{"key":"ref64","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"ref65","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2018.8603013"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.1109\/SYNASC.2017.00033"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0249-4"},{"key":"ref68","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_14"},{"key":"ref69","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23702-7_11"},{"key":"ref70","doi-asserted-by":"publisher","DOI":"10.1145\/2338965.2336771"},{"key":"ref71","doi-asserted-by":"publisher","DOI":"10.1145\/1831708.1831732"},{"key":"ref72","first-page":"58:1","article-title":"Green: Reducing, reusing and recycling constraints in program analysis","volume-title":"Foundations of Software Engineering","author":"Visser","year":"2012"}],"container-title":["IEEE Transactions on Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/ieeexplore.ieee.org\/ielam\/32\/9923560\/9521719-aam.pdf","content-type":"application\/pdf","content-version":"am","intended-application":"syndication"},{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/32\/9923560\/09521719.pdf?arnumber=9521719","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,11]],"date-time":"2024-01-11T23:10:06Z","timestamp":1705014606000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9521719\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,1]]},"references-count":72,"journal-issue":{"issue":"10"},"URL":"https:\/\/doi.org\/10.1109\/tse.2021.3106964","relation":{},"ISSN":["0098-5589","1939-3520","2326-3881"],"issn-type":[{"type":"print","value":"0098-5589"},{"type":"electronic","value":"1939-3520"},{"type":"electronic","value":"2326-3881"}],"subject":[],"published":{"date-parts":[[2022,10,1]]}}}