{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:18:15Z","timestamp":1725491895788},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540730989"},{"type":"electronic","value":"9783540730996"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73099-6_7","type":"book-chapter","created":{"date-parts":[[2007,9,14]],"date-time":"2007-09-14T07:04:02Z","timestamp":1189753442000},"page":"60-72","source":"Crossref","is-referenced-by-count":0,"title":["Bounded Model Checking with Description Logic Reasoning"],"prefix":"10.1007","author":[{"given":"Shoham","family":"Ben-David","sequence":"first","affiliation":[]},{"given":"Richard","family":"Trefler","sequence":"additional","affiliation":[]},{"given":"Grant","family":"Weddell","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","volume-title":"The Description Logic Handbook","author":"F. Baader","year":"2003","unstructured":"Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.: The Description Logic Handbook. Cambridge University Press, Cambridge (2003)"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028744","volume-title":"Computer Aided Verification","author":"I. Beer","year":"1998","unstructured":"Beer, I., Ben-David, S., Landver, A.: On-the-fly model checking of RCTL formulas. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, Springer, Heidelberg (1998)"},{"key":"7_CR3","unstructured":"Ben-David, S., Trefler, R., Weddell, G.: Model checking the basic modalities of CTL with description logic. In: Proc. International Workshop on Description Logics, pp. 223\u2013230 (2006)"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol.\u00a01579, Springer, Heidelberg (1999)"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Bryant, R.: Graph-based algorithms for boolean function manipulation. In IEEE Transactions on Computers, vol. c-35(8) (1986)","DOI":"10.1109\/TC.1986.1676819"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model verifier. In: Computer Aided Verification, pp. 495\u2013499, (July 1999)","DOI":"10.1007\/3-540-48683-6_44"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E. Clarke","year":"1982","unstructured":"Clarke, E., Emerson, E.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logics of Programs. LNCS, vol.\u00a0131, Springer, Heidelberg (1982)"},{"key":"7_CR8","volume-title":"Model Checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (2000)"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Hanna, Z., Katz, J.: Bounded model checking with QBF. In: Eighth International Conference on Theory and Applications of Satisfiability Testing, pp. 408\u2013414, (June 2005)","DOI":"10.1007\/11499107_32"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"Database Programming Languages","author":"A. Dovier","year":"2002","unstructured":"Dovier, A., Quintarelli, E.: Model checking based data retrieval. In: Ghelli, G., Grahne, G. (eds.) DBPL 2001. LNCS, vol.\u00a02397, Springer, Heidelberg (2002)"},{"key":"7_CR11","volume-title":"Logic-Based Artificial Intelligence","author":"G. Gottlob","year":"2000","unstructured":"Gottlob, G., Gr\u00e4del, E., Veith, H.: Linear Time Datalog for Branching Time Logic (chapter\u00a019). In: Minker, J. (ed.) Logic-Based Artificial Intelligence, Kluwer, Boston (2000)"},{"issue":"1","key":"7_CR12","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1145\/504077.504079","volume":"3","author":"G. Gottlob","year":"2002","unstructured":"Gottlob, G., Gr\u00e4del, E., Veith, H.: Datalog LITE: a deductive query language with linear time model checking. Computational Logic\u00a03(1), 42\u201379 (2002)","journal-title":"Computational Logic"},{"key":"7_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/3-540-69778-0_30","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"I. Horrocks","year":"1998","unstructured":"Horrocks, I.: The FaCT system. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol.\u00a01397, pp. 307\u2013312. Springer, Heidelberg (1998)"},{"key":"7_CR14","unstructured":"Horrocks, I., Tobies, S.: Reasoning with axioms: Theory and practice. In: Proc. of the 7th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR 2000), pp. 285\u2013296 (2000)"},{"key":"7_CR15","unstructured":"Jussila, T., Biere, A.: Compressing bmc encodings with QBF. In: Fourth International Workshop on Bounded Model Checking, pp. 27\u201339, (August 2006)"},{"key":"7_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K. McMillan","year":"1993","unstructured":"McMillan, K.: Symbolic Model Checking. Kluwer Academic Publishers, Norwell (1993)"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient sat solver. In: 38th Design Automation Conference, pp. 530\u2013535 (June 2001)","DOI":"10.1145\/378239.379017"},{"key":"7_CR18","unstructured":"NuSMV examples collection, \n \n http:\/\/nusmv.irst.itc.it\/examples\/examples.html"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th IEEE Symposium on Foundation of Computer Science, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Quielle, J., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: 5th International Symposium on Programming (1982)","DOI":"10.1007\/3-540-11494-7_22"},{"key":"7_CR21","unstructured":"Sahasrabudhe, M.: SQL-based CTL model checking for telephony feature interactions. In: A Master Thesis, Univesity of Waterloo, Ontario, Canada (2004)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73099-6_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:00:02Z","timestamp":1619517602000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73099-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540730989","9783540730996"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73099-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}