{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T20:00:42Z","timestamp":1694635242779},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2009,3,1]],"date-time":"2009-03-01T00:00:00Z","timestamp":1235865600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Front. Comput. Sci. China"],"published-print":{"date-parts":[[2009,3]]},"DOI":"10.1007\/s11704-009-0003-9","type":"journal-article","created":{"date-parts":[[2009,2,26]],"date-time":"2009-02-26T13:09:26Z","timestamp":1235653766000},"page":"130-141","source":"Crossref","is-referenced-by-count":2,"title":["Symbolic model checking APSL"],"prefix":"10.1007","volume":"3","author":[{"given":"Wanwei","family":"Liu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ji","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Huowang","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaodong","family":"Ma","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhaofei","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2009,3,12]]},"reference":[{"issue":"8","key":"3_CR1","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"Bryant R E. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 1986, C-35(8): 677\u2013691","journal-title":"IEEE Transactions on Computers"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"McMillan K L. Symbolic Model Checking, An Approach to the State Explosion Problem. PhD thesis, Carnegie Mellon University, Kluwer Academic Publishers, 1993","DOI":"10.1007\/978-1-4615-3190-6_3"},{"key":"3_CR3","unstructured":"Accellera. Accellera property languages reference manual. http:\/\/www.eda.org\/vfv\/docs\/PSL-v1.1.pdf , 2004"},{"issue":"4","key":"3_CR4","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.entcs.2007.09.004","volume":"190","author":"R. Bloem","year":"2007","unstructured":"Bloem R, Galler S, Jobstmann B, et al. Specify, compile, run: Hardware from PSL. Electronic Notes in Theoretical Computer Science, 2007, 190(4): 3\u201316","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Boule M, Zilic Z. Efficient automata-based assersion-checker Synthesis of SEREs for hardware emulation. In: Proceedings of 12th Conference on Asia South Pacific Design Automation. IEEE, 2007","DOI":"10.1109\/ASPDAC.2007.358006"},{"key":"3_CR6","series-title":"LNCS","first-page":"1","volume-title":"Proceeding of International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Y. Vardi","year":"2001","unstructured":"Vardi M Y. Branching vs. linear time: Final showdown. In: Proceeding of International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer, 2001, LNCS, 2031: 1\u201322"},{"key":"3_CR7","unstructured":"Bustan D, Fisman D, Havlicek J. Automata construction for PSL. Technical Report MCS05-04, IBM Haifa Research Lab, 2005"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Ruah S, Fisman D, Ben-David S. Automata construction for on-the-fly model checking PSL safety simple subset. Technical Report H0234, IBM Haifa Research Lab, 2005","DOI":"10.1007\/11678779_2"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Jin N, Shen C. Dynamic verifying the properties of the simple subset of PSL. In: Proceedings of 1st IEEE Symposium of Theoretical Aspects on Software Engineering, 2007, 173\u2013182","DOI":"10.1109\/TASE.2007.20"},{"key":"3_CR10","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1007\/3-540-58179-0_72","volume-title":"Proceedings of the 6th Conference on Computer Aided verification","author":"E. M. Clarke","year":"1994","unstructured":"Clarke E M, Grumberg O, Hamaguchi K. Another Look at LTL Model Checking. In: Proceedings of the 6th Conference on Computer Aided verification. Berlin: Springer-Verlag, 1994, LNCS, 818: 415\u2013427"},{"key":"3_CR11","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1007\/3-540-48683-6_44","volume-title":"Proceedings of the 11th Conference on Computer Aided Verification","author":"A. Cimatti","year":"1999","unstructured":"Cimatti A, Clarke E, Giunchiglia F, et al. NuSMV: A New Symbolic Model Verifier. In: Proceedings of the 11th Conference on Computer Aided Verification. Berlin: Springer, 1999, LNCS, 1633: 495\u2013499"},{"key":"3_CR12","series-title":"LNCS","first-page":"573","volume-title":"Proceedings of the 14th International Symposium on Formal Methods","author":"A. Pnueli","year":"2006","unstructured":"Pnueli A, Zaks A. PSL model checking and runtime verification via testers. In: Misra J, Nipkow T, Sekerinski E, eds. Proceedings of the 14th International Symposium on Formal Methods. Berlin: Springer-Verlag, 2006, LNCS, 4085: 573\u2013586"},{"key":"3_CR13","unstructured":"Martin A J. The design of a self-timed circuit for distributed mutual exclusion. In: Fuchs H, ed. Proceedings of the 1985 Chapel Hill Conference on Very Large Scale Integration, 1985."},{"issue":"1\u20132","key":"3_CR14","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. Wolper","year":"1983","unstructured":"Wolper P. Temporal logic can be more expressive. Information and Control, 1983, 56(1\u20132): 72\u201399","journal-title":"Information and Control"},{"issue":"1","key":"3_CR15","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M. Y. Vardi","year":"1994","unstructured":"Vardi M Y, Wolper P. Reasoning about Infinite Computations. Information and Computation, 1994, 115(1): 1\u201337","journal-title":"Information and Computation"},{"key":"3_CR16","series-title":"LNCS","first-page":"296","volume-title":"Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Armoni","year":"2002","unstructured":"Armoni R, Fix L, Flaisher A, et al. The ForSpec Temporal Logic: A New Temporal Property-Specification Language. In: Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer, 2002, LNCS, 2280: 296\u2013311"},{"key":"3_CR17","unstructured":"Beer I, Ben-David S, Eisner C, et al. RuleBase: an industry-oriented formal verification tool. In: Proceedings of 33rd Design Automation Conference, ACM Press, 1996, 655\u2013660"},{"key":"3_CR18","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1016\/j.tcs.2008.03.011","volume":"404","author":"S. Ben-David","year":"2008","unstructured":"Ben-David S, Embedding Finite Automata within Regular Expressions. Theoretical Computer Science, 2008, 404: 202\u2013218","journal-title":"Theoretical Computer Science"},{"key":"3_CR19","series-title":"LNCS","first-page":"1","volume-title":"Proceedings of Haifa Verification Conference","author":"T. Tuerk","year":"2007","unstructured":"Tuerk T, Schneider K, Gordon M. Haifa Verification Conference. In: Proceedings of Haifa Verification Conference. Berlin: Springer, 2007, LNCS, 4383: 1\u201315"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Liu W, Wang J, Chen H, et al. Symbolic model checking apsl. In: Davies J, Li X, ed. Proceedings of Second IEEE International Symposium on Theoretical Aspects of Software Engineering, 2008, 39\u201346","DOI":"10.1109\/TASE.2008.24"}],"container-title":["Frontiers of Computer Science in China"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-009-0003-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11704-009-0003-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-009-0003-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,2]],"date-time":"2021-10-02T11:16:37Z","timestamp":1633173397000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11704-009-0003-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,3]]},"references-count":20,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2009,3]]}},"alternative-id":["3"],"URL":"https:\/\/doi.org\/10.1007\/s11704-009-0003-9","relation":{},"ISSN":["1673-7350","1673-7466"],"issn-type":[{"value":"1673-7350","type":"print"},{"value":"1673-7466","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,3]]}}}