{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,24]],"date-time":"2024-07-24T15:54:40Z","timestamp":1721836480486},"reference-count":107,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"4","license":[{"start":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T00:00:00Z","timestamp":1648771200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T00:00:00Z","timestamp":1648771200000},"content-version":"am","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T00:00:00Z","timestamp":1648771200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T00:00:00Z","timestamp":1648771200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1617916","1901769"],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000183","name":"U.S. Army Research Office","doi-asserted-by":"publisher","award":["W911NF-19-1-0054"],"id":[{"id":"10.13039\/100000183","id-type":"DOI","asserted-by":"publisher"}]},{"name":"DARPA ARCOS","award":["FA8750-20-C-0507"]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IIEEE Trans. Software Eng."],"published-print":{"date-parts":[[2022,4,1]]},"DOI":"10.1109\/tse.2020.3016778","type":"journal-article","created":{"date-parts":[[2020,8,14]],"date-time":"2020-08-14T20:35:26Z","timestamp":1597437326000},"page":"1212-1227","source":"Crossref","is-referenced-by-count":2,"title":["Conditional Quantitative Program Analysis"],"prefix":"10.1109","volume":"48","author":[{"ORCID":"http:\/\/orcid.org\/0000-0003-0666-1427","authenticated-orcid":false,"given":"Mitchell","family":"Gerrard","sequence":"first","affiliation":[]},{"given":"Mateus","family":"Borges","sequence":"additional","affiliation":[]},{"ORCID":"http:\/\/orcid.org\/0000-0002-1937-1544","authenticated-orcid":false,"given":"Matthew B.","family":"Dwyer","sequence":"additional","affiliation":[]},{"ORCID":"http:\/\/orcid.org\/0000-0001-9646-646X","authenticated-orcid":false,"given":"Antonio","family":"Filieri","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref1","article-title":"DO-178C: Software considerations in airborne systems and equipment certification","year":"2011"},{"key":"ref2","article-title":"ISO 10218: Robots and robotic devices safety requirements for industrial robots","year":"2011"},{"key":"ref3","article-title":"ISO 13482: Robots and robotic devices safety requirements for personal care robots","year":"2014"},{"key":"ref4","article-title":"EN 50126: Railways applications the specification and demonstration of reliability, availability, maintainability and safety (RAMS),","year":"2017"},{"key":"ref5","article-title":"ISO 26262: Road vehicles functional safety","year":"2011"},{"key":"ref6","article-title":"IEC 62304: Medical device software\u2013software life cycle processes","year":"2006"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/FOSE.2007.18"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2014.03.001"},{"key":"ref9","article-title":"IEC 61508: Functional safety of electrical\/electronic\/programmable safety-related systems","year":"2010"},{"key":"ref10","article-title":"DO-333 : Formal methods supplement to DO-178C and DO-278A","year":"2011"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06200-6_1"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1049\/cp.2015.0278"},{"key":"ref14","article-title":"Practical statistical evaluation of critical software","author":"Ladkin","year":"2016"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/32.210303"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/WSC40007.2019.9004839"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1145\/2338965.2336773"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606608"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/2635868.2635899"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2017.8115649"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-Companion.2019.00032"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_8"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-013-0195-3"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16612-9_11"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/3158668"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1145\/249069.231433"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45099-3_17"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36577-X_40"},{"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","volume":"8","author":"Cadar"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2012.31"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2015.99"},{"key":"ref33","article-title":"An algorithmic theory of lattice points","volume":"38","author":"Barvinok","year":"1999","journal-title":"New Perspectives Algebr. Combinatorics"},{"key":"ref34","article-title":"A user\u2019s guide for latte integrale v1. 7.2","volume":"22","author":"Baldoni","year":"2014"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1145\/1132973.1132980"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/s00453-006-1231-0"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594331"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_15"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594329"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1145\/318593.318659"},{"key":"ref41","article-title":"ALPACA: An instatiation of the alternating conditional analysis framework","author":"Gerrard","year":"2019"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1016\/S0950-5849(98)00093-7"},{"key":"ref44","article-title":"Lecture notes in model checking","author":"Malik","year":"2018"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-61455-2_16"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393664"},{"key":"ref48","volume-title":"Mathematical Statistics: An Introduction","volume":"1","author":"Pestman","year":"1998"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-57288-8_9"},{"key":"ref50","volume-title":"Handbook of Satisfiability","author":"Biere","year":"2009"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2007.68"},{"key":"ref52","first-page":"151","article-title":"Automated whitebox fuzz testing,","volume-title":"Proc. Netw. Distrib. Syst. Secur. Symp.","volume":"8","author":"Godefroid","year":"2008"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2017.2785841"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786832"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(79)90044-6"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-0348-8438-9_6"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-32859-1_47"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1145\/102782.102783"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462179"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-4145-2"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_21"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40627-0_18"},{"key":"ref63","first-page":"633","volume-title":"Model Counting","author":"Gomes","year":"2009"},{"key":"ref64","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-017-0297-2"},{"key":"ref65","doi-asserted-by":"publisher","DOI":"10.1098\/rspa.2015.0142"},{"key":"ref66","first-page":"3569","article-title":"Algorithmic improvements in approximate counting for probabilistic inference: From linear to logarithmic sat calls","volume-title":"Proc. 25th Int. Joint Conf. Artif. Intell.","author":"Chakraborty"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.1145\/2807591.2807635"},{"key":"ref68","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"ref69","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54580-5_22"},{"key":"ref70","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_34"},{"key":"ref71","first-page":"405","article-title":"ESBMC 1.22","volume-title":"Proc. Int. Conf. Tools Algorithms Construction Anal. Syst.","author":"Morse"},{"key":"ref72","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17502-3_19"},{"key":"ref73","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_50"},{"key":"ref74","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89963-3_30"},{"key":"ref75","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54580-5_31"},{"key":"ref76","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89963-3_32"},{"key":"ref77","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"ref78","doi-asserted-by":"publisher","DOI":"10.1145\/2810012"},{"key":"ref79","article-title":"CIVL: The concurrency intermediate verification language reference manual, v1.19","author":"Dwyer","year":"2019"},{"key":"ref80","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17502-3_9"},{"key":"ref81","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180177"},{"key":"ref82","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_3"},{"key":"ref83","doi-asserted-by":"publisher","DOI":"10.1145\/1181775.1181787"},{"key":"ref84","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884835"},{"key":"ref85","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44829-2_17"},{"key":"ref86","doi-asserted-by":"publisher","DOI":"10.1145\/1181775.1181790"},{"key":"ref87","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390634"},{"key":"ref88","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706307"},{"key":"ref89","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_12"},{"key":"ref90","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_48"},{"key":"ref91","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03811-6"},{"key":"ref92","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39176-7_1"},{"key":"ref93","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46675-9_7"},{"key":"ref94","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884843"},{"key":"ref95","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106249"},{"key":"ref96","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180259"},{"key":"ref97","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934574"},{"key":"ref98","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"ref99","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_9"},{"key":"ref100","doi-asserted-by":"publisher","DOI":"10.1145\/2642937.2643011"},{"key":"ref101","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884794"},{"key":"ref102","doi-asserted-by":"publisher","DOI":"10.1145\/3213846.3213867"},{"key":"ref103","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00030"},{"key":"ref104","doi-asserted-by":"publisher","DOI":"10.1145\/2593882.2593900"},{"key":"ref105","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594294"},{"key":"ref106","doi-asserted-by":"publisher","DOI":"10.1145\/2541940.2541958"},{"key":"ref107","doi-asserted-by":"publisher","DOI":"10.1145\/2635868.2635923"},{"key":"ref108","doi-asserted-by":"publisher","DOI":"10.1109\/ECBS.2011.8"}],"container-title":["IEEE Transactions on Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/ieeexplore.ieee.org\/ielam\/32\/9758085\/9167482-aam.pdf","content-type":"application\/pdf","content-version":"am","intended-application":"syndication"},{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/32\/9758085\/09167482.pdf?arnumber=9167482","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,9]],"date-time":"2024-01-09T23:19:43Z","timestamp":1704842383000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9167482\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,1]]},"references-count":107,"journal-issue":{"issue":"4"},"URL":"https:\/\/doi.org\/10.1109\/tse.2020.3016778","relation":{},"ISSN":["0098-5589","1939-3520","2326-3881"],"issn-type":[{"value":"0098-5589","type":"print"},{"value":"1939-3520","type":"electronic"},{"value":"2326-3881","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4,1]]}}}