{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T19:45:28Z","timestamp":1770752728124,"version":"3.50.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540237389","type":"print"},{"value":"9783540304944","type":"electronic"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30494-4_18","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T18:42:14Z","timestamp":1277836934000},"page":"245-259","source":"Crossref","is-referenced-by-count":21,"title":["Bounded Verification of Past LTL"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Cimatti","sequence":"first","affiliation":[]},{"given":"Marco","family":"Roveri","sequence":"additional","affiliation":[]},{"given":"Daniel","family":"Sheridan","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","unstructured":"Accellera. Accelera Property Specification Language: Reference Manual \u2013 Version 1.0"},{"key":"18_CR2","first-page":"5","volume-title":"Proceedings of the AAAI Spring Symposium Series on Extending Theories of Action: Formal Theory and Practical Applications","author":"F. Bacchus","year":"1995","unstructured":"Bacchus, F., Kabanza, F.: Control strategies in planning. In: Proceedings of the AAAI Spring Symposium Series on Extending Theories of Action: Formal Theory and Practical Applications, Stanford University, CA, USA, March 1995, pp. 5\u201310. AAAI Press, Menlo Park (1995)"},{"key":"18_CR3","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":"18_CR4","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.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"18_CR5","unstructured":"Castro, J., Kolp, M., Mylopoulos, J.: A requirements-driven development methodology. In: Proceedings of the 13th International Conference on Advanced Information Systems Engineering (2001)"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/3-540-48683-6_44","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"1999","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NuSMV: a new Symbolic Model Verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 495\u2013499. Springer, Heidelberg (1999)"},{"key":"18_CR7","volume-title":"Proceedings of the Twelfth International Joint Conference on Artificial Intelligence (IJCAI)","author":"M. Fisher","year":"1991","unstructured":"Fisher, M.: A resolution method for temporal logic. In: Proceedings of the Twelfth International Joint Conference on Artificial Intelligence (IJCAI), August 1991, Morgan Kaufmann, San Francisco (1991)"},{"key":"18_CR8","unstructured":"Fisher, M., No\u00ebl, P.: Transformation and synthesis in MetateM Part I: Propositional MetateM. Technical Report UMCS-92-2-1, Department of Computer Science, University of Manchester, Manchester M13 9PL, England (February 1992)"},{"key":"18_CR9","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 based encoding for bounded model checking. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 238\u2013254. Springer, Heidelberg (2002)"},{"key":"18_CR10","volume-title":"Proceedings of the 11th IEEE International Requirements Engineering Conference","author":"A. Fuxman","year":"2003","unstructured":"Fuxman, A., Liu, L., Pistore, M., Roveri, M., Mylopoulos, J.: Specifying and analyzing early requirements in Tropos: Some experimental results. In: Proceedings of the 11th IEEE International Requirements Engineering Conference, California, USA, September 2003, ACM-Press, Monterey Bay (2003)"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Temporal Logic in Specification","author":"D. Gabbay","year":"1989","unstructured":"Gabbay, D.: The declarative past and imperative future. In: Banieqbal, B., Pnueli, A., Barringer, H. (eds.) Temporal Logic in Specification. LNCS, vol.\u00a0398, Springer-Verlag, Heidelberg (1989)"},{"key":"18_CR12","unstructured":"Gnesi, S., Latella, D., Lenzini, G.: Formal verification of cryptographic protocols using history dependent automata. In: Proceedings of the of the 4th Workshop on Sistemi Distribuiti: Algoritmi, Architetture e Linguaggi (1999)"},{"key":"18_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/3-540-44685-0_35","volume-title":"CONCUR 2001 - Concurrency Theory","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Piterman, N., Vardi, M.: Extended temporal logic revisited. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol.\u00a02154, pp. 519\u2013534. Springer Verlag, Heidelberg (2001)"},{"key":"18_CR14","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1109\/LICS.2002.1029846","volume-title":"Proceedings of the 17th IEEE Symp. Logic in Computer Science (LICS 2002)","author":"F. Laroussinie","year":"2002","unstructured":"Laroussinie, F., Markey, N.: Ph. Schnoebelen. Temporal logic with forgettable past. In: Proceedings of the 17th IEEE Symp. Logic in Computer Science (LICS 2002), Denmark,, July 2002, pp. 383\u2013392. IEEE Comp. Soc. Press, Copenhagen (2002)"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: 39th Design Automation Conference, Las Vegas (June 2001)","DOI":"10.1145\/378239.379017"},{"key":"18_CR16","unstructured":"Sheridan, D.: The optimality of a fast CNF conversion and its use with SAT. Technical Report APES-82-2002, APES Research Group (March 2004), Available from http:\/\/www.dcs.st-and.ac.uk\/~apes\/apesreports.html"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"van Lamsweerde, A.: Goal-oriented requirements engineering: A guided tour. In: Proceedings of the 5th IEEE International Symposium on Requirements Engineering, pp. 249\u2013263 (2001)","DOI":"10.1109\/ISRE.2001.948567"}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30494-4_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T09:57:07Z","timestamp":1740218227000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30494-4_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540237389","9783540304944"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30494-4_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}