{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,4]],"date-time":"2025-06-04T19:04:07Z","timestamp":1749063847095,"version":"3.37.3"},"reference-count":52,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"4","license":[{"start":{"date-parts":[[2021,12,1]],"date-time":"2021-12-01T00:00:00Z","timestamp":1638316800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2021,12,1]],"date-time":"2021-12-01T00:00:00Z","timestamp":1638316800000},"content-version":"am","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"funder":[{"DOI":"10.13039\/501100010261","name":"National Key R&D Program of China","doi-asserted-by":"publisher","award":["2018AAA0103202"],"award-info":[{"award-number":["2018AAA0103202"]}],"id":[{"id":"10.13039\/501100010261","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62172322","61751207","61732013"],"award-info":[{"award-number":["62172322","61751207","61732013"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100010261","name":"Shaanxi Key Science and Technology Innovation Team Project","doi-asserted-by":"publisher","award":["2019TD-001"],"award-info":[{"award-number":["2019TD-001"]}],"id":[{"id":"10.13039\/501100010261","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Rel."],"published-print":{"date-parts":[[2021,12]]},"DOI":"10.1109\/tr.2021.3118877","type":"journal-article","created":{"date-parts":[[2021,10,26]],"date-time":"2021-10-26T20:32:36Z","timestamp":1635280356000},"page":"1455-1467","source":"Crossref","is-referenced-by-count":1,"title":["A CEGAR-Based Static\u2013Dynamic Approach to Verifying Full Regular Properties of C Programs"],"prefix":"10.1109","volume":"70","author":[{"given":"Kai","family":"Yang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5429-4580","authenticated-orcid":false,"given":"Cong","family":"Tian","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3870-2505","authenticated-orcid":false,"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"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2138-749X","authenticated-orcid":false,"given":"Hongwei","family":"Du","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref39","first-page":"90","article-title":"An improved decision procedure for propositional projection temporal logic","author":"z","year":"0","journal-title":"Proc 1st Int Conf Formal Engineering Methods"},{"journal-title":"Temporal Logic and Temporal Logic Programming","year":"2005","author":"z","key":"ref38"},{"article-title":"An extended interval temporal logic and a framing technique for temporal logic programming","year":"1996","author":"duan","key":"ref33"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2014.02.011"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/TR.2020.2999441"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-C.2017.98"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2021.02.007"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1109\/32.57624"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0044-z"},{"key":"ref28","first-page":"246","article-title":"Model checking propositional projection temporal logic based on spin","author":"duan","year":"0","journal-title":"Proc 1st Int Conf Formal Engineering Methods"},{"key":"ref27","first-page":"47","article-title":"Propositional projection temporal logic, b$\\ddot{u}$ chi automata and $\\omega$-regular expressions","author":"tian","year":"0","journal-title":"Proc Int Conf Theory Appl Models Comput"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpdc.2017.09.003"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/TR.2018.2873260"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/TR.2015.2452931"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_4"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_2"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_22"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1145\/1453101.1453150"},{"key":"ref23","doi-asserted-by":"crossref","first-page":"1814","DOI":"10.23940\/ijpe.20.11.p13.18141825","article-title":"Software fault detection for sequencing constraint defects","volume":"16","author":"cheng","year":"2020","journal-title":"Int J Performability Eng"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2017.09.026"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-007-0062-z"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1145\/1133255.1134029"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1145\/3828.3837"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"ref10","first-page":"24","article-title":"Static and dynamic analysis: Synergy and duality","author":"ernst","year":"0","journal-title":"Proc ICSE Workshop Dyn Anal"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24756-2_1"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1007\/BF02944904"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44829-2_17"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/3468264.3468602"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2004.829807"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36577-X_14"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/TR.2018.2876333"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/TR.2018.2806349"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.23940\/ijpe.21.02.p8.241252"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050046"},{"article-title":"Automated verification of system requirements and software specifications","year":"2016","author":"dietsch","key":"ref49"},{"key":"ref9","first-page":"52","article-title":"Design and synthesis of synchronization skeletons using branching time temporal logic","author":"clarke","year":"0","journal-title":"Proc Workshop Program Logic"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34026-0_45"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2019.12.038"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1145\/565816.503279"},{"journal-title":"Standard Performance Evaluation Corporation (SPEC)","year":"0","key":"ref47"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-04915-1_5"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2017.07.032"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11737-9_29"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1007\/s11704-016-6059-4"}],"container-title":["IEEE Transactions on Reliability"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/24\/9629389\/09586736.pdf?arnumber=9586736","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,8]],"date-time":"2022-03-08T21:18:15Z","timestamp":1646774295000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9586736\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,12]]},"references-count":52,"journal-issue":{"issue":"4"},"URL":"https:\/\/doi.org\/10.1109\/tr.2021.3118877","relation":{},"ISSN":["0018-9529","1558-1721"],"issn-type":[{"type":"print","value":"0018-9529"},{"type":"electronic","value":"1558-1721"}],"subject":[],"published":{"date-parts":[[2021,12]]}}}