{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:01:07Z","timestamp":1725490867086},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540735946"},{"type":"electronic","value":"9783540735953"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73595-3_24","type":"book-chapter","created":{"date-parts":[[2007,8,30]],"date-time":"2007-08-30T09:31:33Z","timestamp":1188466293000},"page":"346-361","source":"Crossref","is-referenced-by-count":11,"title":["Encodings of Bounded LTL Model Checking in Effectively Propositional Logic"],"prefix":"10.1007","author":[{"given":"Juan Antonio","family":"Navarro-P\u00e9rez","sequence":"first","affiliation":[]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","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.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol.\u00a01579, Springer, Heidelberg (1999)"},{"key":"24_CR2","doi-asserted-by":"crossref","unstructured":"Biere, A., Heljanko, K., Junttila, T., Latvala, T., Schuppan, V.: Linear encodings of bounded LTL model checking. Logical Methods in Computer Science 2(5:5) (2006)","DOI":"10.2168\/LMCS-2(5:5)2006"},{"key":"24_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"436","DOI":"10.1007\/3-540-44585-4_43","volume-title":"Computer Aided Verification","author":"F. Copty","year":"2001","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: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 436\u2013453. Springer, Heidelberg (2001)"},{"key":"24_CR5","doi-asserted-by":"publisher","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\u00a05, 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"issue":"1","key":"24_CR6","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2005.07.016","volume":"144","author":"M. Jehle","year":"2006","unstructured":"Jehle, M., Johannsen, J., Lange, M., Rachinsky, N.: Bounded model checking for all regular properties. Electr. Notes Theor. Comput. Sci.\u00a0144(1), 3\u201318 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"24_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"186","DOI":"10.1007\/978-3-540-30494-4_14","volume-title":"Formal Methods in Computer-Aided Design","author":"T. Latvala","year":"2004","unstructured":"Latvala, T., Biere, A., Heljanko, K., Junttila, T.: Simple bounded LTL model checking. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 186\u2013200. Springer, Heidelberg (2004)"},{"key":"24_CR8","unstructured":"Martin, A.J.: The design of a self-timed circuit for distributed mutual exclusion. In: Fuchs, H. (ed.) Proceedings of the 1985 Chapel Hill Conference on Very Large Scale Integration (1985)"},{"key":"24_CR9","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking: An Approach to the State Explosion Problem","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"24_CR10","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. International Journal on Software Tools for Technology Transfer (STTT)\u00a07, 156\u2013173 (2005)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"issue":"1","key":"24_CR11","doi-asserted-by":"publisher","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 for safety properties. Formal Methods in System Design\u00a024(1), 5\u201324 (2004)","journal-title":"Formal Methods in System Design"},{"issue":"1","key":"24_CR12","first-page":"35","volume":"19","author":"G. Sutcliffe","year":"2006","unstructured":"Sutcliffe, G., Suttner, C.: The state of CASC. AI Communications\u00a019(1), 35\u201348 (2006)","journal-title":"AI Communications"},{"issue":"2","key":"24_CR13","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.B.: The TPTP problem library: CNF release v1.2.1. Journal of Automated Reasoning\u00a021(2), 177\u2013203 (1998)","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-21"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73595-3_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T09:53:05Z","timestamp":1619517185000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73595-3_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540735946","9783540735953"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73595-3_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}