{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:44:16Z","timestamp":1775868256285,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540242970","type":"print"},{"value":"9783540305798","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-30579-8_14","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T11:45:34Z","timestamp":1292845534000},"page":"199-215","source":"Crossref","is-referenced-by-count":122,"title":["Purity and Side Effect Analysis for Java Programs"],"prefix":"10.1007","author":[{"given":"Alexandru","family":"S\u0103lcianu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Rinard","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"14_CR1","unstructured":"Ananian, C.S.: MIT FLEX compiler infrastructure for Java (1998-2004), Available from http:\/\/www.flex-compiler.lcs.mit.edu"},{"key":"14_CR2","unstructured":"Birka, A.: Compiler-enforced immutability for the Java language. Technical Report MIT-LCS-TR-908, MIT Laboratory for Computer Science, Revision of Master\u2019s thesis (June 2003)"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Boyapati, C., Khurshid, S., Marinov, D.: Korat: Automated testing based on Java predicates. In: Proc. ISSTA (2002)","DOI":"10.1145\/566172.566191"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Boyapati, C., Rinard, M.C.: A parameterized type system for race-free Java programs. In: Proc. 16th OOPSLA (2001)","DOI":"10.1145\/504282.504287"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Burdy, L., Cheon, Y., Cok, D., Ernst, M.D., Kiniry, J., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. Technical Report NII-R0309, Computing Science Institute, Univ. of Nijmegen (2003)","DOI":"10.1016\/S1571-0661(04)80810-7"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Cahoon, B., McKinley, K.S.: Data flow analysis for software prefetching linked data structures in Java. In: Proc. 10th International Conference on Parallel Architectures and Compilation Techniques (2001)","DOI":"10.1109\/PACT.2001.953309"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Carlisle, M.C., Rogers, A.: Software caching and computation migration in Olden. In: Proc. 5th PPoPP (1995)","DOI":"10.1145\/209936.209941"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/3-540-36384-X_6","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"N. Cata\u00f1o","year":"2002","unstructured":"Cata\u00f1o, N., Huismann, M.: ChAsE: a static checker for JML\u2019s assignable clause. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 26\u201340. Springer, Heidelberg (2002)"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Choi, J.-D., Burke, M., Carini, P.: Efficient flow-sensitive interprocedural computation of pointer-induced aliases and side effects. In: Proc. 20th POPL (1993)","DOI":"10.1145\/158511.158639"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, D., Drossopoulou, S.: Ownership, encapsulation and the disjointness of type and effect. In: Proc. 17th OOPSLA (2002)","DOI":"10.1145\/582419.582447"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Corbett, J., Dwyer, M., Hatcliff, J., Pasareanu, C.: Bandera: Extracting finite-state models from Java source code. In: Proc. 22nd ICSE (2000)","DOI":"10.1145\/337180.337234"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Corbett, J.C.: Using shape analysis to reduce finite-state models of concurrent java programs. Software Engineering and Methodology\u00a09(1) (2000)","DOI":"10.1145\/332740.332741"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Crary, K., Walker, D., Morrisett, G.: Typed memory management in a calculus of capabilities. In: Proc. 26th POPL (1999)","DOI":"10.1145\/292540.292564"},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/978-3-540-24851-4_21","volume-title":"ECOOP 2004 \u2013 Object-Oriented Programming","author":"R. DeLine","year":"2004","unstructured":"DeLine, R., F\u00e4hndrich, M.: Typestates for objects. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol.\u00a03086, pp. 465\u2013490. Springer, Heidelberg (2004)"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lilibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended Static Checking for Java. In: Proc. PLDI (2002)","DOI":"10.1145\/512529.512558"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Hind, M., Pioli, A.: Which pointer analysis should I use? In: Proc. ISSTA (2000)","DOI":"10.1145\/347324.348916"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Jouvelot, P., Gifford, D.K.: Algebraic reconstruction of types and effects. In: Proc. 18th POPL (1991)","DOI":"10.1145\/99583.99623"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Lam, P., Rinard, M.: Role analysis. In: Proc. 29th POPL (2002)","DOI":"10.1145\/503272.503276"},{"key":"14_CR19","unstructured":"Kuncak, V., Leino, K.R.M.: In-place refinement for effect checking. In: 2nd Intl. Workshop on Automated Verification of Infinite-State Systems (2003)"},{"key":"14_CR20","unstructured":"Leavens, G.T.: Advances and issues in JML. In: Presentation at the Java Verification Workshop (2002)"},{"key":"14_CR21","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML. Technical Report 96-06p, Iowa State University (2001)"},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., Poetzsch-Heffter, A., Zhou, Y.: Using data groups to specify and check side effects. In: Proc. PLDI (2002)","DOI":"10.1145\/512529.512559"},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"Lucassen, J.M., Gifford, D.K.: Polymorphic effect systems. In: Proc. 15th POPL (1988)","DOI":"10.1145\/73560.73564"},{"key":"14_CR24","unstructured":"Marinov, D., Andoni, A., Daniliuc, D., Khurshid, S., Rinard, M.: An evaluation of exhaustive testing for data structures. Technical Report MIT-LCS-TR-921, MIT CSAIL, Cambridge, MA (2003)"},{"key":"14_CR25","doi-asserted-by":"crossref","unstructured":"Milanova, A., Rountev, A., Ryder, B.G.: Parameterized object sensitivity for points-to and side-effect analyses for Java. In: Proc. ISSTA (2002)","DOI":"10.1145\/566172.566174"},{"key":"14_CR26","unstructured":"Mueller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular specification of frame properties in JML. Technical Report TR 02-02, Iowa State University (2002)"},{"key":"14_CR27","doi-asserted-by":"crossref","unstructured":"Rinard, M., S\u0103lcianu, A., Bugrara, S.: A classification system and analysis for aspect-oriented programs. In: Proc. 12th FSE (2004)","DOI":"10.1145\/1029894.1029917"},{"key":"14_CR28","unstructured":"Rountev, A.: Precise identification of side-effect-free methods in Java. In: IEEE International Conference on Software Maintenance (2004)"},{"key":"14_CR29","unstructured":"Salcianu, A.: Pointer analysis and its applications to Java programs. Master\u2019s thesis, MIT Laboratory for Computer Science (2001)"},{"key":"14_CR30","unstructured":"Salcianu, A., Rinard, M.: A combined pointer and purity analysis for Java programs. Technical Report MIT-CSAIL-TR-949, MIT CSAIL (2004)"},{"key":"14_CR31","unstructured":"Spoto, F., Poll, E.: Static analysis for JML\u2019s assignable clauses. In: Proc. 10th FOOL (2003)"},{"key":"14_CR32","doi-asserted-by":"crossref","unstructured":"Tkachuk, O., Dwyer, M.B.: Adapting side effects analysis for modular program model checking. In: Proc. 11th FSE (2003)","DOI":"10.1145\/940071.940097"},{"key":"14_CR33","doi-asserted-by":"crossref","unstructured":"Tofte, M., Birkedal, L.: A region inference algorithm. Transactions on Programming Languages and Systems\u00a020(4) (1998)","DOI":"10.1145\/291891.291894"},{"key":"14_CR34","doi-asserted-by":"crossref","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S.: Model checking programs. In: Proc. 15th ASE (2000)","DOI":"10.1109\/ASE.2000.873645"},{"key":"14_CR35","doi-asserted-by":"crossref","unstructured":"Whaley, J., Rinard, M.: Compositional pointer and escape analysis for Java programs. In: Proc. 14th OOPSLA (1999)","DOI":"10.1145\/320384.320400"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30579-8_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,15]],"date-time":"2021-11-15T18:48:31Z","timestamp":1637002111000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30579-8_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540242970","9783540305798"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30579-8_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}