{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T08:26:31Z","timestamp":1777623991017,"version":"3.51.4"},"reference-count":75,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"3","license":[{"start":{"date-parts":[[2019,9,1]],"date-time":"2019-09-01T00:00:00Z","timestamp":1567296000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2019,9,1]],"date-time":"2019-09-01T00:00:00Z","timestamp":1567296000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2019,9,1]],"date-time":"2019-09-01T00:00:00Z","timestamp":1567296000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61420106004"],"award-info":[{"award-number":["61420106004"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61732013"],"award-info":[{"award-number":["61732013"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61751207"],"award-info":[{"award-number":["61751207"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61572386"],"award-info":[{"award-number":["61572386"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Rel."],"published-print":{"date-parts":[[2019,9]]},"DOI":"10.1109\/tr.2018.2876333","type":"journal-article","created":{"date-parts":[[2018,11,12]],"date-time":"2018-11-12T23:19:42Z","timestamp":1542064782000},"page":"1101-1116","source":"Crossref","is-referenced-by-count":15,"title":["Verifying Full Regular Temporal Properties of Programs via Dynamic Program Execution"],"prefix":"10.1109","volume":"68","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3582-9559","authenticated-orcid":false,"given":"Meng","family":"Wang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cong","family":"Tian","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nan","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3119-3242","authenticated-orcid":false,"given":"Zhenhua","family":"Duan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref73","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00253-1"},{"key":"ref72","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_60"},{"key":"ref71","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27705-4_12"},{"key":"ref70","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2011.59"},{"key":"ref74","doi-asserted-by":"publisher","DOI":"10.1145\/1297027.1297069"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1145\/1455518.1455522"},{"key":"ref75","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68524-1_3"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081750"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-007-0062-z"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2014.02.011"},{"key":"ref31","article-title":"Verifying schedulability of tasks in ROS-based systems","author":"cui","year":"2018","journal-title":"J Combinatorial Optim"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1109\/TR.2018.2806349"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"ref36","article-title":"A compiler for MSVL and its applications","author":"yang","year":"2017","journal-title":"Theor Comput Sci"},{"key":"ref35","article-title":"Verifying a scheduling protocol of safety-critical systems","author":"wang","year":"2018","journal-title":"J Combinatorial Optim"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/s10878-014-9776-3"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.1109\/CSCWD.2013.6580942"},{"key":"ref62","year":"0"},{"key":"ref61","year":"0"},{"key":"ref63","year":"0"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2016.02.037"},{"key":"ref64","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"ref27","author":"duan","year":"2005","journal-title":"Temporal Logic and Temporal Logic Programming"},{"key":"ref65","doi-asserted-by":"publisher","DOI":"10.21236\/ADA360973"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2004.22"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/s10878-012-9551-2"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_40"},{"key":"ref68","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"ref69","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-008-0091-0"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_29"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"ref20","article-title":"SLIC: A specification language for interface checking (of C)","author":"ball","year":"2002"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_22"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_4"},{"key":"ref24","first-page":"141","article-title":"A tutorial on runtime verification","volume":"34","author":"falcone","year":"2013","journal-title":"Engineering Dependable Software Systems"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_2"},{"key":"ref26","article-title":"An extended interval temporal logic and a framing technique for temporal logic programming","author":"duan","year":"1996"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-C.2017.98"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1007\/BF02944904"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2008.08.001"},{"key":"ref59","first-page":"51","article-title":"Verifying systemc: A software model checking approach","author":"cimatti","year":"2010","journal-title":"Proc IEEE 10th Int Conf Formal Methods Comput -Aided Des"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2015.40"},{"key":"ref57","article-title":"Translating C programs to MSVL programs","author":"wang","year":"2018","journal-title":"arXiv 1809 00959"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1007\/s11432-015-0882-6"},{"key":"ref55","author":"clarke","year":"1999","journal-title":"Model checking"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90066-U"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1007\/s11704-016-6059-4"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-002-0095-0"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0044-z"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1109\/TR.2018.2834476"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_45"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44829-2_17"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/1060289.1060297"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134029"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190257"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2009.5351147"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/TR.2014.2335995"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2005.77"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/TR.2015.2508559"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.09.001"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45139-0_7"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926431"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34026-0_45"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.08.039"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2494596"},{"key":"ref42","first-page":"209","article-title":"KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs","author":"cadar","year":"2008","journal-title":"Proc of the 8th USENIX Symp on Operating Systems Design and Implementation"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88194-0_12"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950800738X"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2004.1281665"}],"container-title":["IEEE Transactions on Reliability"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/24\/8821425\/08531789.pdf?arnumber=8531789","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,13]],"date-time":"2022-07-13T20:53:30Z","timestamp":1657745610000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8531789\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,9]]},"references-count":75,"journal-issue":{"issue":"3"},"URL":"https:\/\/doi.org\/10.1109\/tr.2018.2876333","relation":{},"ISSN":["0018-9529","1558-1721"],"issn-type":[{"value":"0018-9529","type":"print"},{"value":"1558-1721","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,9]]}}}