{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T16:26:25Z","timestamp":1742401585723},"reference-count":26,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2001,2,1]],"date-time":"2001-02-01T00:00:00Z","timestamp":980985600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4549,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2001,2]]},"DOI":"10.1016\/s0304-3975(00)00090-6","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T14:45:40Z","timestamp":1027608340000},"page":"95-118","source":"Crossref","is-referenced-by-count":8,"title":["The Verus language: representing time efficiently with BDDs"],"prefix":"10.1016","volume":"253","author":[{"given":"S\u00e9rgio Vale Aguiar","family":"Campos","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Edmund","family":"Clarke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(00)00090-6_BIB1","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcourbetis, D. Dill, Model-checking for real-time systems, Proc. 5th Symp. on Logics in Computer Science, 1990, pp. 414\u2013425.","DOI":"10.1109\/LICS.1990.113766"},{"key":"10.1016\/S0304-3975(00)00090-6_BIB2","series-title":"Automata for modeling real-time systems","author":"Alur","year":"1990"},{"key":"10.1016\/S0304-3975(00)00090-6_BIB3","doi-asserted-by":"crossref","DOI":"10.1016\/0167-6423(92)90005-V","article-title":"The ESTEREL synchronous programming language: design, semantics, implementation","volume":"19","author":"Berry","year":"1992","journal-title":"Sci. Comput. Programm."},{"key":"10.1016\/S0304-3975(00)00090-6_BIB4","series-title":"A timed full LOTOS with time\/action tree semantics","author":"Bolognesi","year":"1994"},{"key":"10.1016\/S0304-3975(00)00090-6_BIB5","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, J. Hwang, Symbolic model checking: 1020 states and beyond. 5th Symp. on Logics in Computer Science, 1990."},{"key":"10.1016\/S0304-3975(00)00090-6_BIB6","doi-asserted-by":"crossref","unstructured":"S.V. Campos, A quantitative approach to the formal verification of real-time systems, Ph.D. thesis, SCS, Carnegie Mellon University, 1996.","DOI":"10.1007\/3-540-63166-6_46"},{"key":"10.1016\/S0304-3975(00)00090-6_BIB7","doi-asserted-by":"crossref","unstructured":"S.V. Campos, E.M. Clarke, W. Marrero, M. Minea, H. Hiraishi, Computing quantitative characteristics of finite-state real-time systems, Real-Time Systems Symp., 1994.","DOI":"10.1109\/REAL.1994.342709"},{"key":"10.1016\/S0304-3975(00)00090-6_BIB8","doi-asserted-by":"crossref","unstructured":"S.V. Campos, E.M. Clarke, W. Marrero, M. Minea, Verifying the performance of the PCI local bus using symbolic techniques, ICCD, 1995.","DOI":"10.1109\/ICCD.1995.528793"},{"key":"10.1016\/S0304-3975(00)00090-6_BIB9","doi-asserted-by":"crossref","unstructured":"S.V. Campos, E.M. Clarke, W. Marrero, M. Minea, Verus: a tool for quantitative analysis of finite-state real-time systems, Workshop on Languages, Compilers and Tools for Real-Time Systems, 1995.","DOI":"10.1145\/216636.216661"},{"key":"10.1016\/S0304-3975(00)00090-6_BIB10","doi-asserted-by":"crossref","unstructured":"S.V. Campos, O. Grumberg, Selective quantitative analysis and interval model checking: verifying different facets of a system, Comput. Aided Verification (1996).","DOI":"10.1007\/3-540-61474-5_74"},{"key":"10.1016\/S0304-3975(00)00090-6_BIB11","series-title":"Synthesis of synchronization skeletons for branching time temporal logic, Logic of Programs: Workshop, Yorktown Heights, NY, May 1981.","volume":"Vol. 131","author":"Clarke","year":"1981"},{"key":"10.1016\/S0304-3975(00)00090-6_BIB12","unstructured":"E.M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D.E. Long, K.L. McMillan, L.A. Ness, Verification of the Futurebus+ cache coherence protocol, 11th CHDL, 1993."},{"key":"10.1016\/S0304-3975(00)00090-6_BIB13","doi-asserted-by":"crossref","unstructured":"P. Clements, C. Heitmeyer, G. Labaw, A. Rose, MT: a toolset for specifying and analyzing real-time systems, IEEE Real-Time Systems Symp., 1993.","DOI":"10.1109\/REAL.1993.393519"},{"issue":"2","key":"10.1016\/S0304-3975(00)00090-6_BIB14","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1016\/0304-3975(94)00169-J","article-title":"A brief story of timed CSP","volume":"138","author":"Davies","year":"1995","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00090-6_BIB15","series-title":"Quantitative temporal reasoning","author":"Emerson","year":"1990"},{"key":"10.1016\/S0304-3975(00)00090-6_BIB16","doi-asserted-by":"crossref","unstructured":"A.N. Fredette, R. Cleaveland, RTSL: a language for real-time schedulability analysis, IEEE Real-Time Systems Symp., 1993.","DOI":"10.1109\/REAL.1993.393489"},{"key":"10.1016\/S0304-3975(00)00090-6_BIB17","doi-asserted-by":"crossref","unstructured":"V. Hartonas-Garmhausen, S. Campos, E. Clarke, A. Cimatti, F. Giunchiglia, Verification of a safety-critical railway interlocking system with real-time constraints, 28th IEEE Internat. Symp. on Fault Tolerant Computing, 1998.","DOI":"10.1109\/FTCS.1998.689498"},{"key":"10.1016\/S0304-3975(00)00090-6_BIB18","doi-asserted-by":"crossref","unstructured":"T. Henzinger, P. Ho, H. Wong-Toi, HyTech: the next generation, IEEE Real-Time Systems Symp., 1995.","DOI":"10.1109\/REAL.1995.495196"},{"key":"10.1016\/S0304-3975(00)00090-6_BIB19","doi-asserted-by":"crossref","unstructured":"T. Henzinger, X. Nicollin, J. Sifakis, S. Yovine, Symbolic model checking for real-time systems, Proc. 7th Symp. on Logic in Computer Science, 1992.","DOI":"10.1109\/LICS.1992.185551"},{"key":"10.1016\/S0304-3975(00)00090-6_BIB20","unstructured":"F. Jahanian, D. Stuart, A method for verifying properties of modechart specifications, IEEE Real-Time Systems Symp., 1988."},{"key":"10.1016\/S0304-3975(00)00090-6_BIB21","doi-asserted-by":"crossref","unstructured":"C. Locke, D. Vogel, T. Mesler, Building a predictable avionics platform in Ada: a case study, IEEE Real-Time Systems Symp., 1991.","DOI":"10.1109\/REAL.1991.160372"},{"key":"10.1016\/S0304-3975(00)00090-6_BIB22","doi-asserted-by":"crossref","unstructured":"K.L. McMillan, Symbolic model checking \u2013 an approach to the state explosion problem, Ph.D. Thesis, SCS, Carnegie Mellon University, 1992.","DOI":"10.1007\/978-1-4615-3190-6_3"},{"issue":"1","key":"10.1016\/S0304-3975(00)00090-6_BIB23","doi-asserted-by":"crossref","DOI":"10.1016\/0164-1212(92)90045-L","article-title":"Formal methods for the specification and design of real-time safety critical systems","volume":"18","author":"Ostroff","year":"1992","journal-title":"J. Systems Software"},{"key":"10.1016\/S0304-3975(00)00090-6_BIB24","unstructured":"S.T. Probst, Chemical process safety and operability analysis using symbolic model checking, Ph.D. Thesis, Dept. of Chemical Engineering, Carnegie Mellon University, 1996."},{"issue":"3","key":"10.1016\/S0304-3975(00)00090-6_BIB25","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1007\/BF01211556","article-title":"TIC","volume":"5","author":"Quemada","year":"1993","journal-title":"Formal aspects computing"},{"key":"10.1016\/S0304-3975(00)00090-6_BIB26","doi-asserted-by":"crossref","unstructured":"G. Winskel, The Formal Semantics of Programming Languages, an Introduction, The MIT Press, Cambridge, MA, 1994, pp. 135\u2013139.","DOI":"10.7551\/mitpress\/3054.001.0001"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397500000906?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397500000906?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,1,9]],"date-time":"2020-01-09T17:37:20Z","timestamp":1578591440000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397500000906"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,2]]},"references-count":26,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2001,2]]}},"alternative-id":["S0304397500000906"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(00)00090-6","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2001,2]]}}}