{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:59:49Z","timestamp":1750309189476,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":26,"publisher":"ACM","license":[{"start":{"date-parts":[[2008,10,27]],"date-time":"2008-10-27T00:00:00Z","timestamp":1225065600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2008,10,27]]},"DOI":"10.1145\/1455770.1455793","type":"proceedings-article","created":{"date-parts":[[2008,11,6]],"date-time":"2008-11-06T13:49:50Z","timestamp":1225979390000},"page":"161-174","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":29,"title":["Verifiable functional purity in java"],"prefix":"10.1145","author":[{"given":"Matthew","family":"Finifter","sequence":"first","affiliation":[{"name":"University of California, Berkeley, Berkeley, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adrian","family":"Mettler","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, Berkeley, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naveen","family":"Sastry","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, Berkeley, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Wagner","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, Berkeley, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2008,10,27]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2007.24"},{"key":"e_1_3_2_1_2_1","volume-title":"High Integrity Software: The SPARK Approach to Safety and Security","author":"Barnes J.","year":"2003","unstructured":"J. Barnes . High Integrity Software: The SPARK Approach to Safety and Security . Addison-Wesley Longman Publishing Co., Inc. , Boston, MA, USA , 2003 . J. Barnes. High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 2003."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1314466.1314467"},{"key":"e_1_3_2_1_5_1","unstructured":"W. Bright. D language 2.0. http:\/\/www.digitalmars.com\/d\/2.0\/.  W. Bright. D language 2.0. http:\/\/www.digitalmars.com\/d\/2.0\/."},{"key":"e_1_3_2_1_6_1","unstructured":"L. Brown. AEScalc. http:\/\/www.unsw.adfa.edu.au\/~lpb\/src\/AEScalc\/AEScalc.jar.  L. Brown. AEScalc. http:\/\/www.unsw.adfa.edu.au\/~lpb\/src\/AEScalc\/AEScalc.jar."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0167-4"},{"key":"e_1_3_2_1_8_1","volume-title":"A runtime assertion checker for the Java Modeling Language","author":"Cheon Y.","year":"2002","unstructured":"Y. Cheon and G. Leavens . A runtime assertion checker for the Java Modeling Language , 2002 . Y. Cheon and G. Leavens. A runtime assertion checker for the Java Modeling Language, 2002."},{"key":"e_1_3_2_1_9_1","unstructured":"T. Close and S. Butler. Waterken server. http:\/\/waterken.sourceforge.net\/.  T. Close and S. Butler. Waterken server. http:\/\/waterken.sourceforge.net\/."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/858336.858337"},{"key":"e_1_3_2_1_11_1","unstructured":"HTML4 Test Suite. http:\/\/www.w3.org\/MarkUp\/Test\/HTML401\/current\/.  HTML4 Test Suite. http:\/\/www.w3.org\/MarkUp\/Test\/HTML401\/current\/."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/0096-0551(95)00008-9"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/268998.266644"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/954666.971189"},{"key":"e_1_3_2_1_15_1","volume-title":"Design by contract with JML","author":"Leavens G.","year":"2003","unstructured":"G. Leavens and Y. Cheon . Design by contract with JML , 2003 . G. Leavens and Y. Cheon. Design by contract with JML, 2003."},{"key":"e_1_3_2_1_17_1","series-title":"Object-Oriented Series","volume-title":"Eiffel: The Language","author":"Meyer B.","unstructured":"B. Meyer . Eiffel: The Language . Object-Oriented Series . Prentice Hall , Englewood Cliffs, NJ, USA , B. Meyer. Eiffel: The Language. Object-Oriented Series. Prentice Hall, Englewood Cliffs, NJ, USA,"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/268998.266669"},{"key":"e_1_3_2_1_20_1","unstructured":"D. Oswald S. Raha I. Macfarlane and D. Walters. HTMLParser 1.6. http:\/\/htmlparser.sourceforge.net\/.  D. Oswald S. Raha I. Macfarlane and D. Walters. HTMLParser 1.6. http:\/\/htmlparser.sourceforge.net\/."},{"key":"e_1_3_2_1_21_1","first-page":"82","volume-title":"ICSM '04: Proceedings of the 20th IEEE International Conference on Software Maintenance","author":"Precise","year":"2004","unstructured":"Precise identification of side-effect-free methods in java . In ICSM '04: Proceedings of the 20th IEEE International Conference on Software Maintenance , pages 82 -- 91 , Washington, DC, USA , 2004 . IEEE Computer Society. Precise identification of side-effect-free methods in java. In ICSM '04: Proceedings of the 20th IEEE International Conference on Software Maintenance, pages 82--91, Washington, DC, USA, 2004. IEEE Computer Society."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/505586.505589"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_14"},{"key":"e_1_3_2_1_24_1","unstructured":"Verifying Security Properties in Electronic Voting Machines. PhD thesis University of California at Berkeley 2007.  Verifying Security Properties in Electronic Voting Machines. PhD thesis University of California at Berkeley 2007."},{"key":"e_1_3_2_1_25_1","unstructured":"F. Sauer. Eclipse metrics plugin 1.3.6. http:\/\/metrics.sourceforge.net\/.  F. Sauer. Eclipse metrics plugin 1.3.6. http:\/\/metrics.sourceforge.net\/."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094828"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143169"},{"key":"e_1_3_2_1_28_1","volume-title":"Auditors: An extensible, dynamic code verification mechanism","author":"Yee K.-P.","year":"2003","unstructured":"K.-P. Yee and M. Miller . Auditors: An extensible, dynamic code verification mechanism , 2003 . http:\/\/www.erights.org\/elang\/kernel\/auditors\/index.html. K.-P. Yee and M. Miller. Auditors: An extensible, dynamic code verification mechanism, 2003. http:\/\/www.erights.org\/elang\/kernel\/auditors\/index.html."}],"event":{"name":"CCS08: 15th ACM Conference on Computer and Communications Security 2008","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control","ACM Association for Computing Machinery"],"location":"Alexandria Virginia USA","acronym":"CCS08"},"container-title":["Proceedings of the 15th ACM conference on Computer and communications security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1455770.1455793","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1455770.1455793","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:54:14Z","timestamp":1750287254000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1455770.1455793"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,10,27]]},"references-count":26,"alternative-id":["10.1145\/1455770.1455793","10.1145\/1455770"],"URL":"https:\/\/doi.org\/10.1145\/1455770.1455793","relation":{},"subject":[],"published":{"date-parts":[[2008,10,27]]},"assertion":[{"value":"2008-10-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}