{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T13:33:21Z","timestamp":1762004001362},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540001416"},{"type":"electronic","value":"9783540361350"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36135-9_16","type":"book-chapter","created":{"date-parts":[[2007,5,31]],"date-time":"2007-05-31T22:43:21Z","timestamp":1180651401000},"page":"243-259","source":"Crossref","is-referenced-by-count":47,"title":["Bounded Model Checking for Timed Systems"],"prefix":"10.1007","author":[{"given":"G.","family":"Audemard","sequence":"first","affiliation":[]},{"given":"A.","family":"Cimatti","sequence":"additional","affiliation":[]},{"given":"A.","family":"Kornilowicz","sequence":"additional","affiliation":[]},{"given":"R.","family":"Sebastiani","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,11,5]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"G. Audemard, P. Bertoli, A. Cimatti, A. Korni lowicz, and R. Sebastiani. A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions. In Proc. CADE\u20192002., 2002.","DOI":"10.1007\/3-540-45620-1_17"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur. Timed Automata. In Proc. CAV\u201999, pages 8\u201322, 1999.","DOI":"10.1007\/3-540-48683-6_3"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"A. Biere, A. Cimatti, E. M. Clarke, and Yunshan Zhu. Symbolic Model Checking without BDDs. In Proc. TACAS\u201999, pages 193\u2013207, 1999.","DOI":"10.21236\/ADA360973"},{"key":"16_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"546","DOI":"10.1007\/BFb0028779","volume-title":"Kronos: A model-checking tool for real-time systems","author":"M. Bozga","year":"1998","unstructured":"M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, and S. Yovine. Kronos: A model-checking tool for real-time systems. In A. J. Hu and M. Y. Vardi, editors, Proc. 10th International Conference on Computer Aided Verification, Vancouver, Canada, volume 1427 of LNCS, pages 546\u2013550. Springer-Verlag, 1998."},{"key":"16_CR5","series-title":"Lect Notes Comput Sci","volume-title":"Benefits of Bounded Model Checking at an Industrial Setting","author":"F. Copty","year":"2001","unstructured":"F. Copty, L. Fix, E. Giunchiglia, G. Kamhi, A. Tacchella, and M. Vardi. Benefits of Bounded Model Checking at an Industrial Setting. In Proc. CAV\u20192001, LNCS. Springer, 2001."},{"key":"16_CR6","series-title":"Lect Notes Comput Sci","first-page":"197","volume-title":"Automatic Verification Methods for Finite State Systems","author":"D. L. Dill","year":"1989","unstructured":"David L. Dill. Timing assumptions and verification of finite-state concurrent systems. InAutomatic Verification Methods for Finite State Systems, volume 407 of Lecture Notes in Computer Science, pages 197\u2013212. Springer-Verlag, June 1989."},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"M. Davis, G. Longemann, and D. Loveland. A machine program for theorem proving. Journal of the ACM, 5(7), 1962.","DOI":"10.1145\/368273.368557"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"C. Daws and S. Yovine. Two examples of verification of multirate timed automata with kronos. In Proc. 16th IEEE Real-Time Systems Symposium, pages 66\u201375, 1995.","DOI":"10.1109\/REAL.1995.495197"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"E.A. Emerson. Temporal and Modal Logic. InJ. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 995\u20131072. Elsevier Science Publisher B.V., 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"16_CR10","unstructured":"E. Giunchiglia, A. Massarotto, and R. Sebastiani. Act, and the Rest Will Follow: Exploiting Determinism in Planning as Satisfiability. In Proc. AAAI\u201998, pages 948\u2013953, 1998."},{"issue":"2","key":"16_CR11","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T. Henzinger","year":"1994","unstructured":"T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193\u2013244, 1994.","journal-title":"Information and Computation"},{"key":"16_CR12","unstructured":"Chu Min Li and Anbulagan. Heuristics based on unit propagation for satisfiability problems. In Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI-97), pages 366\u2013371, 1997."},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"L. Lamport. A Fast Mutual-exclusion Algorithm. ACM Transactions on Computer Systems, 5(1), 1987.","DOI":"10.1145\/7351.7352"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"K. G. Larsen, P. Pettersson, and W. Yi. Model-Checking for Real-Time Systems. In Fundamentals of Computation Theory, pages 62\u201388, 1995.","DOI":"10.1007\/3-540-60249-6_41"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"K.G. Larsen, C. Weise, W. Yi, and J. Pearson. Clock difference diagrams. Technical Report 98\/99, DoCS, Uppsala University, Sweden, 1998.","DOI":"10.7146\/brics.v5i46.19491"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"J. Moeller, J. Lichtenberg, H. Andersen, and H. Hulgaard. Fully Symbolic Model Checking of Timed Systems using Difference Decision Diagrams. In Electronic Notes in Theoretical Computer Science, volume 23. Elsevier Science, 2001.","DOI":"10.1016\/S1571-0661(04)80671-6"},{"key":"16_CR17","series-title":"Lect Notes Comput Sci","volume-title":"Verification of Timed Automata via Satisfiability Checking","author":"P. Niebert","year":"2002","unstructured":"P. Niebert, M. Mahfoudh, E. Asarin, M. Bozga, and O. Maler. Verification of Timed Automata via Satisfiability Checking. In Proc. of FTRTFT\u201902, LNCS. Springer-Verlag, 2002."},{"key":"16_CR18","series-title":"Lect Notes Comput Sci","volume-title":"Towards bounded model checking for the universal fragment of TCTL","author":"W. Penczek","year":"2002","unstructured":"W. Penczek, B. Wo\u017ana, and A. Zbrzezny. Towards bounded model checking for the universal fragment of TCTL. In Proc. of FTRTFT\u201902, LNCS. Springer-Verlag, 2002."},{"key":"16_CR19","unstructured":"R. Sebastiani. Integrating SAT Solvers with Math Reasoners: Foundations and Basic Algorithms. Technical Report 0111-22, ITC-IRST, November 2001."},{"key":"16_CR20","series-title":"Lect Notes Comput Sci","volume-title":"Tuning SAT Checkers for Bounded Model Checking","author":"O. Shtrichmann","year":"2000","unstructured":"Ofer Shtrichmann. Tuning SAT Checkers for Bounded Model Checking. In Proc. CAV\u20192000, volume 1855 of LNCS. Springer, 2000."},{"key":"16_CR21","unstructured":"Maria Sorea. Bounded model checking for timed automata. ENTCS, 68(5), 2002."},{"key":"16_CR22","doi-asserted-by":"crossref","unstructured":"Farn Wang. Efficient data structure for fully symbolic verification of real-time software systems. InTools and Algorithms for Construction and Analysis of Systems, pages 157\u2013171, 2000.","DOI":"10.1007\/3-540-46419-0_12"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Networked and Distributed Sytems \u2014 FORTE 2002"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36135-9_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T11:17:45Z","timestamp":1556450265000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36135-9_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540001416","9783540361350"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-36135-9_16","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}