{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:10:59Z","timestamp":1761610259365,"version":"build-2065373602"},"reference-count":19,"publisher":"Elsevier BV","issue":"4","license":[{"start":{"date-parts":[[2002,12,1]],"date-time":"2002-12-01T00:00:00Z","timestamp":1038700800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2002,12,1]],"date-time":"2002-12-01T00:00:00Z","timestamp":1038700800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3893,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2002,12]]},"DOI":"10.1016\/s1571-0661(04)80581-4","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T12:47:47Z","timestamp":1096462067000},"page":"128-141","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":3,"title":["Tracing the executions of concurrent programs"],"prefix":"10.1016","volume":"70","author":[{"given":"Elsa","family":"Gunter","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Doron","family":"Peled","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)80581-4_NEWBIB1","first-page":"70","article-title":"An analyzer for message sequence charts","volume":"1","author":"Alur","year":"1996","journal-title":"Software: Concepts and Tools"},{"year":"1991","series-title":"Verification of Sequential and Concurrent Programs","author":"Apt","key":"10.1016\/S1571-0661(04)80581-4_NEWBIB2"},{"issue":"4","key":"10.1016\/S1571-0661(04)80581-4_NEWBIB3","first-page":"747","article-title":"Model-checking Concurrent Systems with Unbounded Integer Variables: Symbolic Representations","volume":"21","author":"Bultan","year":"1999","journal-title":"approximations, and experimental results, TOPLAS"},{"key":"10.1016\/S1571-0661(04)80581-4_NEWBIB4","series-title":"Workshop on Logic of Programs, Yorktown Heights, NY, Lecture Notes in Computer Science 131","first-page":"52","article-title":"Design and synthesis of synchronization skeletons using branching time temporal logic","author":"Clarke","year":"1981"},{"key":"10.1016\/S1571-0661(04)80581-4_NEWBIB5","series-title":"Characterizing correctness properties of parallel programs using fixpoints, International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science 85","first-page":"169","author":"Emerson","year":"1980"},{"year":"1997","series-title":"UML Distilled: Applying the Standard Object Modeling Language","author":"Fowler","key":"10.1016\/S1571-0661(04)80581-4_NEWBIB6"},{"year":"1992","series-title":"Program Verfication","author":"Francez","key":"10.1016\/S1571-0661(04)80581-4_NEWBIB7"},{"key":"10.1016\/S1571-0661(04)80581-4_NEWBIB8","first-page":"1203","volume":"30","author":"Gansner","year":"2000","journal-title":"An open graph visualization system and its applications to software engineering, Software - Practice and Experience"},{"key":"10.1016\/S1571-0661(04)80581-4_NEWBIB9","series-title":"Simple On-the-fly Automatic Verification of Linear Temporal Logic, PSTV95, Protocol Specification Testing and Verification","first-page":"3","author":"Gerth","year":"1995"},{"key":"10.1016\/S1571-0661(04)80581-4_NEWBIB10","doi-asserted-by":"crossref","unstructured":"P. Godefroid, Model checking for programming languages using Verisoft, POPL 1997, 174\u2013186","DOI":"10.1145\/263699.263717"},{"key":"10.1016\/S1571-0661(04)80581-4_NEWBIB11","unstructured":"G. Holzmann, Design and Validation of Computer Protocol, Prentice Hall"},{"key":"10.1016\/S1571-0661(04)80581-4_NEWBIB12","doi-asserted-by":"crossref","unstructured":"E. Gunter, D. Peled, Path Exploration Tool, TACAS 1999, LNCS 1579, Springer, 405\u2013419","DOI":"10.1007\/3-540-49059-0_28"},{"key":"10.1016\/S1571-0661(04)80581-4_NEWBIB13","doi-asserted-by":"crossref","unstructured":"E. Gunter, D. Peled, Temporal debuging for concurrent systems, TACAS 2002, LNCS 2280, Springer, 431\u2013444","DOI":"10.1007\/3-540-46002-0_30"},{"key":"10.1016\/S1571-0661(04)80581-4_NEWBIB14","first-page":"385","author":"King","year":"1976","journal-title":"Symbolic execution and program testing, Communiucation of the ACM"},{"key":"10.1016\/S1571-0661(04)80581-4_NEWBIB15","unstructured":"ITU-T Recommendation Z.120, Message Sequence Chart (MSC), March 1993"},{"year":"1979","series-title":"The Art of Software Testing","author":"Myers","key":"10.1016\/S1571-0661(04)80581-4_NEWBIB16"},{"year":"1993","series-title":"Real-Time Object-Oriented Modeling","author":"Selic","key":"10.1016\/S1571-0661(04)80581-4_NEWBIB17"},{"key":"10.1016\/S1571-0661(04)80581-4_NEWBIB18","doi-asserted-by":"crossref","unstructured":"N. Sharygina, D. Peled, A combined testing and verification approach for software reliability, FME 2001, LNCS 2021, 611\u2013628","DOI":"10.1007\/3-540-45251-6_35"},{"key":"10.1016\/S1571-0661(04)80581-4_NEWBIB19","doi-asserted-by":"crossref","unstructured":"A. Pnueli, The temporal logic of programs, 18th IEEE symposium on Foundation of Computer Science, 1977, 46\u201357","DOI":"10.1109\/SFCS.1977.32"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104805814?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104805814?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:06:04Z","timestamp":1761609964000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104805814"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,12]]},"references-count":19,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2002,12]]}},"alternative-id":["S1571066104805814"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80581-4","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[2002,12]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Tracing the executions of concurrent programs","name":"articletitle","label":"Article Title"},{"value":"Electronic Notes in Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1571-0661(04)80581-4","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2002 Published by Elsevier B.V.","name":"copyright","label":"Copyright"}]}}