{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T11:40:24Z","timestamp":1736422824251,"version":"3.32.0"},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2006,5,1]],"date-time":"2006-05-01T00:00:00Z","timestamp":1146441600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[2006,5]]},"DOI":"10.1007\/s10703-006-0003-4","type":"journal-article","created":{"date-parts":[[2006,6,14]],"date-time":"2006-06-14T11:52:46Z","timestamp":1150285966000},"page":"263-289","source":"Crossref","is-referenced-by-count":6,"title":["Optimistic synchronization-based state-space reduction"],"prefix":"10.1007","volume":"28","author":[{"given":"Scott D.","family":"Stoller","sequence":"first","affiliation":[]},{"given":"Ernie","family":"Cohen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,6,2]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"G. Brat, K. Havelund, S. Park, and W. Visser, \u201cModel checking programs,\u201d in IEEE Int'l. Conference on Automated Software Engineering (ASE), 2000, pp. 3\u201312.","DOI":"10.1109\/ASE.2000.873645"},{"key":"3_CR2","unstructured":"E.M. Clarke, Jr., O. Grumberg, and D.A. Peled, Model Checking, MIT Press, 1999."},{"key":"3_CR3","unstructured":"E. Cohen and L. Lamport, \u201cReduction in TLA,\u201d in Proc. 9th Int'l. Conference on Concurrency Theory (CONCUR), vol. 1466 of Lecture Notes in Computer Science, Springer-Verlag, 1998, pp. 317\u2013331."},{"key":"3_CR4","unstructured":"E. Cohen, \u201cSeparation and reduction,\u201d in Proc. 5th Int'l. Conference on Mathematics of Program Construction, vol. 1837 of Lecture Notes in Computer Science, Springer-Verlag, 2000."},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"C. Flanagan and S. Freund, \u201cDetecting race conditions in large programs,\u201d in Workshop on Program Analysis for Software Tools and Engineering (PASTE), ACM Press, 2001, pp. 90\u201396.","DOI":"10.1145\/379605.379687"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"C. Flanagan, S.N. Freund, and S. Qadeer, \u201cThread-modular verification for shared-memory programs,\u201d in Proc. European Symposium on Programming (ESOP), 2002, pp. 262\u2013277.","DOI":"10.1007\/3-540-45927-8_19"},{"key":"3_CR7","unstructured":"C. Flanagan, S. Qadeer, and S. Seshia, \u201cA modular checker for multithreaded programs,\u201d in Proc. 14th Int'l. Conference on Computer-Aided Verification (CAV), vol. 2404 of Lecture Notes in Computer Science, Springer-Verlag, 2002, pp. 180\u2013194."},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"C. Flanagan and S. Qadeer, \u201cTransactions for software model checking,\u201d in Proc. 2nd Workshop on Software Model Checking, vol. 89(3) of Electronic Notes in Theoretical Computer Science. Elsevier, 2003.","DOI":"10.1016\/S1571-0661(05)82560-5"},{"key":"3_CR9","unstructured":"P. Godefroid, Partial-Order Methods for the Verification of Concurrent Systems, vol. 1032 of Lecture Notes in Computer Science. Springer-Verlag, 1996."},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"P. Godefroid, \u201cModel checking for programming languages using VeriSoft,\u201d in Proc. 24th ACM Symposium on Principles of Programming Languages (POPL), ACM Press, 1997, pp. 174\u2013186.","DOI":"10.1145\/263699.263717"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"K. Havelund and T. Pressburger, \u201cModel checking Java programs using Java PathFinder,\u201d Int. J. on Softw. Tools for Technol. Trans., Vol. 2, No. 4, 2000.","DOI":"10.1007\/s100090050043"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"G.J. Holzmann, \u201cThe Spin model checker,\u201d IEEE Trans. Softw. Engi., Vol. 23, No. 5, pp. 279\u2013295, 1997.","DOI":"10.1109\/32.588521"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"G.J. Holzmann and D. Peled, \u201cAn improvement in formal verification,\u201d in Proc. 7th Int'l. Conference on Formal Description Techniques (FORTE \u203294), Chapman & Hall, 1995, pp. 197\u2013211.","DOI":"10.1007\/978-0-387-34878-0_13"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"D. Kozen, \u201cA completeness theorem for Kleene algebras and the algebra of regular events,\u201d Inform. Comput., Vol. 110, No. 2, pp. 366\u2013390, 1994.","DOI":"10.1006\/inco.1994.1037"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"R.J. Lipton, \u201cReduction: A method of proving properties of parallel programs,\u201d Communications of the ACM, Vol. 18, No. 12, pp. 717\u2013721, 1975.","DOI":"10.1145\/361227.361234"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T.E. Anderson, \u201cEraser: A dynamic data race detector for multi-threaded programs,\u201d ACM Trans. on Comp. Syst., Vol. 15, No. 4, pp. 391\u2013411, 1997.","DOI":"10.1145\/265924.265927"},{"key":"3_CR17","unstructured":"S.D. Stoller and E. Cohen, \u201cOptimistic synchronization-based state-space reduction,\u201d in Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), vol. 2619 of Lecture Notes in Computer Science, Springer-Verlag, 2003, pp. 489\u2013504."},{"key":"3_CR18","unstructured":"S.D. Stoller, \u201cModel-checking multi-threaded distributed Java programs,\u201d Int. J. on Softw. Tools for Technol. Trans., Vol. 4, No. 1, pp. 71\u201391, 2002."},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"A. Valmari, \u201cStubborn set methods for process algebras,\u201d in D. Peled, V.R. Pratt, and G.J. Holzmann (Eds.), Proc. Workshop on Partial Order Methods in Verification, vol. 29 of DIMACS Series, American Mathematical Society, 1997, pp. 213\u2013231.","DOI":"10.1090\/dimacs\/029\/12"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"C. von Praun and T.R. Gross, \u201cObject race detection,\u201d in Proc. 16th ACM Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), vol. 36(11) of SIGPLAN Notices, ACM Press, 2001, pp. 70\u201382.","DOI":"10.1145\/504311.504288"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"J. Whaley and M.C. Rinard, \u201cCompositional pointer and escape analysis for Java programs,\u201d in Proc. ACM Conf. on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), ACM Press, 1999, pp. 187\u2013206.","DOI":"10.1145\/320385.320400"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-0003-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-006-0003-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-0003-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T10:41:07Z","timestamp":1736419267000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-006-0003-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,5]]},"references-count":21,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2006,5]]}},"alternative-id":["3"],"URL":"https:\/\/doi.org\/10.1007\/s10703-006-0003-4","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2006,5]]}}}