{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T23:26:18Z","timestamp":1649028378251},"reference-count":15,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"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":[[2007,1]]},"DOI":"10.1007\/s11390-007-9004-z","type":"journal-article","created":{"date-parts":[[2007,2,9]],"date-time":"2007-02-09T18:31:12Z","timestamp":1171045872000},"page":"39-43","source":"Crossref","is-referenced-by-count":4,"title":["Bounded Model Checking of CTL"],"prefix":"10.1007","volume":"22","author":[{"given":"Zhi-Hong","family":"Tao","sequence":"first","affiliation":[]},{"given":"Cong-Hua","family":"Zhou","sequence":"additional","affiliation":[]},{"given":"Zhong","family":"Chen","sequence":"additional","affiliation":[]},{"given":"Li-Fu","family":"Wang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2007,2,14]]},"reference":[{"key":"9004_CR1","unstructured":"Clarke E M, Grumberg O, Peled D. Model Checking. MIT Press, 2000."},{"issue":"3","key":"9004_CR2","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/BF01257083","volume":"20","author":"M Ben-Ari","year":"1983","unstructured":"Ben-Ari M, Manna Z, Pnueli A. The temporal logic of branching time. Acta Information, 1983, 20(3): 207\u2013226.","journal-title":"Acta Information"},{"issue":"1","key":"9004_CR3","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A Pnueli","year":"1981","unstructured":"Pnueli A. A temporal logic of concurrent programs. Theoretical Computer Science, 1981, 13(1): 45\u201360.","journal-title":"Theoretical Computer Science"},{"key":"9004_CR4","doi-asserted-by":"crossref","unstructured":"McMillan K L. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"9004_CR5","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J R Burch","year":"1992","unstructured":"Burch J R, Clarke E M, McMillan K L. Symbolic model checking: 1020 states and beyond. Information and Computation, 1992, 98: 142\u2013170.","journal-title":"Information and Computation"},{"key":"9004_CR6","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R E Bryant","year":"1986","unstructured":"Bryant R E. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, 1986, 35: 677\u2013691.","journal-title":"IEEE Transactions on Computers"},{"key":"9004_CR7","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke E M, Zhu Y. Symbolic model checking without BDDs. In Proc. Tools and Algorithms for the Analysis and Construction of Systems (TACAS\u201999), LNCS 1579, Springer-Verlag, 1999, pp. 193\u2013207.","DOI":"10.1007\/3-540-49059-0_14"},{"issue":"1","key":"9004_CR8","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1007\/s11390-005-0004-6","volume":"20","author":"X W Li","year":"2005","unstructured":"Li X W, Li G H, Shao M. Formal verification techniques based on Boolean satisfiability problem. Journal of Computer Science and Technology, 2005, 20(1): 38\u201347.","journal-title":"Journal of Computer Science and Technology"},{"issue":"2","key":"9004_CR9","first-page":"1","volume":"62","author":"B Wozna","year":"2004","unstructured":"Wozna B. ACTL* properties and bounded model checking. Fundamenta Informaticae, 2004, 62(2): 1\u201323.","journal-title":"Fundamenta Informaticae"},{"key":"9004_CR10","unstructured":"Kleine B\u00fcing H, Lettmann H. Propositional Logic: Deduction and Algorithms, Cambridge University Press, 1999."},{"key":"9004_CR11","unstructured":"Hilbert D, Ackermann W. Principles of Mathematical Logic. New York, Chelsea, 1950."},{"key":"9004_CR12","unstructured":"Quine W V Q. Methods of Logic. Newyork: Heny Holt, 1959."},{"key":"9004_CR13","doi-asserted-by":"crossref","unstructured":"Anil Nerode, Richard A Shore. Logic for Applications. Spinger, 1997.","DOI":"10.1007\/978-1-4612-0649-1"},{"key":"9004_CR14","first-page":"408","volume-title":"Proc. International Conference on Theory and Applications of Satisfiability Testing (SAT\u201905), LNCS 3569","author":"N Dershowitz","year":"2005","unstructured":"Dershowitz N, Hanna Z, Katz J. Bounded Model Checking with QBF. In Proc. International Conference on Theory and Applications of Satisfiability Testing (SAT\u201905), LNCS 3569, Springer-Verlag, St. Andrews, UK, 2005, pp. 408\u2013414."},{"issue":"7","key":"9004_CR15","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis M, Logemann G, Loveland D. A machine program for theorem-proving. Communications of the ACM, 1962, 5(7): 394\u2013397.","journal-title":"Communications of the ACM"}],"container-title":["Journal of Computer Science and Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-007-9004-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11390-007-9004-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-007-9004-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T14:32:38Z","timestamp":1559399558000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11390-007-9004-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,1]]},"references-count":15,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2007,1]]}},"alternative-id":["9004"],"URL":"https:\/\/doi.org\/10.1007\/s11390-007-9004-z","relation":{},"ISSN":["1000-9000","1860-4749"],"issn-type":[{"value":"1000-9000","type":"print"},{"value":"1860-4749","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,1]]}}}