{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T21:51:07Z","timestamp":1725573067646},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540242970"},{"type":"electronic","value":"9783540305798"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-30579-8_25","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T16:45:34Z","timestamp":1292863534000},"page":"380-395","source":"Crossref","is-referenced-by-count":23,"title":["Simple Is Better: Efficient Bounded Model Checking for Past LTL"],"prefix":"10.1007","author":[{"given":"Timo","family":"Latvala","sequence":"first","affiliation":[]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[]},{"given":"Keijo","family":"Heljanko","sequence":"additional","affiliation":[]},{"given":"Tommi","family":"Junttila","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","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., Cimatti, 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":"25_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/3-540-48683-6_8","volume-title":"Computer Aided Verification","author":"A. Biere","year":"1999","unstructured":"Biere, A., Clarke, E., Raimi, R., Zhu, Y.: Verifying Safety Properties of a PowerPCTM Microprocessor Using Symbolic Model Checking without BDDs. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 60\u201371. Springer, Heidelberg (1999)"},{"key":"25_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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., Fracer, 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":"25_CR4","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 of safety properties. Formal Methods in System Design\u00a024, 5\u201324 (2004)","journal-title":"Formal Methods in System Design"},{"key":"25_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-46002-0_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Havelund","year":"2002","unstructured":"Havelund, K., Ro\u015fu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 342\u2013356. Springer, Heidelberg (2002)"},{"key":"25_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1007\/978-3-540-45138-9_38","volume-title":"Mathematical Foundations of Computer Science 2003","author":"P. Gastin","year":"2003","unstructured":"Gastin, P., Oddoux, D.: LTL with past and two-way very-weak alternating automata. In: Rovan, B., Vojt\u00e1\u0161, P. (eds.) MFCS 2003. LNCS, vol.\u00a02747, pp. 439\u2013448. Springer, Heidelberg (2003)"},{"key":"25_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/3-540-36577-X_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Benedetti","year":"2003","unstructured":"Benedetti, M., Cimatti, A.: Bounded model checking for past LTL. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 18\u201333. Springer, Heidelberg (2003)"},{"key":"25_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1007\/3-540-15648-8_16","volume-title":"Logics of Programs","author":"O. Lichtenstein","year":"1985","unstructured":"Lichtenstein, O., Pnueli, A., Zuck, L.D.: The glory of the past. In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol.\u00a0193, pp. 196\u2013218. Springer, Heidelberg (1985)"},{"key":"25_CR9","unstructured":"Kamp, J.: Tense Logic and the Theory of Linear Order. PhD thesis, University of California, Los Angeles, California (1968)"},{"key":"25_CR10","first-page":"163","volume-title":"Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages","author":"D.M. Gabbay","year":"1980","unstructured":"Gabbay, D.M., Pnueli, A., Shelah, S., Stavi, J.: On the temporal basis of fairness. In: Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages, Las Vegas, Nevada, pp. 163\u2013173. ACM, New York (1980)"},{"key":"25_CR11","first-page":"383","volume-title":"17th IEEE Symp. Logic in Computer Science (LICS 2002)","author":"F. Laroussinie","year":"2002","unstructured":"Laroussinie, F., Markey, N., Schnoebelen, P.: Temporal logic with forgettable past. In: 17th IEEE Symp. Logic in Computer Science (LICS 2002), pp. 383\u2013392. IEEE Computer Society Press, Los Alamitos (2002)"},{"key":"25_CR12","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. Journal of the ACM\u00a032, 733\u2013749 (1985)","journal-title":"Journal of the ACM"},{"key":"25_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"25_CR14","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, 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":"25_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/3-540-36126-X_15","volume-title":"Formal Methods in Computer-Aided Design","author":"A. Frisch","year":"2002","unstructured":"Frisch, A., Sheridan, D., Walsh, T.: A fixpoint encoding for bounded model checking. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 238\u2013255. Springer, Heidelberg (2002)"},{"key":"25_CR16","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.: Model checking of safety properties. Formal Methods in System Design\u00a019, 291\u2013314 (2001)","journal-title":"Formal Methods in System Design"},{"key":"25_CR17","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/s100090200070","volume":"4","author":"H. Tauriainen","year":"2002","unstructured":"Tauriainen, H., Heljanko, K.: Testing LTL formula translation into B\u00fcchi automata. STTT - International Journal on Software Tools for Technology Transfer\u00a04, 57\u201370 (2002)","journal-title":"STTT - International Journal on Software Tools for Technology Transfer"},{"key":"25_CR18","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference. IEEE, Los Alamitos (2001)","DOI":"10.1145\/378239.379017"},{"key":"25_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-540-30494-4_18","volume-title":"Formal Methods in Computer-Aided Design","author":"A. Cimatti","year":"2004","unstructured":"Cimatti, A., Roveri, M., Sheridan, D.: Bounded verification of past LTL. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 245\u2013259. Springer, Heidelberg (2004)"},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Temporal induction by incremental SAT solving. In: Encarna\u00e7\u00e3o, J.L. (ed.) Computer Aided Design Modelling, Systems Engineering, CAD-Systems. ENTCS, vol.\u00a089. Elsevier, Amsterdam (1980)","DOI":"10.1016\/S1571-0661(05)82542-3"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30579-8_25.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,15]],"date-time":"2021-11-15T23:48:07Z","timestamp":1637020087000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30579-8_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540242970","9783540305798"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30579-8_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}