{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:25:35Z","timestamp":1754483135628},"reference-count":22,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[2003,9,1]],"date-time":"2003-09-01T00:00:00Z","timestamp":1062374400000},"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":3619,"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,9]]},"DOI":"10.1016\/s1571-0661(05)80009-x","type":"journal-article","created":{"date-parts":[[2005,5,20]],"date-time":"2005-05-20T13:21:17Z","timestamp":1116595277000},"page":"499-517","source":"Crossref","is-referenced-by-count":18,"title":["Space-Reduction Strategies for Model Checking Dynamic Software"],"prefix":"10.1016","volume":"89","author":[{"family":"Robby","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthew B.","family":"Dwyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Hatcliff","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Radu","family":"Iosif","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(05)80009-X_BIB1","series-title":"International Journal on Software Tools for Technology Transfer.","article-title":"Symmetric spin","author":"Bosnacki","year":"2002"},{"key":"10.1016\/S1571-0661(05)80009-X_BIB2","series-title":"Proceedings of the Workshop on Advances in Verification","article-title":"Java PathFinder - a second generation of a Java model-checker","author":"Brat","year":"2000"},{"key":"10.1016\/S1571-0661(05)80009-X_BIB3","series-title":"Model Checking","author":"Clarke","year":"2000"},{"key":"10.1016\/S1571-0661(05)80009-X_BIB4","series-title":"Proc. 5th International Conference on Computer Aided Verification, volume 1427 of Lecture Notes in Computer Science","first-page":"147","article-title":"Exploiting symmetries in temporal logic model checking","author":"Clarke","year":"1998"},{"key":"10.1016\/S1571-0661(05)80009-X_BIB5","series-title":"Proc. 5th International Conference on Computer Aided Verification, volume 697 of Lecture Notes in Computer Science.","article-title":"Exploiting symmetries in temporal logic model checking","author":"Clarke","year":"1993"},{"key":"10.1016\/S1571-0661(05)80009-X_BIB6","series-title":"Proceedings of the 22nd International Conference on Software Engineering","article-title":"Bandera: Extracting finite-state models from Java source code","author":"Corbett","year":"2000"},{"key":"10.1016\/S1571-0661(05)80009-X_BIB7","series-title":"Theoretical and Applied Aspects of SPIN Model Checking (LNCS 1680)","article-title":"dspin: A dynamic extension of SPIN","author":"Demartini","year":"1999"},{"key":"10.1016\/S1571-0661(05)80009-X_BIB8","series-title":"Proceedings of the 1st International Symposium on Formal Methods for Components and Objects (to appear)","article-title":"Model-checking middleware-based event-driven real-time embedded software (extended version)","author":"Deng","year":"2002"},{"key":"10.1016\/S1571-0661(05)80009-X_BIB9","article-title":"Using static and dynamic escape analysis to enable model reductions in model-checking concurrent object-oriented programs","author":"Dwyer","year":"2003","journal-title":"Technical Report SANTOS-TR2003-1, Kansas State University"},{"key":"10.1016\/S1571-0661(05)80009-X_BIB10","series-title":"Proc. 5th International Conference on Computer Aided Verification, volume 697 of Lecture Notes in Computer Science.","article-title":"Symmetry and model checking","author":"Emerson","year":"1993"},{"key":"10.1016\/S1571-0661(05)80009-X_BIB11","series-title":"Proceedings of Tenth International SPIN Workshop, volume 2648 of Lecture Notes in Computer Science.","article-title":"Thread-modular model checking","author":"Flanagan","year":"2003"},{"key":"10.1016\/S1571-0661(05)80009-X_BIB12","series-title":"Proceedings of the 25th International Conference on Software Engineering","article-title":"Cadena: An integrated development, analysis, and verification environment for component-based systems","author":"Hatcliff","year":"2003"},{"issue":"1","key":"10.1016\/S1571-0661(05)80009-X_BIB13","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1145\/2455.2460","article-title":"Algebraic laws for nondeterminism and concurrency","volume":"32","author":"Henessy","year":"1985","journal-title":"Journal of the ACM"},{"key":"10.1016\/S1571-0661(05)80009-X_BIB14","series-title":"Proc. 15th International Conference on Computer Aided Verification","article-title":"Thread-modular abstraction refinement","author":"Henzinger","year":"2003"},{"key":"10.1016\/S1571-0661(05)80009-X_BIB15","series-title":"Proceedings of the 29th ACM Symposium on Principles of Programming Languages","first-page":"58","article-title":"Lazy abstraction","author":"Henzinger","year":"2002"},{"key":"10.1016\/S1571-0661(05)80009-X_BIB16","series-title":"Proceedings of Third International SPIN Workshop","article-title":"State compression in spin: Recursive indexing and compression training runs","author":"Holzmann","year":"1997"},{"key":"10.1016\/S1571-0661(05)80009-X_BIB17","series-title":"Proceedings of Ninth International SPIN Workshop, volume 2318 of Lecture Notes in Computer Science","first-page":"22","article-title":"Symmetry reduction criteria for software model checking","author":"Iosif","year":"2002"},{"key":"10.1016\/S1571-0661(05)80009-X_BIB18","article-title":"Symmetry reductions for model checking of concurrent dynamic software","author":"Iosif","year":"2002","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"1\/2","key":"10.1016\/S1571-0661(05)80009-X_BIB19","first-page":"47","article-title":"Better verification through symmetry","volume":"9","author":"Ip","year":"1996","journal-title":"Formal Methods in System Design"},{"key":"10.1016\/S1571-0661(05)80009-X_BIB20","series-title":"Proceedings of Eigth International SPIN Workshop, volume 2057 of Lecture Notes in Computer Science","first-page":"80","article-title":"Addressing dynamic issues of program model checking","author":"Lerda","year":"2001"},{"key":"10.1016\/S1571-0661(05)80009-X_BIB21","series-title":"Proceedings of the 4th Joint Meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (to appear)","article-title":"Bogor: An extensible and highly-modular model checking framework","author":"Robby","year":"2003"},{"key":"10.1016\/S1571-0661(05)80009-X_BIB22","unstructured":"Bogor Website http:\/\/bogor.projects.cis.ksu.edu 2003"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S157106610580009X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S157106610580009X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,1,26]],"date-time":"2019-01-26T10:50:26Z","timestamp":1548499826000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S157106610580009X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,9]]},"references-count":22,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2003,9]]}},"alternative-id":["S157106610580009X"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(05)80009-x","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2003,9]]}}}