{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T22:35:55Z","timestamp":1784241355883,"version":"3.55.0"},"reference-count":31,"publisher":"Elsevier BV","issue":"5","license":[{"start":{"date-parts":[[2003,5,1]],"date-time":"2003-05-01T00:00:00Z","timestamp":1051747200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3742,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003,5]]},"DOI":"10.1016\/s1571-0661(04)80523-1","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T12:47:47Z","timestamp":1096462067000},"page":"116-134","source":"Crossref","is-referenced-by-count":18,"title":["Bounded Model Checking for Timed Automata1 1This research was supported by the National Science Foundation under grants CCR-00-82560 and CCR-00-86096."],"prefix":"10.1016","volume":"68","author":[{"given":"Maria","family":"Sorea","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)80523-1_NEWBIB1","unstructured":"Alur R., \u201cTechniques for Automatic Verification of Real-Time Systems,\u201d Ph.D. thesis, Stanford University (1991)."},{"key":"10.1016\/S1571-0661(04)80523-1_NEWBIB2","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1007\/3-540-48683-6_3","article-title":"Timed automata","volume":"1633","author":"Alur","year":"1999","journal-title":"Lecture Notes in Computer Science"},{"key":"10.1016\/S1571-0661(04)80523-1_NEWBIB3","first-page":"414","article-title":"Model-checking for real-time systems","author":"Alur","year":"1990","journal-title":"5th Symp. on Logic in Computer Science (LICS 90)"},{"key":"10.1016\/S1571-0661(04)80523-1_NEWBIB4","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"A theory of timed automata","volume":"126","author":"Alur","year":"1994","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80523-1_NEWBIB5","doi-asserted-by":"crossref","unstructured":"Audemard G., A. Cimatti, A. Kornilowicz and R. Sebastiani, Bounded model checking for timed systems, Proceedings of the 2nd Workshop on Real-Time Tools (RT-TOOLS'2002) (2002).","DOI":"10.1007\/3-540-36135-9_16"},{"key":"10.1016\/S1571-0661(04)80523-1_NEWBIB6","doi-asserted-by":"crossref","unstructured":"Barrett, C. W., D. L. Dill and A. Stump, Checking satisfiability of first-order formulas by incremental translation to SAT (2002), to be presented at CAV 2002.","DOI":"10.1007\/3-540-45657-0_18"},{"key":"10.1016\/S1571-0661(04)80523-1_NEWBIB7","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","article-title":"Graph-based algorithms for boolean function Manipulation","volume":"C-35","author":"Bryant","year":"1986","journal-title":"IEEE Transactions on Computers"},{"key":"10.1016\/S1571-0661(04)80523-1_NEWBIB8","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1011276507260","article-title":"Bounded model checking using satisfiability solving","volume":"19","author":"Clarke","year":"2001","journal-title":"Formal Methods in System Design"},{"key":"10.1016\/S1571-0661(04)80523-1_NEWBIB9","doi-asserted-by":"crossref","unstructured":"Copty, F., L. Fix, R. Fraer, E. Giunchiglia, G. Kamhi, A. Tacchella and M. Vardi, Benefits of bounded model checking in an industrial setting, in: Computer-Aided Verification, CAV 2001, Lecture Notes in Computer Science 2101 (2001), pp. 436\u2013453.","DOI":"10.1007\/3-540-44585-4_43"},{"key":"10.1016\/S1571-0661(04)80523-1_NEWBIB10","unstructured":"Dams, D. R., \u201cAbstract Interpretation and Partition Refinement for Model Checking,\u201d Ph.D. thesis, Eindhoven University of Technology, P.O. Box 513, 5600 MB Eindhoven, The Netherlands (1996)."},{"key":"10.1016\/S1571-0661(04)80523-1_NEWBIB11","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1007\/BFb0020947","article-title":"The tool KRONOS","volume":"1066","author":"Daws","year":"1996","journal-title":"Lecture Notes in Computer Science"},{"key":"10.1016\/S1571-0661(04)80523-1_NEWBIB12","unstructured":"de Moura L. and H. Rue\u00df, Lemmas on demand for satisfiability solvers, in: Proceedings of the Fifth International Symposium on the Theory and Applications of Satisfiability Testing (SAT 2002), Cincinnati, Ohio, 2002."},{"key":"10.1016\/S1571-0661(04)80523-1_NEWBIB13","doi-asserted-by":"crossref","unstructured":"de Moura L., H. Rue\u00df and M. Sorea, Lazy theorem proving for bounded model checking over infinite domains, in: A. Voronkov, editor, 18th Conference on Automated Deduction (CADE), Lecture Notes in Computer Science 2392 (2002), pp. 438\u2013455.","DOI":"10.1007\/3-540-45620-1_35"},{"key":"10.1016\/S1571-0661(04)80523-1_NEWBIB14","unstructured":"Dill D., Timing assumptions and verification of finite-state concurrent systems, in: Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science 407 (1989), pp. 197\u2013212."},{"key":"10.1016\/S1571-0661(04)80523-1_NEWBIB15","unstructured":"Filli\u01cetre J.-C., S. Owre, H. Rue\u00df and N. Shankar, ICS: Integrated canonizer and solver, in: G. Berry, H. Comon and A. Finkel, editors, Proceedings of CAV'2001, Lecture Notes in Computer Science 2102 (2001), pp. 246\u2013249."},{"key":"10.1016\/S1571-0661(04)80523-1_NEWBIB16","first-page":"3","article-title":"Simple on-the-fly automatic verification of linear temporal logic","author":"Gerth","year":"1995","journal-title":"Protocol Specification Testing and Verification"},{"key":"10.1016\/S1571-0661(04)80523-1_NEWBIB17","doi-asserted-by":"crossref","first-page":"460","DOI":"10.1007\/3-540-63166-6_48","article-title":"HYTECH: A model checker for hybrid systems","volume":"1254","author":"Henzinger","year":"1997","journal-title":"Lecture Notes in Computer Science"},{"key":"10.1016\/S1571-0661(04)80523-1_NEWBIB18","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1006\/inco.1994.1045","article-title":"Symbolic model checking for real-time systems","volume":"111","author":"Henzinger","year":"1994","journal-title":"Information and Computation"},{"key":"10.1016\/S1571-0661(04)80523-1_NEWBIB19","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1023\/A:1011254632723","article-title":"Model checking of safety properties","volume":"19","author":"Kupferman","year":"2001","journal-title":"Formal Methods in System Design"},{"key":"10.1016\/S1571-0661(04)80523-1_NEWBIB20","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/7351.7352","article-title":"A fast mutual exclusion algorithm","volume":"5","author":"Lamport","year":"1987","journal-title":"ACM Transactions on Computer Systems"},{"key":"10.1016\/S1571-0661(04)80523-1_NEWBIB21","first-page":"271","article-title":"Clock difference diagrams","volume":"6","author":"Larsen","year":"1999","journal-title":"Nordic Journal of Computing"},{"key":"10.1016\/S1571-0661(04)80523-1_NEWBIB22","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","article-title":"UPPAAL in a nutshell","volume":"1","author":"Larsen","year":"1997","journal-title":"Int. Journal on Software Tools for Technology Transfer"},{"key":"10.1016\/S1571-0661(04)80523-1_NEWBIB23","doi-asserted-by":"crossref","unstructured":"M\u2298ller J., J. Lichtenberg, H. R. Andersen and H. Hulgaard, Difference decision diagrams, in: Computer Science Logic, The IT University of Copenhagen, Denmark, 1999.","DOI":"10.1007\/3-540-48168-0_9"},{"key":"10.1016\/S1571-0661(04)80523-1_NEWBIB24","article-title":"Predicate abstraction for dense real-time systems","volume":"65","author":"M\u00f6ller","year":"2002","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80523-1_NEWBIB25","doi-asserted-by":"crossref","unstructured":"Niebert P., M. Mahfoudh, E. Asarin, M. Bozga, N. Jain and O. Maler, Verification of timed automata via satisfiability checking, in: Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT), Lecture Notes in Computer Science (2002).","DOI":"10.1007\/3-540-45739-9_15"},{"key":"10.1016\/S1571-0661(04)80523-1_NEWBIB26","doi-asserted-by":"crossref","unstructured":"Owre S., J. M. Rushby and N. Shankar, PVS: A prototype verification system, in: 11th International Conference on Automated Deduction (CADE), Lecture Notes in Artificial Intelligence 607 (1992), pp. 748\u2013752.","DOI":"10.1007\/3-540-55602-8_217"},{"key":"10.1016\/S1571-0661(04)80523-1_NEWBIB27","doi-asserted-by":"crossref","unstructured":"Penczek W., B. Wozna and A. Zbrzezny, Towards bounded model checking for the universal fragment of TCTL, in: Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT), Lecture Notes in Computer Science (2002).","DOI":"10.1007\/3-540-45739-9_17"},{"key":"10.1016\/S1571-0661(04)80523-1_NEWBIB28","doi-asserted-by":"crossref","first-page":"769","DOI":"10.1145\/322276.322288","article-title":"Deciding linear inequalities by computing loop residues","volume":"28","author":"Shostak","year":"1981","journal-title":"Journal of the ACM"},{"key":"10.1016\/S1571-0661(04)80523-1_NEWBIB29","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1007\/BF01211865","article-title":"Safety, liveness and fairness in temporal logic","volume":"6","author":"Sistla","year":"1994","journal-title":"Formal Aspects of Computing"},{"key":"10.1016\/S1571-0661(04)80523-1_NEWBIB30","unstructured":"Sorea M., Tempo: A model-checker for event-recording automata, in: Proceedings of RT-TOOLS'01, Aalborg, Denmark, 2001, also available as Technical Report SRI-CSL-01\u201304, Computer Science Laboratory, SRI International, Menlo Park, CA, 2001. URL http:\/\/www.csl.sri.com\/papers\/csl-01-04\/"},{"key":"10.1016\/S1571-0661(04)80523-1_NEWBIB31","first-page":"25","article-title":"Analysis of timed systems using time-abstracting bisimulations","volume":"18","author":"Tripakis","year":"2001"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104805231?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104805231?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T03:11:44Z","timestamp":1585883504000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104805231"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,5]]},"references-count":31,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2003,5]]}},"alternative-id":["S1571066104805231"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80523-1","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2003,5]]}}}