{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:24:44Z","timestamp":1761596684279},"reference-count":38,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"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":4215,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Science of Computer Programming"],"published-print":{"date-parts":[[2002,1]]},"DOI":"10.1016\/s0167-6423(01)00033-8","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T10:03:45Z","timestamp":1027591425000},"page":"39-47","source":"Crossref","is-referenced-by-count":23,"title":["Generic tools for verifying concurrent systems"],"prefix":"10.1016","volume":"42","author":[{"given":"Rance","family":"Cleaveland","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steven T.","family":"Sims","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0167-6423(01)00033-8_BIB1","unstructured":"R. Alur T. Henzinger (Eds.), in: Computer Aided Verification (CAV \u201996), New Brunswick, New Jersey, Lecture Notes in Computer Science, vol. 1102, Springer, Berlin, July 1996."},{"key":"10.1016\/S0167-6423(01)00033-8_BIB2","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/0167-6423(92)90005-V","article-title":"The ESTEREL synchronous programming language","volume":"19","author":"Berry","year":"1992","journal-title":"Sci. Comput. Programming"},{"key":"10.1016\/S0167-6423(01)00033-8_BIB3","doi-asserted-by":"crossref","unstructured":"G. Bhat, R. Cleaveland, Efficient local model checking for fragments of the modal \u03bc-calculus, in: T. Margaria, B. Steffen (Eds.), Tools and Algorithms for the Construction and Analysis of Systems (TACAS \u201996), Passau, Germany, Lecture Notes in Computer Science, vol. 1055, Springer, Berlin, March 1996, pp. 107\u2013126.","DOI":"10.1007\/3-540-61042-1_41"},{"key":"10.1016\/S0167-6423(01)00033-8_BIB4","doi-asserted-by":"crossref","unstructured":"G. Bhat, R. Cleaveland, Efficient model checking via the equational \u03bc-calculus, in: Eleventh Ann. Symp. on Logic in Computer Science (LICS \u201996), New Brunswick, New Jersey, IEEE Computer Society Press, Silver Spring, MD, July 1996, pp. 304\u2013312.","DOI":"10.1109\/LICS.1996.561358"},{"key":"10.1016\/S0167-6423(01)00033-8_BIB5","doi-asserted-by":"crossref","unstructured":"G. Bhat, R. Cleaveland, G. Luettgen, A practical approach to implementing real-time semantics, Ann. Software Eng. 7 (special issue on real-time software engineering) (1999) 127\u2013155.","DOI":"10.1023\/A:1018982020561"},{"key":"10.1016\/S0167-6423(01)00033-8_BIB6","doi-asserted-by":"crossref","unstructured":"B. Bloom, A. Dsouza, Generating BDD models for process algebra terms, in: P. Wolper (Ed.), Computer Aided Verification (CAV \u201995), Li\u00e8ge, Belgium, Lecture Notes in Computer Science, vol. 939, Springer, Berlin, June 1995, pp. 16\u201330.","DOI":"10.1007\/3-540-60045-0_37"},{"key":"10.1016\/S0167-6423(01)00033-8_BIB7","doi-asserted-by":"crossref","unstructured":"B. Bloom, S. Istrail, A. Meyer, Bisimulation can't be traced, in: Fifteenth Ann. ACM Symp. on Principles of Programming Languages (POPL \u201988), San Diego, ACM Press, New York, January 1988, pp. 229\u2013239.","DOI":"10.1145\/73560.73580"},{"issue":"3","key":"10.1016\/S0167-6423(01)00033-8_BIB8","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/0167-6423(95)00003-B","article-title":"Transformational design and implementation of a new efficient solution to the ready simulation problem","volume":"24","author":"Bloom","year":"1995","journal-title":"Sci. Comput. Programming"},{"key":"10.1016\/S0167-6423(01)00033-8_BIB9","unstructured":"G. Brebner, Private communication."},{"key":"10.1016\/S0167-6423(01)00033-8_BIB10","series-title":"Distributed Systems Analysis with CCS","author":"Bruns","year":"1997"},{"issue":"2","key":"10.1016\/S0167-6423(01)00033-8_BIB11","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","article-title":"Symbolic model checking: 1020 states and beyond","volume":"98","author":"Burch","year":"1992","journal-title":"Inform. Comput."},{"key":"10.1016\/S0167-6423(01)00033-8_BIB12","unstructured":"CCITT, CCITT recommendation Z.100: specification and description language SDL, Technical Report, ITU General Secretariat, 1988."},{"key":"10.1016\/S0167-6423(01)00033-8_BIB13","unstructured":"U. Celikkan, Semantic preorders in the automated verification of concurrent systems, Ph.D. Thesis, North Carolina State University, Raleigh, 1995."},{"key":"10.1016\/S0167-6423(01)00033-8_BIB14","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/s004460050010","article-title":"Generating diagnostic information for behavioral preorders","volume":"9","author":"Celikkan","year":"1995","journal-title":"Distributed Comput."},{"issue":"2","key":"10.1016\/S0167-6423(01)00033-8_BIB15","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","article-title":"Automatic verification of finite-state concurrent systems using temporal logic specifications","volume":"8","author":"Clarke","year":"1986","journal-title":"ACM Trans. Programming Languages Systems"},{"issue":"4","key":"10.1016\/S0167-6423(01)00033-8_BIB16","doi-asserted-by":"crossref","first-page":"626","DOI":"10.1145\/242223.242257","article-title":"Formal methods","volume":"28","author":"Clarke","year":"1996","journal-title":"ACM Comput. Surveys"},{"issue":"2","key":"10.1016\/S0167-6423(01)00033-8_BIB17","first-page":"50","article-title":"Modeling and verifying distributed systems using priorities","volume":"17","author":"Cleaveland","year":"1996","journal-title":"Software Concepts Tools"},{"key":"10.1016\/S0167-6423(01)00033-8_BIB18","doi-asserted-by":"crossref","unstructured":"R. Cleaveland, E. Madelaine, S. Sims, A front-end generator for verification tools, in: E. Brinksma, R. Cleaveland, K.G. Larsen, B. Steffen (Eds.), Tools and Algorithms for the Construction and Analysis of Systems (TACAS \u201995), Aarhus, Denmark, Lecture Notes in Computer Science, vol. 1019, Springer, Berlin, May 1995, pp. 153\u2013173.","DOI":"10.1007\/3-540-60630-0_8"},{"issue":"1","key":"10.1016\/S0167-6423(01)00033-8_BIB19","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1145\/151646.151648","article-title":"The concurrency workbench","volume":"15","author":"Cleaveland","year":"1993","journal-title":"ACM Trans. Programming Languages Systems"},{"key":"10.1016\/S0167-6423(01)00033-8_BIB20","doi-asserted-by":"crossref","unstructured":"R. Cleaveland, S. Sims, The NCSU concurrency workbench, in: Alur, Henzinger (Eds.), Computer Aided Verification (CAV \u201996), New Brunswick, New Jersey, Lecture Notes in Computer Science, vol. 1102, Springer, Berlin, July 1996, pp. 394\u2013397.","DOI":"10.1007\/3-540-61474-5_87"},{"issue":"4","key":"10.1016\/S0167-6423(01)00033-8_BIB21","doi-asserted-by":"crossref","first-page":"607","DOI":"10.1145\/242223.242252","article-title":"Strategic directions in concurrency research","volume":"28","author":"Cleaveland","year":"1996","journal-title":"ACM Comput. Surveys"},{"key":"10.1016\/S0167-6423(01)00033-8_BIB22","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/BF01383878","article-title":"A linear-time model-checking algorithm for the alternation-free modal mu-calculus","volume":"2","author":"Cleaveland","year":"1993","journal-title":"Formal Methods System Des."},{"issue":"1","key":"10.1016\/S0167-6423(01)00033-8_BIB23","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/0304-3975(94)90269-0","article-title":"CTL* and ECTL* as fragments of the modal mu-calculus","volume":"126","author":"Dam","year":"1994","journal-title":"Theoret. Comput. Sci."},{"issue":"1\u20132","key":"10.1016\/S0167-6423(01)00033-8_BIB24","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1016\/S0167-6423(96)00031-7","article-title":"Modeling and verifying active structural control systems","volume":"29","author":"Elseaidy","year":"1997","journal-title":"Sci. Comput. Programming"},{"key":"10.1016\/S0167-6423(01)00033-8_BIB25","doi-asserted-by":"crossref","unstructured":"E.A. Emerson, C. Jutla, A.P. Sistla, On model-checking for fragments of \u03bc-calculus, in: C. Courcoubetis (Ed.), Computer Aided Verification (CAV \u201993), Elounda, Greece, Lecture Notes in Computer Science, vol. 697, Springer, Berlin, June\/July 1993, pp. 385\u2013396.","DOI":"10.1007\/3-540-56922-7_32"},{"key":"10.1016\/S0167-6423(01)00033-8_BIB26","unstructured":"E.A. Emerson, C.-L. Lei, Efficient model checking in fragments of the propositional mu-calculus, in: Symp. on Logic in Computer Science (LICS \u201986), Cambridge, MA, IEEE Computer Society Press, Silver spring, MD, June 1986, pp. 267\u2013278."},{"key":"10.1016\/S0167-6423(01)00033-8_BIB27","doi-asserted-by":"crossref","unstructured":"J.-C. Fernandez, An implementation of an efficient algorithm for bisimulation equivalence, Sci. Comput. Programming, 13 (1989\/1990) 219\u2013236.","DOI":"10.1016\/0167-6423(90)90071-K"},{"key":"10.1016\/S0167-6423(01)00033-8_BIB28","doi-asserted-by":"crossref","unstructured":"J.-C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, M. Sighireanu, CADP: a protocol validation and verification toolbox, in: Alur, Henzinger (Eds.), Computer Aided Verification (CAV \u201996), New Brunswick, New Jersey, Lecture Notes in Computer Science, vol. 1102, Springer, Berlin, July 1996, pp. 437\u2013440.","DOI":"10.1007\/3-540-61474-5_97"},{"key":"10.1016\/S0167-6423(01)00033-8_BIB29","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","article-title":"Statecharts","volume":"8","author":"Harel","year":"1987","journal-title":"Sci. Comput. Programming"},{"key":"10.1016\/S0167-6423(01)00033-8_BIB30","series-title":"Communicating Sequential Processes","author":"Hoare","year":"1985"},{"issue":"3","key":"10.1016\/S0167-6423(01)00033-8_BIB31","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","article-title":"Results on the propositional \u03bc-calculus","volume":"27","author":"Kozen","year":"1983","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0167-6423(01)00033-8_BIB32","series-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Manna","year":"1992"},{"key":"10.1016\/S0167-6423(01)00033-8_BIB33","series-title":"Communication and Concurrency","author":"Milner","year":"1989"},{"key":"10.1016\/S0167-6423(01)00033-8_BIB34","unstructured":"International Standards Organization, LOTOS \u2014 a formal description technique based on the temporal ordering of observational behavior, Technical Report ISO\/TC 97\/SC 21 N 1573, ISO, February 1987."},{"issue":"6","key":"10.1016\/S0167-6423(01)00033-8_BIB35","doi-asserted-by":"crossref","first-page":"973","DOI":"10.1137\/0216062","article-title":"Three partition refinement algorithms","volume":"16","author":"Paige","year":"1987","journal-title":"SIAM J. Comput."},{"key":"10.1016\/S0167-6423(01)00033-8_BIB36","unstructured":"G.D. Plotkin, A structural approach to operational semantics, Technical Report DAIMI-FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark, 1981."},{"key":"10.1016\/S0167-6423(01)00033-8_BIB37","series-title":"The Unified Modeling Language Reference Manual","author":"Rumbaugh","year":"1998"},{"key":"10.1016\/S0167-6423(01)00033-8_BIB38","unstructured":"S. Sims, Customizable tools for verifying concurrent systems, Ph.D. Thesis, North Carolina State University, Raleigh, 1997."}],"container-title":["Science of Computer Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642301000338?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642301000338?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T01:23:12Z","timestamp":1578446592000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0167642301000338"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,1]]},"references-count":38,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2002,1]]}},"alternative-id":["S0167642301000338"],"URL":"https:\/\/doi.org\/10.1016\/s0167-6423(01)00033-8","relation":{},"ISSN":["0167-6423"],"issn-type":[{"value":"0167-6423","type":"print"}],"subject":[],"published":{"date-parts":[[2002,1]]}}}