{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:21:01Z","timestamp":1747592461676},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Comput. Sci. Technol."],"published-print":{"date-parts":[[2009,1]]},"DOI":"10.1007\/s11390-009-9208-5","type":"journal-article","created":{"date-parts":[[2009,3,26]],"date-time":"2009-03-26T14:12:18Z","timestamp":1238076738000},"page":"96-109","source":"Crossref","is-referenced-by-count":4,"title":["Improved Bounded Model Checking for the Universal Fragment of CTL"],"prefix":"10.1007","volume":"24","author":[{"given":"Liang","family":"Xu","sequence":"first","affiliation":[]},{"given":"Wei","family":"Chen","sequence":"additional","affiliation":[]},{"given":"Yan-Yan","family":"Xu","sequence":"additional","affiliation":[]},{"given":"Wen-Hui","family":"Zhang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2009,3,1]]},"reference":[{"key":"9208_CR1","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke E, Fujita M, Zhu Y. Symbolic model checking using SAT procedures instead of BDDs. In Proc. DAC, New Orleans, LA, USA, June 21\u201325, 1999, pp.317\u2013320.","DOI":"10.21236\/ADA360973"},{"key":"9208_CR2","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke E, Zhu Y. Symbolic model checking without BDDs. In Proc. TACAS, Amsterdam, The Netherlands, March 22\u201328, 1999, pp.193\u2013207.","DOI":"10.21236\/ADA360973"},{"issue":"1\/2","key":"9208_CR3","first-page":"135","volume":"51","author":"W Penczek","year":"2002","unstructured":"Penczek W, Wo\u0178na B, Zbrzezny A. Bounded model checking for the universal fragment of CTL. Fundamenta Informaticae, 2002, 51(1\/2): 135\u2013156.","journal-title":"Fundamenta Informaticae"},{"key":"9208_CR4","doi-asserted-by":"crossref","unstructured":"Biere A, Clarke E, Raimi R, Zhu Y. Verifying safety properties of a Power PC microprocessor using symbolic model checking without BDDs. In Proc. CAV, Trento, Italy, July 6\u201310, 1999, pp.60\u201371.","DOI":"10.1007\/3-540-48683-6_8"},{"key":"9208_CR5","doi-asserted-by":"crossref","unstructured":"Copty F, Fix L, Fraer R, Giunchiglia E, Kamhi G, Tacchella A, Vardi M Y. Benefits of bounded model checking at an industrial setting. In Proc. CAV, Paris, France, July 18\u201322, 2001, pp.436\u2013453.","DOI":"10.1007\/3-540-44585-4_43"},{"issue":"1","key":"9208_CR6","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1023\/B:FORM.0000004785.67232.f8","volume":"24","author":"O Strichman","year":"2004","unstructured":"Strichman O. Accelerating bounded model checking of safety properties. Formal Methods in System Design, 2004, 24(1): 5\u201324.","journal-title":"Formal Methods in System Design"},{"key":"9208_CR7","doi-asserted-by":"crossref","unstructured":"Jain H, Bartzis C, Clarke E M. Satisfiability checking of non-clausal formulas using general matings. In Proc. SAT, Seattle, WA, USA, August 12\u201315, 2006, pp.75\u201389.","DOI":"10.1007\/11814948_10"},{"issue":"3","key":"9208_CR8","doi-asserted-by":"crossref","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. Science of Computer Programming, 1982, 2(3): 241\u2013266.","journal-title":"Science of Computer Programming"},{"key":"9208_CR9","volume-title":"Model Checking","author":"E M Clarke","year":"1999","unstructured":"Clarke E M, Grunberg O, Peled D A. Model Checking. Cambridge, Massachusetts, London, England: The MIT Press, 1999."},{"issue":"3","key":"9208_CR10","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1006\/jcss.2000.1734","volume":"62","author":"F Buccafurri","year":"2001","unstructured":"Buccafurri F, Eiter T, Gottlob G, Leone N. On ACTL formulae having linear counterexamples. Journal of Computer and System Sciences, 2001, 62(3): 463\u2013515.","journal-title":"Journal of Computer and System Sciences"},{"key":"9208_CR11","doi-asserted-by":"crossref","unstructured":"Pieprzyk J, Cheng Xin Qu. Rotation-symmetric functions and fast hashing. In Proc. ACISP, Brisbane, Queensland, Australia, July 1998, pp.169\u2013180.","DOI":"10.1007\/BFb0053731"},{"key":"9208_CR12","doi-asserted-by":"crossref","unstructured":"E\u00e9n N, S\u00f6rensson N. An extensible SAT-solver. In Proc. SAT, Santa Margherita Ligure, Italy, May 5\u20138, 2003, pp.502\u2013518.","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"9208_CR13","doi-asserted-by":"crossref","unstructured":"E\u00e9n N, S\u00f6rensson N. Effective preprocessing in SAT through variable and clause elimination. In Proc. SAT, St. Andrews, UK, June 19\u201323, 2005, pp.61\u201375.","DOI":"10.1007\/11499107_5"},{"issue":"4","key":"9208_CR14","doi-asserted-by":"crossref","first-page":"543","DOI":"10.1016\/S1571-0661(05)82542-3","volume":"89","author":"N E\u00e9n","year":"2003","unstructured":"E\u00e9n N, S\u00f6rensson N. Temporal induction by incremental SAT solving. Electronic Notes in Theoretical Computer Science, 2003, 89(4): 543\u2013560.","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"9208_CR15","doi-asserted-by":"crossref","unstructured":"Xu Y, Chen W, Xu L, Zhang W. Evaluation of SAT-based bounded model checking of ACTL properties. In Proc. TASE, Shanghai, China, June 5\u20138, 2007, pp.339\u2013348.","DOI":"10.1109\/TASE.2007.22"},{"key":"9208_CR16","doi-asserted-by":"crossref","unstructured":"Zhang W. Verification of ACTL properties by bounded model checking. In Proc. EUROCAST, Gran Canaria, Spain, February 12\u201316, 2007, pp.199\u2013202.","DOI":"10.1007\/978-3-540-75867-9_70"},{"key":"9208_CR17","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3540-6","volume-title":"Software Reliability Methods","author":"D A Peled","year":"2001","unstructured":"Peled D A. Software Reliability Methods. New York: Springer, USA, 2001."},{"key":"9208_CR18","doi-asserted-by":"crossref","unstructured":"Zhou C, Ding D. Improved SAT based bounded model checking. In Proc. TAMC, Beijing, China, May 15\u201320, 2006, pp.611\u2013620.","DOI":"10.1007\/11750321_58"},{"key":"9208_CR19","doi-asserted-by":"crossref","unstructured":"Penczek W, Wo\u0178na B, Zbrzezny A. Towards bounded model checking for the universal fragment of TCTL. In Proc. FTRTFT, Oldenburg, Germany, September 9\u201312, 2002, pp.265\u2013290.","DOI":"10.1007\/3-540-45739-9_17"},{"key":"9208_CR20","doi-asserted-by":"crossref","unstructured":"Audemard G, Cimatti A, Kornilowicz A, Sebastiani R. Bounded model checking for timed systems. In Proc. FORTE, Houston, Texas, USA, November 11\u201314, 2002, pp.243\u2013259.","DOI":"10.1007\/3-540-36135-9_16"},{"key":"9208_CR21","doi-asserted-by":"crossref","unstructured":"Markey N, Schnoebelen P. Symbolic model checking for simply-timed systems. In Proc. FTRTFT, Grenoble, France, September 22\u201324, 2004, pp.102\u2013117.","DOI":"10.1007\/978-3-540-30206-3_9"},{"key":"9208_CR22","doi-asserted-by":"crossref","unstructured":"Sheini H M, Sakallah K A. From propositional satisfiability to satisfiability modulo theories. In Proc. SAT, Seattle, WA, USA, August 12\u201315, 2006, pp.1\u20139.","DOI":"10.1007\/11814948_1"}],"container-title":["Journal of Computer Science and Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-009-9208-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11390-009-9208-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-009-9208-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T14:32:41Z","timestamp":1559399561000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11390-009-9208-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,1]]},"references-count":22,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2009,1]]}},"alternative-id":["9208"],"URL":"https:\/\/doi.org\/10.1007\/s11390-009-9208-5","relation":{},"ISSN":["1000-9000","1860-4749"],"issn-type":[{"value":"1000-9000","type":"print"},{"value":"1860-4749","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,1]]}}}