{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,14]],"date-time":"2026-01-14T16:43:30Z","timestamp":1768409010299,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540008989","type":"print"},{"value":"9783540365778","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36577-x_3","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:12:04Z","timestamp":1269897124000},"page":"18-33","source":"Crossref","is-referenced-by-count":36,"title":["Bounded Model Checking for Past LTL"],"prefix":"10.1007","author":[{"given":"Marco","family":"Benedetti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"P. A. Abdullah, P. Bjesse, and N. Een. Symbolic Reachability Analysis based on SAT-Solvers. In Sixth Int.nl Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201900), 2000.","DOI":"10.1007\/3-540-46419-0_28"},{"key":"3_CR2","unstructured":"F. Bacchus and F. Kabanza. Control Strategies in Planning. In Proc. of the AAAI Spring Symposium Series on Extending Theories of Action: Formal Theory and Practical Applications, pages 5\u201310, Stanford University, CA, USA, March 1995."},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"J. Baumgartner, A. Kuehlmann, and J. Abraham. Property Checking via Structural Analysis. In Proc. CAV\u201902, volume 2404, pages 151\u2013165, 2002.","DOI":"10.1007\/3-540-45657-0_12"},{"key":"3_CR4","series-title":"Technical Report","volume-title":"Bounded Model Checking for Past LTL","author":"M. Benedetti","year":"2003","unstructured":"M. Benedetti and A. Cimatti. Bounded Model Checking for Past LTL. Technical Report 0301-05, ITC-Irst, Trento, Italy, 2003."},{"key":"3_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Symbolic Model Checking without BDDs","author":"A. Biere","year":"1999","unstructured":"A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic Model Checking without BDDs. LNCS, 1579:193\u2013207, 1999."},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu. Symbolic Model Checking Using SAT Procedures instead of BDDs. In Proc. DAC\u201999, pages 317\u2013320, 1999.","DOI":"10.1145\/309847.309942"},{"key":"3_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.21236\/ADA360973","volume-title":"Verifying Safety Properties of a Power PC Microprocessor Using Symbolic Model Checking without BDDs","author":"A. Biere","year":"1999","unstructured":"A. Biere, E. Clarke, R. Raimi, and Y. Zhu. Verifying Safety Properties of a Power PC Microprocessor Using Symbolic Model Checking without BDDs. In Proc CAV99, volume 1633 of LNCS. Springer, 1999."},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"J. Castro, M. Kolp, and J. Mylopoulos. A Requirements-Driven Development Methodology. In Proc. of the 13th Int.nl Conf. on Advanced Information Systems Engineering, 2001.","DOI":"10.1007\/3-540-45341-5_8"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"A. Cimatti, E. M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In Proc. of Int.nl Conf. on Computer-Aided Verification (CAV 2002), 2002.","DOI":"10.1007\/3-540-45657-0_29"},{"key":"3_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1007\/3-540-48683-6_44","volume-title":"Proceedings Eleventh Conference on Computer-Aided Verification (CAV\u201999)","author":"A. Cimatti","year":"1999","unstructured":"A. Cimatti, E.M. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: a newSymbolic ModelVerifier. In N. Halbwachs and D. Peled, editors, Proceedings Eleventh Conference on Computer-Aided Verification (CAV\u201999), number 1633 in LNCS, pages 495\u2013499, 1999."},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"A. Cimatti, E. Giunchiglia, M. Roveri, M. Pistore, R. Sebastiani, and A. Tacchella. Integrating BDD-based and SAT-based Symbolic Model Checking. In Proceeding of 4th International Workshop on Frontiers of Combining Systems (FroCoS\u20192002), 2002.","DOI":"10.1007\/3-540-45988-X_5"},{"key":"3_CR12","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1023\/A:1008615614281","volume":"10","author":"E. Clarke","year":"1997","unstructured":"E. Clarke, O. Grumberg, and K. Hamaguchi. Another Look at LTL Model Checking. Formal Methods in System Design, 10:47\u201371, 1997.","journal-title":"Formal Methods in System Design"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"F. Copty, L. Fix, E. Giunchiglia, G. Kamhi, A. Tacchella, and M. Vardi. Benefits of Bounded Model Checking at an Industrial Setting. In Proceedings of CAV 2001, pages 436\u2013453, 2001.","DOI":"10.1007\/3-540-44585-4_43"},{"key":"3_CR14","first-page":"995","volume-title":"Handbook of Theoretical Computer Science","author":"E.A. Emerson","year":"1990","unstructured":"E.A. Emerson. Temporal and Modal Logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 995\u20131072. Elsevier Science Publisher B.V., 1990."},{"key":"3_CR15","unstructured":"A. Fuxman. Formal Analysis of Early Requirements Specifications. PhD thesis, University of Toronto, Toronto, Canada, 2001."},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Dov Gabbay. The Declarative Past and Imperative Future. In Proccedings of the Colloquium on Temporal Logic and Specifications, volume 398, pages 409\u2013448. Springer-Verlag, 1987.","DOI":"10.1007\/3-540-51803-7_36"},{"key":"3_CR17","unstructured":"S. Gnesi, D. Latella, and G. Lenzini. Formal Verification of Cryptographic Protocols using History Dependent Automata. In Proc. of the 4thWorkshop on Sistemi Distribuiti: Algoritmi, Architetture e Linguaggi, 1999."},{"key":"3_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"519","DOI":"10.1007\/3-540-44685-0_35","volume-title":"Extended Temporal Logic Revisited","author":"O. Kupferman","year":"2001","unstructured":"O. Kupferman, N. Piterman, and M. Vardi. Extended Temporal Logic Revisited. In Proc. 12th Int.nl Conf. on Concurrency Theory, number 2154 in LNCS, pages 519\u2013534, 2001."},{"key":"3_CR19","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1016\/0304-3975(95)00035-U","volume":"148","author":"F. Laroussinie","year":"1995","unstructured":"F. Laroussinie and Ph. Schnoebelen. A Hierarchy of Temporal Logics with Past. Theoretical Computer Science, 148:303\u2013324, 1995.","journal-title":"Theoretical Computer Science"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an Efficient SAT Solver. In Proc. of the 38th Design Automation Conference, 2001.","DOI":"10.1145\/378239.379017"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"M. Sheeran, S. Singh, and G. Stalmarck. Checking safety properties using induction and a SAT-solver. In Proc. Int.nl Conf. on Formal Methods in Computer-Aided Design, 2000.","DOI":"10.1007\/3-540-40922-X_8"},{"key":"3_CR22","series-title":"Lect Notes Comput Sci","volume-title":"Tuning SAT Checkers for Bounded Model Checking","author":"O. Shtrichmann","year":"2000","unstructured":"O. Shtrichmann. Tuning SAT Checkers for Bounded Model Checking. In Proc. CAV\u20192000, volume 1855 of LNCS. Springer, 2000."},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"A. van Lamsweerde. Goal-Oriented Requirements Engineering:A Guided Tour. In Proc. 5th IEEE International Symposium on Requirements Engineering, pages 249\u2013263, 2001.","DOI":"10.1109\/ISRE.2001.948567"},{"key":"3_CR24","unstructured":"M. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First Annual Symposium on Logic in Computer Science, 1986."},{"key":"3_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1007\/10722167_13","volume-title":"Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking","author":"P. F. Williams","year":"2000","unstructured":"P. F. Williams, A. Biere, E. M. Clarke, and A. Gupta. Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking. In Proc. CAV\u20192000, volume 1855 of LNCS, pages 124\u2013138. Springer, 2000."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36577-X_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T19:10:19Z","timestamp":1739992219000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36577-X_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008989","9783540365778"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-36577-x_3","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2003]]}}}