{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T11:08:23Z","timestamp":1790075303911,"version":"4.0.1"},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T00:00:00Z","timestamp":1780876800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,6,8]]},"abstract":"<jats:p>\n                    We propose\n                    <jats:italic toggle=\"yes\">error enumeration<\/jats:italic>\n                    , a method that aims to discover soundness defects in type analyzers by generating ill-typed programs by construction. Given a well-typed program\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mi>\ud835\udc43<\/mml:mi>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    , it systematically injects type mismatches at all possible program locations to explore ill-typed programs that differ from\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mi>\ud835\udc43<\/mml:mi>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    by replacing one expression with incompatible ones. The core contributions of our work are: (1) soundly injecting type mismatches even in the presence of type inference and refinements, and (2) enabling practical exploration of large seed programs by pruning the search space. Incomplete type information complicates the injection of type mismatches, as type inference can silently \"repair\" the injected error by adjusting inferred types in the surrounding context so that the program still type-checks. We address this by introducing a lightweight, usage-based reasoning technique that recovers missing types of program elements by leveraging the existing type annotations at each element\u2019s use site. This enables the injection of errors that guarantee type incompatibilities at the use sites of variables and other expressions. Finally, to prune the search space, we enumerate only those errors that ultimately lead to comparisons between types with distinct shape characteristics.\n                  <\/jats:p>\n                  <jats:p>\n                    We evaluated our implementation,\n                    <jats:sc>Eris<\/jats:sc>\n                    , on (1) three type analyzers integrated into the compilers of Kotlin, Scala, and Groovy, and (2) the Checker Framework, widely used to identify null-related errors in Java programs.\n                    <jats:sc>Eris<\/jats:sc>\n                    has uncovered 64 bugs caused by ill-typed programs: 51 leading to unsoundness, and 13 to compiletime crashes. Further investigation reveals that the majority of the soundness bugs discovered by Eris are triggered under highly complex conditions, where error injection requires (1) specific combinations of actual vs. expected type pairs at deeply-nested program locations, or (2) reasoning about control flow and missing type information, capabilities that lie beyond the scope of existing work.\n                  <\/jats:p>","DOI":"10.1145\/3808320","type":"journal-article","created":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T18:04:09Z","timestamp":1780941849000},"page":"1839-1863","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Enumerating Ill-Typed Programs for Testing Type Analyzers"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9906-3073","authenticated-orcid":false,"given":"Thodoris","family":"Sotiropoulos","sequence":"first","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2970-1391","authenticated-orcid":false,"given":"Zhendong","family":"Su","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,6,8]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/3022671.2984004"},{"key":"e_1_3_2_3_2","unstructured":"Apache Groovy Project. 2026. Apache Groovy Language Documentation: Flow Typing. https:\/\/groovy-lang.org\/semantics.html#section-flow-typing. Accessed online; March 24 2026."},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","unstructured":"Subarno Banerjee Lazaro Clapp and Manu Sridharan. 2019. NullAway: practical type-based null safety for Java (ESEC\/FSE 2019). Association for Computing Machinery New York NY USA 740\u2013750. doi:10.1145\/3338906.3338919","DOI":"10.1145\/3338906.3338919"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3485500"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523427"},{"key":"e_1_3_2_7_2","unstructured":"Checker Framework Developers. 2026. The Checker Framework Manual: Type Refinement. https:\/\/checkerframework.org\/manual\/#type-refinement-examples. Accessed online; March 24 2026."},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","unstructured":"Junjie Chen Yanwei Bai Dan Hao Yingfei Xiong Hongyu Zhang and Bing Xie. 2017. Learning to Prioritize Test Programs for Compiler Testing. In 2017 IEEE\/ACM 39th International Conference on Software Engineering (ICSE). 700\u2013711. doi:10.1109\/ICSE.2017.70","DOI":"10.1109\/ICSE.2017.70"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","unstructured":"Junjie Chen Yanwei Bai Dan Hao Yingfei Xiong Hongyu Zhang Lu Zhang and Bing Xie. 2016. Test Case Prioritization for Compilers: A Text-Vector Based Approach. In 2016 IEEE International Conference on Software Testing Verification and Validation (ICST). 266\u2013277. doi:10.1109\/ICST.2016.19","DOI":"10.1109\/ICST.2016.19"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/3729375"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/3363562"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_12"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2019.04.002"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2015.65"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985889"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454092"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/3450952"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3597926.3598130"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3691620.3695035"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632919"},{"key":"e_1_3_2_21_2","unstructured":"Google. 2024. Catch common Java mistakes as compile-time errors. https:\/\/errorprone.info\/. Online accessed; 14-11-2024."},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/3372123"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3660781"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3547653"},{"key":"e_1_3_2_25_2","unstructured":"JetBrains. 2026. Kotlin Documentation: Type Checks and Casts (Smart Casts). https:\/\/kotlinlang.org\/docs\/typecasts.html#smart-casts. Accessed online; March 24 2026."},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/3691620.3695034"},{"key":"e_1_3_2_27_2","unstructured":"Elad Kinsbruner Hila Peleg and Shachar Itzhaky. 2024. Kotlin\u2019s Type System is (Also) Unsound. arXiv preprint arXiv:2408.10804 (2024)."},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3360607"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594334"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814319"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3617232.3624874"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656386"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737986"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428264"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591295"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3763171"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/3728968"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009900"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/1982595.1982615"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390656"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/3763117"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254104"},{"key":"e_1_3_2_44_2","unstructured":"Scala Documentation Team. 2026. Scala 3 Reference: Explicit Nulls and Flow Typing. https:\/\/docs.scala-lang.org\/scala3\/reference\/experimental\/explicit-nulls.html#flow-typing. Accessed online; March 24 2026."},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632904"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","unstructured":"Thodoris Sotiropoulos and Zhendong Su. 2026. Artifact for \"Enumerating Ill-Typed Programs for Testing Type Analyzers\". doi:10.5281\/zenodo.19033618","DOI":"10.5281\/zenodo.19033618"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICST49551.2021.00044"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984038"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/3368826.3377927"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993570"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/3763094"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/3597926.3598087"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/3689719"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1145\/3611643.3616272"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1145\/3643759"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062379"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632910"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3808320","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T10:51:16Z","timestamp":1790074276000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3808320"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6,8]]},"references-count":57,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2026,6,8]]}},"alternative-id":["10.1145\/3808320"],"URL":"https:\/\/doi.org\/10.1145\/3808320","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,6,8]]},"assertion":[{"value":"2025-11-12","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-04-03","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-06-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}