{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,17]],"date-time":"2025-09-17T06:11:06Z","timestamp":1758089466357,"version":"3.44.0"},"reference-count":27,"publisher":"IEEE","license":[{"start":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T00:00:00Z","timestamp":1750550400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T00:00:00Z","timestamp":1750550400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/501100005089","name":"Beijing Municipal Natural Science Foundation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100005089","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002367","name":"Chinese Academy of Sciences","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100002367","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025,6,22]]},"DOI":"10.1109\/dac63849.2025.11133195","type":"proceedings-article","created":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T17:35:41Z","timestamp":1757957741000},"page":"1-7","source":"Crossref","is-referenced-by-count":0,"title":["Property-driven Parallel Symbolic Model Checking of LTL"],"prefix":"10.1109","author":[{"given":"Yuheng","family":"Su","sequence":"first","affiliation":[{"name":"University of Chinese Academy of Sciences"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yingcheng","family":"Li","sequence":"additional","affiliation":[{"name":"University of Chinese Academy of Sciences"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qiusong","family":"Yang","sequence":"additional","affiliation":[{"name":"Institute of Software, Chinese Academy of Sciences"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yiwei","family":"Ci","sequence":"additional","affiliation":[{"name":"University of Chinese Academy of Sciences"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ziyu","family":"Huang","sequence":"additional","affiliation":[{"name":"Beijing Forestry University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1007\/bfb0058022"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35746-6_1"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_40"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-002-0093-2"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/2632362.2632379"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63516-3_12"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780195085914.001.0001"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/BF00121128"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/tc.1986.1676819"},{"key":"ref12","first-page":"267","article-title":"Efficient model checking in fragments of the propositional mu-calculus (extended abstract)","volume-title":"Proceedings of the Symposium on Logic in Computer Science (LICS \u201886)","author":"Emerson"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-40922-x_24"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1_11"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19583-9_9"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-005-1493-1"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpdc.2014.07.009"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/BF02127976"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-016-0433-2"},{"key":"ref21","article-title":"Ppsmc artifact"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_61"},{"key":"ref23","first-page":"52","article-title":"A liveness checking algorithm that counts","volume-title":"Formal Methods in Computer-Aided Design, FMCAD 2012","author":"Claessen"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38088-4_3"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_6"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39724-3_35"}],"event":{"name":"2025 62nd ACM\/IEEE Design Automation Conference (DAC)","start":{"date-parts":[[2025,6,22]]},"location":"San Francisco, CA, USA","end":{"date-parts":[[2025,6,25]]}},"container-title":["2025 62nd ACM\/IEEE Design Automation Conference (DAC)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/11132383\/11132091\/11133195.pdf?arnumber=11133195","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,16]],"date-time":"2025-09-16T05:36:14Z","timestamp":1758000974000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/11133195\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,22]]},"references-count":27,"URL":"https:\/\/doi.org\/10.1109\/dac63849.2025.11133195","relation":{},"subject":[],"published":{"date-parts":[[2025,6,22]]}}}