{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T05:13:35Z","timestamp":1771046015816,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642103728","type":"print"},{"value":"9783642103735","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-10373-5_15","type":"book-chapter","created":{"date-parts":[[2009,11,16]],"date-time":"2009-11-16T11:45:27Z","timestamp":1258371927000},"page":"286-305","source":"Crossref","is-referenced-by-count":10,"title":["Bounded Semantics of CTL and SAT-Based Verification"],"prefix":"10.1007","author":[{"given":"Wenhui","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"15_CR1","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/j.entcs.2005.07.019","volume":"144","author":"M. Awedh","year":"2006","unstructured":"Awedh, M., Somenzi, F.: Termination Criteria for Bounded Model Checking: Extensions and Comparison. Electr. Notes Theor. Comput. Sci.\u00a0144(1), 51\u201366 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"15_CR2","series-title":"Advances in Computers","volume-title":"Bounded Model Checking","author":"A. Biere","year":"2003","unstructured":"Biere, A., Cimmatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded Model Checking. Advances in Computers, vol.\u00a058. Academic Press, London (2003)"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimmatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"15_CR4","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"},{"issue":"8","key":"15_CR5","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R. Bryant","year":"1986","unstructured":"Bryant, R.: Graph based algorithms for boolean function manipulation. IEEE Transaction on Computers\u00a035(8), 677\u2013691 (1986)","journal-title":"IEEE Transaction on Computers"},{"issue":"2","key":"15_CR6","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1109\/12.73590","volume":"40","author":"R.E. Bryant","year":"1991","unstructured":"Bryant, R.E.: On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication. IEEE Trans. Computers\u00a040(2), 205\u2013213 (1991)","journal-title":"IEEE Trans. Computers"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Bryant, R.: Binary decision diagrams and beyond: enabling technologies for formal verification. In: CAD 1995, pp. 236\u2013243 (1995)","DOI":"10.1109\/ICCAD.1995.480018"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Chen, W., Zhang, W.: Bounded Model Checking of ACTL formulae. In: TASE 2009, pp. 90\u201399 (2009)","DOI":"10.1109\/TASE.2009.15"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/978-3-540-24622-0_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"E.M. Clarke","year":"2004","unstructured":"Clarke, E.M., Kroening, D., Ouaknine, J., Strichman, O.: Completeness and Complexity of Bounded Model Checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 85\u201396. Springer, Heidelberg (2004)"},{"issue":"2","key":"15_CR10","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/s10009-004-0182-5","volume":"7","author":"E.M. Clarke","year":"2005","unstructured":"Clarke, E.M., Kroening, D., Ouaknine, J., Strichman, O.: Computational challenges in bounded model checking. STTT\u00a07(2), 174\u2013183 (2005)","journal-title":"STTT"},{"key":"15_CR11","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (1999)"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. Een","year":"2004","unstructured":"Een, N., Sorensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"issue":"3","key":"15_CR13","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E. Allen Emerson","year":"1982","unstructured":"Allen Emerson, E., Clarke, E.M.: Using Branching-time Temporal Logics to Synthesize Synchronization Skeletons. Science of Computer Programming\u00a02(3), 241\u2013266 (1982)","journal-title":"Science of Computer Programming"},{"issue":"1","key":"15_CR14","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E. Allen Emerson","year":"1986","unstructured":"Allen Emerson, E., Halpern, J.Y.: Sometimes and Not Never revisited: on branching versus linear time temporal logic. J. ACM\u00a033(1), 151\u2013178 (1986)","journal-title":"J. ACM"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Gorgonio, K., Xia, F.: Modeling and verifying asynchronous communication mechanisms using coloured Petri nets. In: ACSD 2008, pp. 138\u2013147 (2008)","DOI":"10.1109\/ACSD.2008.4574605"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1007\/11513988_10","volume-title":"Computer Aided Verification","author":"K. Heljanko","year":"2005","unstructured":"Heljanko, K., Junttila, T.A., Latvala, T.: Incremental and complete bounded model checking for full PLTL. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 98\u2013111. Springer, Heidelberg (2005)"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/3-540-36384-X_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D. Kroening","year":"2003","unstructured":"Kroening, D., Strichman, O.: Efficient computation of recurrence diameters. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 298\u2013309. Springer, Heidelberg (2003)"},{"issue":"1","key":"15_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/7351.7352","volume":"5","author":"L. Lamport","year":"1987","unstructured":"Lamport, L.: A fast mutual exclusion algorithm. ACM Transactions on Computer Systems\u00a05(1), 1\u201311 (1987)","journal-title":"ACM Transactions on Computer Systems"},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science","first-page":"468","volume-title":"Theory and Applications of Satisfiability Testing","author":"D. Berre Le","year":"2003","unstructured":"Le Berre, D., Simon, L., Tacchella, A.: Challenges in the QBF arena: the SAT 2003 evaluation of QBF solvers. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 468\u2013485. Springer, Heidelberg (2003)"},{"key":"15_CR20","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"15_CR21","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":"2","key":"15_CR22","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/s10009-004-0183-4","volume":"7","author":"M.R. Prasad","year":"2005","unstructured":"Prasad, M.R., Biere, A., Gupta, A.: A survey of recent advances in SAT-based formal verification. STTT\u00a07(2), 156\u2013173 (2005)","journal-title":"STTT"},{"issue":"1","key":"15_CR23","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/s11390-007-9004-z","volume":"22","author":"Z.-H. Tao","year":"2007","unstructured":"Tao, Z.-H., Zhou, C.-H., Chen, Z., Wang, L.-F.: Bounded Model Checking of CTL. J. Comput. Sci. Technol.\u00a022(1), 39\u201343 (2007)","journal-title":"J. Comput. Sci. Technol."},{"issue":"1","key":"15_CR24","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."},{"issue":"1","key":"15_CR25","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/s11390-009-9208-5","volume":"24","author":"L. Xu","year":"2009","unstructured":"Xu, L., Chen, W., Xu, Y., Zhang, W.: Improved Bounded Model Checking for Universal Fragment of CTL. Journal of Computer Science and Technology\u00a024(1), 96\u2013109 (2009)","journal-title":"Journal of Computer Science and Technology"},{"key":"15_CR26","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1109\/TASE.2007.22","volume-title":"Proceedings of the 1st Joint IEEE\/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE 2007)","author":"Y. Xu","year":"2007","unstructured":"Xu, Y., Chen, W., Xu, L., Zhang, W.: Evaluation of SAT-based Bounded Model Checking of ACTL Properties. In: Proceedings of the 1st Joint IEEE\/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE 2007), pp. 339\u2013348. IEEE Computer Society Press, Los Alamitos (2007)"},{"key":"15_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/978-3-540-70952-7_18","volume-title":"Formal Methods: Applications and Technology","author":"W. Zhang","year":"2007","unstructured":"Zhang, W.: SAT-based verification of LTL formulas. In: Brim, L., Haverkort, B.R., Leucker, M., van de Pol, J. (eds.) FMICS 2006 and PDMC 2006. LNCS, vol.\u00a04346, pp. 277\u2013292. Springer, Heidelberg (2007)"},{"key":"15_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"556","DOI":"10.1007\/978-3-540-75867-9_70","volume-title":"Computer Aided Systems Theory \u2013 EUROCAST 2007","author":"W. Zhang","year":"2007","unstructured":"Zhang, W.: Verification of ACTL properties by bounded model checking. In: Moreno D\u00edaz, R., Pichler, F., Quesada Arencibia, A. (eds.) EUROCAST 2007. LNCS, vol.\u00a04739, pp. 556\u2013563. Springer, Heidelberg (2007)"},{"key":"15_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-540-76650-6_12","volume-title":"Formal Methods and Software Engineering","author":"W. Zhang","year":"2007","unstructured":"Zhang, W.: Model checking with SAT-based characterization of ACTL formulas. In: Butler, M., Hinchey, M.G., Larrondo-Petrie, M.M. (eds.) ICFEM 2007. LNCS, vol.\u00a04789, pp. 191\u2013211. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-10373-5_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,13]],"date-time":"2025-02-13T07:22:33Z","timestamp":1739431353000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-10373-5_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642103728","9783642103735"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-10373-5_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}