{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:43Z","timestamp":1774837843518,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":37,"publisher":"ACM","license":[{"start":{"date-parts":[[2012,6,12]],"date-time":"2012-06-12T00:00:00Z","timestamp":1339459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-11-2-0221"],"award-info":[{"award-number":["FA8750-11-2-0221"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2012,6,12]]},"DOI":"10.1145\/2318202.2318210","type":"proceedings-article","created":{"date-parts":[[2012,7,3]],"date-time":"2012-07-03T11:53:15Z","timestamp":1341316395000},"page":"42-49","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":34,"title":["Verification games"],"prefix":"10.1145","author":[{"given":"Werner","family":"Dietl","sequence":"first","affiliation":[{"name":"University of Washington"}]},{"given":"Stephanie","family":"Dietzel","sequence":"additional","affiliation":[{"name":"University of Washington"}]},{"given":"Michael D.","family":"Ernst","sequence":"additional","affiliation":[{"name":"University of Washington"}]},{"given":"Nathaniel","family":"Mote","sequence":"additional","affiliation":[{"name":"University of Washington"}]},{"given":"Brian","family":"Walker","sequence":"additional","affiliation":[{"name":"University of Washington"}]},{"given":"Seth","family":"Cooper","sequence":"additional","affiliation":[{"name":"University of Washington"}]},{"given":"Timothy","family":"Pavlik","sequence":"additional","affiliation":[{"name":"University of Washington"}]},{"given":"Zoran","family":"Popovi\u0107","sequence":"additional","affiliation":[{"name":"University of Washington"}]}],"member":"320","published-online":{"date-parts":[[2012,6,12]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1251535.1251543"},{"key":"e_1_3_2_1_2_1","first-page":"35","volume-title":"FMCAD","author":"Ball T.","year":"2010","unstructured":"T. Ball , E. Bounimova , R. Kumar , and V. Levin . SLAM2: static driver verification with under 4% false alarms . In FMCAD , pages 35 -- 42 , 2010 . T. Ball, E. Bounimova, R. Kumar, and V. Levin. SLAM2: static driver verification with under 4% false alarms. In FMCAD, pages 35--42, 2010."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1965724.1965743"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development","author":"Bertot Y.","year":"2004","unstructured":"Y. Bertot and P. Cast\u00e9ran . Interactive Theorem Proving and Program Development ; Coq'Art: The Calculus of Inductive Constructions. Springer-Verlag , 2004 . Y. Bertot and P. Cast\u00e9ran. Interactive Theorem Proving and Program Development; Coq'Art: The Calculus of Inductive Constructions. Springer-Verlag, 2004."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1028976.1028980"},{"key":"e_1_3_2_1_7_1","volume-title":"RDL","author":"Bracha G.","year":"2004","unstructured":"G. Bracha . Pluggable type systems . In RDL , Oct. 2004 . G. Bracha. Pluggable type systems. In RDL, Oct. 2004."},{"key":"e_1_3_2_1_8_1","unstructured":"Checker Framework website. http:\/\/types.cs.washington.edu\/checker-framework\/.  Checker Framework website. http:\/\/types.cs.washington.edu\/checker-framework\/."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2159365.2159367"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1038\/nature09304"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1822348.1822354"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263744"},{"key":"e_1_3_2_1_15_1","first-page":"227","volume-title":"Verified Software: Theories","author":"Cousot P.","year":"2007","unstructured":"P. Cousot . The verification grand challenge and abstract interpretation . In Verified Software: Theories , Tools, Experiments , pages 227 -- 240 . Dec. 2007 . P. Cousot. The verification grand challenge and abstract interpretation. In Verified Software: Theories, Tools, Experiments, pages 227--240. Dec. 2007."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325699"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985889"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032497.2032520"},{"key":"e_1_3_2_1_21_1","first-page":"24","volume-title":"WODA","author":"Ernst M. D.","year":"2003","unstructured":"M. D. Ernst . Static and dynamic analysis: Synergy and duality . In WODA , pages 24 -- 27 , May 2003 . M. D. Ernst. Static and dynamic analysis: Synergy and duality. In WODA, pages 24--27, May 2003."},{"key":"e_1_3_2_1_22_1","unstructured":"D. Greenfieldboyce and J. S. Foster. Type qualifiers for Java. http:\/\/www.cs.umd.edu\/Grad\/scholarlypapers\/papers\/greenfiledboyce.pdf Aug. 8 2005.  D. Greenfieldboyce and J. S. Foster. Type qualifiers for Java. http:\/\/www.cs.umd.edu\/Grad\/scholarlypapers\/papers\/greenfiledboyce.pdf Aug. 8 2005."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297027.1297051"},{"key":"e_1_3_2_1_24_1","unstructured":"Web interface to the Julia analyzer. http:\/\/julia.scienze.univr.it.  Web interface to the Julia analyzer. http:\/\/julia.scienze.univr.it."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1743546.1743574"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_27_1","volume-title":"Bibliopolis","author":"Martin-L\u00f6f P.","year":"1984","unstructured":"P. Martin-L\u00f6f . Intuitionistic type theory: notes by Giovanni Sambin of a series of lectures given in Padua. Studies in proof theory\/Lecture notes, 1 . Bibliopolis , 1984 . P. Martin-L\u00f6f. Intuitionistic type theory: notes by Giovanni Sambin of a series of lectures given in Padua. Studies in proof theory\/Lecture notes, 1. Bibliopolis, 1984."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_26"},{"key":"e_1_3_2_1_29_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL --- A Proof Assistant for Higher-Order Logic","author":"Nipkow T.","year":"2002","unstructured":"T. Nipkow , L. Paulson , and M. Wenzel . Isabelle\/HOL --- A Proof Assistant for Higher-Order Logic , volume 2283 of Lecture Notes in Computer Science . 2002 . T. Nipkow, L. Paulson, and M. Wenzel. Isabelle\/HOL --- A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. 2002."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390656"},{"key":"e_1_3_2_1_31_1","volume-title":"MIT Dept. of EECS","author":"Quinonez J.","year":"2008","unstructured":"J. Quinonez . Inference of reference immutability in Java. Master's thesis , MIT Dept. of EECS , May 2008 . J. Quinonez. Inference of reference immutability in Java. Master's thesis, MIT Dept. of EECS, May 2008."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70592-5_26"},{"key":"e_1_3_2_1_33_1","volume-title":"Lectures on the Curry-Howard Isomorphism. Studies in Logic and the Foundations of Mathematics","author":"S\u00f8rensen M. H.","year":"2006","unstructured":"M. H. S\u00f8rensen and P. Urzyczyn . Lectures on the Curry-Howard Isomorphism. Studies in Logic and the Foundations of Mathematics . 2006 . M. H. S\u00f8rensen and P. Urzyczyn. Lectures on the Curry-Howard Isomorphism. Studies in Logic and the Foundations of Mathematics. 2006."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2008.8"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939164"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-009-0132-5"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985826"},{"key":"e_1_3_2_1_38_1","volume-title":"MIT Dept. of EECS","author":"Tschantz M. S.","year":"2006","unstructured":"M. S. Tschantz . Javari : Adding reference immutability to Java. Master's thesis , MIT Dept. of EECS , Aug. 2006 . M. S. Tschantz. Javari: Adding reference immutability to Java. Master's thesis, MIT Dept. of EECS, Aug. 2006."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094828"}],"event":{"name":"ECOOP'12: 26th European Conference on Object-Oriented Programming","location":"Beijing China","acronym":"ECOOP'12","sponsor":["AITO Assoc Internationale por les Technologies Objects","SIGPLAN ACM Special Interest Group on Programming Languages","SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 14th Workshop on Formal Techniques for Java-like Programs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2318202.2318210","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2318202.2318210","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T11:05:57Z","timestamp":1750244757000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2318202.2318210"}},"subtitle":["making verification fun"],"short-title":[],"issued":{"date-parts":[[2012,6,12]]},"references-count":37,"alternative-id":["10.1145\/2318202.2318210","10.1145\/2318202"],"URL":"https:\/\/doi.org\/10.1145\/2318202.2318210","relation":{},"subject":[],"published":{"date-parts":[[2012,6,12]]},"assertion":[{"value":"2012-06-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}