{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T04:05:28Z","timestamp":1746331528366,"version":"3.40.4"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319085869"},{"type":"electronic","value":"9783319085876"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08587-6_16","type":"book-chapter","created":{"date-parts":[[2014,7,2]],"date-time":"2014-07-02T03:38:32Z","timestamp":1404272312000},"page":"224-239","source":"Crossref","is-referenced-by-count":9,"title":["QBF Encoding of Temporal Properties and QBF-Based Verification"],"prefix":"10.1007","author":[{"given":"Wenhui","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS\/ETAPS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)","DOI":"10.1007\/3-540-49059-0_14"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimmatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded Model Checking. Advances in Computers, vol.\u00a058. Academic Press (2003)","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, J.: Symbolic model checking: 1020 states and beyond. LICS, pp. 428\u2013439 (1990)","DOI":"10.1109\/LICS.1990.113767"},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/3-540-48683-6_44","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"1999","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NUSMV: A New Symbolic Model Verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 495\u2013499. Springer, Heidelberg (1999)"},{"key":"16_CR5","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. The MIT Press (1999)"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"591","DOI":"10.1007\/978-3-642-38768-5_52","volume-title":"Computing and Combinatorics","author":"Z. Duan","year":"2013","unstructured":"Duan, Z., Tian, C., Yang, M., He, J.: Bounded Model Checking for Propositional Projection Temporal Logic. In: Du, D.-Z., Zhang, G. (eds.) COCOON 2013. LNCS, vol.\u00a07936, pp. 591\u2013602. Springer, Heidelberg (2013)"},{"issue":"3","key":"16_CR7","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E.A. Emerson","year":"1982","unstructured":"Emerson, E.A., Clarke, E.M.: Using Branching-time Temporal Logics to Synthesize Synchronization Skeletons. Sci. of Comp. Prog.\u00a02(3), 241\u2013266 (1982)","journal-title":"Sci. of Comp. Prog."},{"issue":"1","key":"16_CR8","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"Emerson, E.A., Halpern, J.Y.: \u201cSometimes\u201d and \u201cNot Never\u201d revisited: on branching versus linear time temporal logic. J. ACM\u00a033(1), 151\u2013178 (1986)","journal-title":"J. ACM"},{"key":"16_CR9","unstructured":"Goultiaeva, A., Van Gelder, A., Bacchus, F.: A Uniform Approach for Generating Proofs and Strategies for Both True and False QBF Formulas. In: IJCAI 2011, pp. 546\u2013553 (2011)"},{"key":"16_CR10","unstructured":"Hoffmann, J., Gomes, C.P., Selman, B., Kautz, H.A.: SAT Encodings of State-Space Reachability Problems in Numeric Domains. In: IJCAI 2007, pp. 1918\u20131923 (2007)"},{"issue":"5","key":"16_CR11","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker Spin. IEEE Transactions on Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"7-8","key":"16_CR12","doi-asserted-by":"publisher","first-page":"779","DOI":"10.1016\/j.scico.2011.02.003","volume":"77","author":"S. Kemper","year":"2012","unstructured":"Kemper, S.: SAT-based verification for timed component connectors. Sci. Comput. Program.\u00a077(7-8), 779\u2013798 (2012)","journal-title":"Sci. Comput. Program."},{"key":"16_CR13","unstructured":"Kontchakov, R., Pulina, L., Sattler, U., Schneider, T., Selmer, P., Wolter, F., Zakharyaschev, M.: Minimal Module Extraction from DL-Lite Ontologies Using QBF Solvers. In: IJCAI 2009, pp. 836\u2013841 (2009)"},{"key":"16_CR14","first-page":"135","volume":"51","author":"W. Penczek","year":"2002","unstructured":"Penczek, W., Wozna, B., Zbrzezny, A.: Bounded Model Checking for the Universal Fragment of CTL. Fundamenta Informaticae\u00a051, 135\u2013156 (2002)","journal-title":"Fundamenta Informaticae"},{"issue":"1","key":"16_CR15","doi-asserted-by":"crossref","first-page":"65","DOI":"10.3233\/FUN-2004-63104","volume":"63","author":"B. Wozna","year":"2004","unstructured":"Wozna, B.: ATCL* properties and Bounded Model Checking. Fundam. Inform.\u00a063(1), 65\u201387 (2004)","journal-title":"Fundam. Inform."},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publisher (1993)","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Peled, D.A.: Software Reliability Methods. Springer (2001)","DOI":"10.1007\/978-1-4757-3540-6"},{"issue":"3","key":"16_CR18","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0020-0190(81)90106-X","volume":"12","author":"G.L. Peterson","year":"1981","unstructured":"Peterson, G.L.: Myths About the Mutual Exclusion Problem. Information Processing Letters\u00a012(3), 115\u2013116 (1981)","journal-title":"Information Processing Letters"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/978-3-642-10373-5_15","volume-title":"Formal Methods and Software Engineering","author":"W. Zhang","year":"2009","unstructured":"Zhang, W.: Bounded Semantics of CTL and SAT-based Verification. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol.\u00a05885, pp. 286\u2013305. Springer, Heidelberg (2009)"},{"key":"16_CR20","unstructured":"Zhang, W.: Bounded Semantics of CTL. Institute of Software, Chinese Academy of Sciences. Technical Report ISCAS-LCS-10-16 (2010)"},{"key":"16_CR21","unstructured":"Zhang, W.: VERDS modeling language, http:\/\/lcs.ios.ac.cn\/~zwh\/verds\/"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08587-6_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T16:41:20Z","timestamp":1746290480000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08587-6_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319085869","9783319085876"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08587-6_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}