pith. machine review for the scientific record. sign in

arxiv: 2605.02569 · v1 · submitted 2026-05-04 · 💻 cs.DB · cs.PL

Recognition: unknown

Static Type Checking for Database Access Code

Mattias Ulbrich, Stefanie Scherzinger, Thomas James Kirz, Werner Dietl

Pith reviewed 2026-05-08 02:08 UTC · model grok-4.3

classification 💻 cs.DB cs.PL
keywords static type checkingJDBCJava database accesstype safetyprepared statementsChecker Frameworkcompile-time verificationruntime error prevention
0
0 comments X

The pith

An extension to the Checker Framework statically verifies correct Java types in JDBC database access code.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents a static type checker for Java database access using JDBC. It checks that the right Java types are used when setting parameters in prepared statements and retrieving values from result sets. This moves a class of type-related runtime errors to compile time. The approach is sound, meaning it catches all such errors without false negatives. Developers can use it on unmodified code, even across methods, and it handles legacy code in a limited mode.

Core claim

We propose an extension of the Java compiler, based on the established Checker Framework, which allows us to bridge this gap. Our approach verifies statically that the correct Java types are used when setting prepared statement parameters or when getting values from result sets. This allows us to lift a practically important class of runtime errors to compile time. Our approach is sound and, therefore, is guaranteed not to produce false negatives.

What carries the argument

The JDBC type checker extension to the Checker Framework, which models the mappings between SQL types and Java types for parameter setting and result retrieval operations.

Load-bearing premise

The Checker Framework's type system extension must correctly model all JDBC type mappings, and any schema or annotation information must accurately reflect the actual database dictionary.

What would settle it

A program containing a JDBC type mismatch that passes the checker without error but causes a runtime type error when executed.

Figures

Figures reproduced from arXiv: 2605.02569 by Mattias Ulbrich, Stefanie Scherzinger, Thomas James Kirz, Werner Dietl.

Figure 1
Figure 1. Figure 1: JDBC 4.3 type conversions [3] for getters (excerpt). 2 PreparedStatement ps = conn . prepareStatement ( sql ); 3 ps . setInt (1 , quantity ); // Bind value of parameter '? ' 4 ResultSet rs = ps . executeQuery (); 5 while ( rs . next ()) { 6 System . out . println ( rs . getInt (" label ")); 7 } When executed repeatedly, with different parameter bindings, prepared statements can improve application performa… view at source ↗
Figure 2
Figure 2. Figure 2: Oopsie System architecture. this type information in automatically generated code annotations. For example, this allows Oopsie to resolve “SELECT *”-queries into higher-order SQL types, which list the order and attributes (with name and type) in the result set. The Oopsie extension has access to the JDBC-recommended type mappings (⃝4 ). Given the code annotations, the Java compiler can type-check the Java … view at source ↗
Figure 3
Figure 3. Figure 3: Steps of inferring Oopsie annotations and checking JDBC access code. The annotations inferred in each step are highlighted in blue and setter/getter-calls identified as correct or buggy are highlighted in green and red, respectively. 4.3.4 Verifying setter and getter calls. Whenever a getter/setter is called on a @Sql-annotated object, the type of the method can then be compared to the expected types store… view at source ↗
Figure 4
Figure 4. Figure 4: Confusion matrices for handwritten test suite: Pre view at source ↗
Figure 5
Figure 5. Figure 5: Ad-hoc analysis of functional software: Manually view at source ↗
Figure 6
Figure 6. Figure 6: Oopsie in degraded mode. Share of analyzable set￾ters (S) and getters (G) that can be type-checked ad-hoc vs. after manual annotation, or remain out of scope (OOS). developers are likely to find Oopsie useful out-of-the-box: Compared to tools like IntelliJ, Oopsie finds important errors that existing tools cannot detect. What stands out is the substantial share of non-local accesses in OSCAR, unlike with O… view at source ↗
read the original abstract

JDBC remains a key technology for database access in Java applications. Since the database dictionary and the Java type system have distinct scopes, developers inevitably need to deal with bugs in SQL-to-Java type mappings. We propose an extension of the Java compiler, based on the established Checker Framework, which allows us to bridge this gap. Our approach verifies statically that the correct Java types are used when setting prepared statement parameters or when getting values from result sets. This allows us to lift a practically important class of runtime errors to compile time. Our approach is sound and, therefore, is guaranteed not to produce false negatives. Our prototype implementation also offers a degraded mode for type-checking legacy software, if developers are only interested in a subset of errors. Our experiments show that our approach detects a wide range of type mismatches in realworld application code and can indeed prevent errors which might otherwise surface as runtime errors. From the perspective of the developer, our approach is extremely lightweight: it processes the unmodified Java code, yet developers may add their own annotations. This allows us to perform type-checking even across method boundaries, whereas commercial developer tools are restricted to local checks. Finally, we show that we can type-check real-world JDBC software with reasonable overhead during compilation.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper presents an extension of the Checker Framework that adds custom type qualifiers for static verification of JDBC calls in Java. It checks that Java types passed to PreparedStatement.setXXX methods and returned by ResultSet.getXXX methods are compatible with the underlying database schema (via annotations or provided metadata), with the goal of catching type-mismatch errors at compile time rather than runtime. The manuscript claims the system is sound with no false negatives, supports a degraded mode for legacy code, processes unmodified source, enables cross-method checking, and reports positive results on real-world applications with acceptable compilation overhead.

Significance. If the soundness claim holds, the work offers a practical, lightweight way to prevent a common source of runtime failures in Java database code. Strengths include reuse of the established Checker Framework, support for unmodified code plus optional annotations, and experimental validation on real applications. These elements could make the technique adoptable by developers and superior to purely local IDE checks.

major comments (2)
  1. [Abstract] Abstract: The central claim that the approach 'is sound and therefore guaranteed not to produce false negatives' is load-bearing. This guarantee rests on the assumption that the Checker Framework extension's qualifiers and subtyping relations completely and correctly encode every valid JDBC-to-Java mapping (including NULL semantics, numeric coercions, java.sql vs java.util date handling, getObject paths, and vendor extensions). The manuscript supplies no formal semantics for the type rules, no exhaustive enumeration against the JDBC specification, and no machine-checked proof or completeness argument; an omitted mapping would silently accept a runtime error.
  2. [Experiments] Experiments section: The paper states that the prototype 'detects a wide range of type mismatches in real-world application code' and prevents errors that would otherwise surface at runtime. However, without reported counts of errors found, false-positive rates, the specific applications or codebases tested, or a comparison against baseline tools, it is impossible to assess coverage, precision, or the practical impact of the soundness guarantee.
minor comments (2)
  1. The description of how schema or annotation information is supplied to the checker (e.g., via @DatabaseSchema or similar) could be clarified with a concrete example showing propagation across method boundaries.
  2. A table enumerating the supported JDBC type mappings and their Java qualifiers would improve readability and allow readers to spot potential gaps.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the detailed and constructive review. We address each major comment below, clarifying our claims and indicating where the manuscript will be revised to strengthen the presentation.

read point-by-point responses
  1. Referee: [Abstract] Abstract: The central claim that the approach 'is sound and therefore guaranteed not to produce false negatives' is load-bearing. This guarantee rests on the assumption that the Checker Framework extension's qualifiers and subtyping relations completely and correctly encode every valid JDBC-to-Java mapping (including NULL semantics, numeric coercions, java.sql vs java.util date handling, getObject paths, and vendor extensions). The manuscript supplies no formal semantics for the type rules, no exhaustive enumeration against the JDBC specification, and no machine-checked proof or completeness argument; an omitted mapping would silently accept a runtime error.

    Authors: We acknowledge that the manuscript does not include a formal semantics, exhaustive enumeration, or machine-checked proof of the type system. Our soundness claim is grounded in the established soundness of the Checker Framework combined with a manual encoding of the core JDBC type mappings (as documented in the JDBC specification) into the qualifier hierarchy. The implementation handles standard cases for setXXX/getXXX, NULL semantics via nullable qualifiers, numeric coercions, and java.sql date types, while getObject is supported via a general Object qualifier. Vendor extensions are noted as out of scope due to their variability. To address the concern, we will revise the paper to add a dedicated subsection that explicitly enumerates the supported mappings and subtyping rules, including the cases mentioned. This provides transparency without requiring a full formalization, which is outside the scope of this practical systems paper. revision: yes

  2. Referee: [Experiments] Experiments section: The paper states that the prototype 'detects a wide range of type mismatches in real-world application code' and prevents errors that would otherwise surface at runtime. However, without reported counts of errors found, false-positive rates, the specific applications or codebases tested, or a comparison against baseline tools, it is impossible to assess coverage, precision, or the practical impact of the soundness guarantee.

    Authors: We agree that additional quantitative details would strengthen the evaluation. The current manuscript reports qualitative results on real-world code but lacks specific counts, false-positive analysis, and tool comparisons. We will revise the Experiments section to include: the exact number of type mismatches detected across the tested applications, the names and sizes of the specific open-source codebases evaluated, a manual verification of precision (including false-positive rate), and a brief comparison to local IDE checks. These additions will better demonstrate coverage and practical impact while remaining consistent with the paper's focus on feasibility. revision: yes

Circularity Check

0 steps flagged

No circularity: implementation relies on external Checker Framework foundations

full rationale

The paper describes an extension of the Checker Framework to add qualifiers and subtyping rules for JDBC type mappings in Java. Its central soundness claim rests on the modeling assumption that the added rules correctly capture all JDBC-to-Java conversions, which is an external modeling choice rather than a derivation that reduces to fitted parameters or self-referential equations. No equations, predictions, or self-citations are used to justify the core result; the work is a tool implementation whose guarantees are conditional on the completeness of the manually supplied type rules and the soundness of the underlying Checker Framework. This is the normal case of a non-circular engineering paper.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the soundness of the Checker Framework's annotation-based type system and the accuracy of any user-provided type mappings or schema information; no free parameters, invented entities, or ad-hoc axioms are introduced in the abstract.

axioms (1)
  • domain assumption The Checker Framework extension correctly encodes JDBC type mappings without false negatives.
    Stated directly in the abstract as the basis for the soundness guarantee.

pith-pipeline@v0.9.0 · 5521 in / 1264 out tokens · 29797 ms · 2026-05-08T02:08:16.860046+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

48 extracted references · 30 canonical work pages

  1. [1]

    Sayed Abdul-Aziz. 2021. JDBC-Course. https://github.com/sayedabdul- aziz/JDBC-Course/tree/04ed1613c612f8d9ae53ef7629c3cb254d6cad40

  2. [2]

    Ambler and Pramodkumar J

    Scott W. Ambler and Pramodkumar J. Sadalage. 2006. Refactoring Databases: Evolutionary Database Design . Addison-Wesley Professional

  3. [3]

    Lance Andersen. 2017. Java Database Connectivity (JDBC) 4.3 Specification (Maintenance Release, JSR-221). https://download.oracle.com/otn-pub/jcp/jdbc- 4_3-mrel3-eval-spec/jdbc4.3-fr-spec.pdf . Accessed: May 5, 2026. 10https://jspecify.dev/ Static Type Checking for Database Access Code

  4. [4]

    Aivar Annamaa, Andrey Breslav, Jevgeni Kabanov, and Varmo Vene. 2010. An Interactive Tool for Analyzing Embedded SQL Queries. In Programming Lan- guages and Systems , Kazunori Ueda (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 131–138

  5. [5]

    Mior, and Daniel Lemire

    Edmon Begoli, Jesús Camacho-Rodríguez, Julian Hyde, Michael J. Mior, and Daniel Lemire. 2018. Apache Calcite: A Foundational Framework for Optimized Query Processing Over Heterogeneous Data Sources. InProc. SIGMOD. 10 pages. doi:10.1145/3183713.3190662

  6. [6]

    Weber, and Anthony Cleve

    Mathieu Beine, Nicolas Hames, Jens H. Weber, and Anthony Cleve. 2014. Bidi- rectional Transformations in Database Evolution: A Case Study ”At Scale”. In Proceedings of the Workshops of the EDBT/ICDT 2014 Joint Conference (EDBT/ICDT 2014), Athens, Greece, March 28, 2014 (CEUR Workshop Proceedings, Vol. 1133). CEUR-WS.org, 100–107. https://ceur-ws.org/Vol-1...

  7. [7]

    Joshua Bloch. 2008. Effective Java: A Programming Language Guide (2nd revised edition (rev). ed.). Addison-Wesley Longman, Amsterdam. http://www.amaz on.de/Effective-Java-Programming-Language-Guide/dp/0321356683/ref=sr_1 _1?ie=UTF8&qid=1303414280&sr=8-1

  8. [8]

    Gilad Bracha. 2004. Pluggable type systems. In Proc. OOPSLA’04 Workshop on Revival of Dynamic Languages

  9. [9]

    Hassan, Mohamed Nasser, and Parminder Flora

    Tse-Hsun Chen, Weiyi Shang, Zhen Ming Jiang, Ahmed E. Hassan, Mohamed Nasser, and Parminder Flora. 2014. Detecting performance anti-patterns for applications developed using object-relational mapping. In Proc. ICSE. doi:10.1 145/2568225.2568259

  10. [10]

    Hassan, Michael W

    Tse-Hsun Chen, Weiyi Shang, Jinqiu Yang, Ahmed E. Hassan, Michael W. God- frey, Mohamed Nasser, and Parminder Flora. 2016. An Empirical Study on the Practice of Maintaining Object-Relational Mapping Code in Java Systems. In Proc. MSR. doi:10.1145/2901739.2901758

  11. [11]

    Schwartzbach

    Aske Simon Christensen, Anders Møller, and Michael I. Schwartzbach. 2003. Precise Analysis of String Expressions. In Static Analysis, Radhia Cousot (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 1–18

  12. [12]

    Justin Clarke, Kevvie Fowler, Erlend Oftedal, Rodrigo Marcos Alvarez, Dave Hartley, Alexander Kornbrust, Gary O’Leary-Steele, Alberto Revelli, Sumit Sid- dharth, and Marco Slaviero. 2009. SQL Injection Attacks and Defense (2 ed.). Syngress Publishing

  13. [13]

    Anthony Cleve, Maxime Gobert, Loup Meurice, Jerome Maes, and Jens H. Weber

  14. [14]

    Understanding database schema evolution: A case study. Sci. Comput. Program. 97 (2015), 113–121. doi:10.1016/J.SCICO.2013.11.025

  15. [15]

    Carlo Curino, Hyun Jin Moon, and Carlo Zaniolo. 2008. Graceful database schema evolution: the PRISM workbench. Proc. VLDB Endow. 1, 1 (2008), 761–

  16. [16]

    doi:10.14778/1453856.1453939

  17. [17]

    Alexandre Decan, Mathieu Goeminne, and Tom Mens. 2017. On the Interaction of Relational Database Access Technologies in Open Source Java Projects. CoRR abs/1701.00416 (2017). arXiv: 1701.00416 http://arxiv.org/abs/1701.00416

  18. [18]

    Checker Framework developers. 2025. The Checker Framework Manual: Cus- tom pluggable types for Java. https://checkerframework.org/manual/. Version 3.49.1

  19. [19]

    Ernst, Kivanç Muslu, and Todd Schiller

    Werner Dietl, Stephanie Dietzel, Michael D. Ernst, Kivanç Muslu, and Todd Schiller. 2011. Building and Using Pluggable Type-Checkers. In Proc. ICSE . doi:10.1145/1985793.1985889

  20. [20]

    Jens Dittrich. 2025. How to get Rid of SQL, Relational Algebra, the Relational Model, ERM, and ORMs in a Single Paper - A Thought Experiment. CoRR abs/2504.12953 (2025). arXiv: 2504.12953 doi:10.48550/ARXIV.2504.12953

  21. [21]

    EISOP. 2026. The EISOP Checker Framework. https://eisop.github.io/cf/ . Accessed: 2026-04-28

  22. [22]

    Maxime Gobert, Csaba Nagy, Henrique Rocha, Serge Demeyer, and Anthony Cleve. 2023. Best practices of testing database manipulation code. Inf. Syst. 111, C (Jan. 2023), 15 pages. doi:10.1016/j.is.2022.102105

  23. [23]

    Mathieu Goeminne, Alexandre Decan, and Tom Mens. 2014. Co-evolving code- related and database-related changes in a data-intensive software system. In 2014 Software Evolution Week - IEEE Conference on Software Maintenance, Reengi- neering, and Reverse Engineering, CSMR-WCRE . 353–357. doi:10.1109/CSMR- WCRE.2014.6747193

  24. [24]

    Mathieu Goeminne and Tom Mens. 2015. Towards a survival analysis of data- base framework usage in Java projects. In Proc. ICSME. doi:10.1109/ICSM.2015. 7332512

  25. [25]

    Gould, Z

    C. Gould, Z. Su, and P. Devanbu. 2004. Static checking of dynamically generated queries in database applications. In Proceedings. 26th International Conference on Software Engineering. 645–654. doi:10.1109/ICSE.2004.1317486

  26. [26]

    Carl Gould, Zhendong Su, and Premkumar T. Devanbu. 2004. JDBC Checker: A Static Analysis Tool for SQL/JDBC Applications. In Proc. ICSE. IEEE Computer Society. doi:10.1109/ICSE.2004.1317494

  27. [27]

    Mike Hinchey. 2018. Analyzing the Evolution of Database Usage in Data‐Intensive Software Systems. 208–240. doi:10.1002/9781119174240.ch12

  28. [28]

    JetBrains. 2024. IntelliJ IDEA 2024.3: Database Tools and SQL . JetBrains. https: //www.jetbrains.com/help/idea/2024.3/relational-databases.html

  29. [29]

    Martin Kellogg, Vlastimil Dort, Suzanne Millstein, and Michael D. Ernst. 2018. Lightweight verification of array indexing. In International Symposium on Soft- ware Testing and Analysis (ISSTA). 3–14. doi:10.1145/3213846.3213849

  30. [30]

    Thomas James Kirz. 2025. OPSC: Catching the ”Oops” in JDBC PreparedState- ments with Static Code Analysis. In Proc. BTW, Student Track . doi:10.18420/B TW2025-64

  31. [31]

    Florian Lanzinger, Alexander Weigl, Mattias Ulbrich, and Werner Dietl. 2021. Scalability and Precision by Combining Expressive Type Systems and Deductive Verification. Proc. OOPSLA (2021). doi:10.1145/3485520

  32. [32]

    McMaster University. 2025. OSCAR-EMR. https://bitbucket.org/oscaremr/osc ar/src/cca70ec9a265370992a8f55d5bcb82d011c4b6ac/

  33. [33]

    Erik Meijer, Brian Beckman, and Gavin Bierman. 2006. LINQ: reconciling ob- ject, relations and XML in the .NET framework. In Proceedings of the 2006 ACM SIGMOD International Conference on Management of Data (Chicago, IL, USA) (SIGMOD ’06). New York, NY, USA, 706. doi:10.1145/1142473.1142552

  34. [34]

    Loup Meurice and Anthony Cleve. 2014. DAHLIA: A visual analyzer of data- base schema evolution. In 2014 Software Evolution Week - IEEE Conference on Software Maintenance, Reengineering, and Reverse Engineering, CSMR-WCRE 2014, Antwerp, Belgium, February 3-6, 2014 . IEEE Computer Society, 464–468. doi:10.1109/CSMR-WCRE.2014.6747219

  35. [36]

    Loup Meurice, Csaba Nagy, and Anthony Cleve. 2016. Detecting and Prevent- ing Program Inconsistencies under Database Schema Evolution. In 2016 IEEE International Conference on Software Quality, Reliability and Security, QRS 2016, Vienna, Austria, August 1-3, 2016 . IEEE, 262–273. doi:10.1109/QRS.2016.38

  36. [37]

    Loup Meurice, Csaba Nagy, and Anthony Cleve. 2016. Static Analysis of Dy- namic Database Usage in Java Systems. In Proc. CAISE. doi:10.1007/978-3-319- 39696-5_30

  37. [38]

    Csaba Nagy and Anthony Cleve. 2017. A Static Code Smell Detector for SQL Queries Embedded in Java Code. In Proc. SCAM. doi:10.1109/SCAM.2017.19

  38. [39]

    Csaba Nagy and Anthony Cleve. 2018. SQLInspect: a static analyzer to inspect database usage in Java applications. In Proceedings of the 40th International Con- ference on Software Engineering: Companion Proceeedings, ICSE 2018, Gothenburg, Sweden, May 27 - June 03, 2018 . ACM, 93–96. doi:10.1145/3183440.3183496

  39. [40]

    Csaba Nagy, Loup Meurice, and Anthony Cleve. 2015. Where was this SQL query executed? a static concept location approach. In 2015 IEEE 22nd Interna- tional Conference on Software Analysis, Evolution, and Reengineering (SANER) . 580–584. doi:10.1109/SANER.2015.7081881

  40. [41]

    Papi, Mahmood Ali, Telmo Luis Correa, Jeff H

    Matthew M. Papi, Mahmood Ali, Telmo Luis Correa, Jeff H. Perkins, and Michael D. Ernst. 2008. Practical pluggable types for Java. In Proc. ISSTA . doi:10.1145/1390630.1390656

  41. [42]

    Dong Qiu, Bixin Li, and Zhendong Su. 2013. An empirical analysis of the co- evolution of schema and code in database applications. In Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering (ESEC/FSE 2013) . New York, NY, USA, 125–135. doi:10.1145/2491411.2491431

  42. [43]

    George Reese. 2000. Database Programming with JDBC and Java, Second Edition. O’Reilly Media, Inc

  43. [44]

    Ilkka Seppälä. 2022. Design Patterns Implemented in Java. https://github.com /iluwatar/java-design-patterns/blob/163c3017bb356937d876cd9a05905c012f3b 0af6/transaction-script/src/main/java/com/iluwatar/transactionscript/HotelD aoImpl.java

  44. [45]

    The OpenNMS Group, Inc. 2025. OpenNMS. https://github.com/OpenNMS/ope nnms

  45. [46]

    Williams, and Tao Xie

    Stephen Thomas, Laurie A. Williams, and Tao Xie. 2009. On automated prepared statement generation to remove SQL injection vulnerabilities.Inf. Softw. Technol. 51, 3 (2009), 589–598. doi:10.1016/J.INFSOF.2008.08.002

  46. [47]

    Mario Linares Vásquez, Boyang Li, Christopher Vendome, and Denys Poshy- vanyk. 2016. Documenting database usages and schema constraints in database- centric applications. In Proceedings of the 25th International Symposium on Soft- ware Testing and Analysis, ISSTA 2016, Saarbrücken, Germany, July 18-20, 2016 . ACM, 270–281. doi:10.1145/2931037.2931072

  47. [48]

    Ricardo Vilaça. 2013. Escada TPC-C. https://github.com/rmpvilaca/EscadaTPC- C/tree/ff15fbf99b39c81725937e11b8eb9665834bfefb

  48. [49]

    Luo, and Werner Dietl

    Tongtong Xiang, Jeff Y. Luo, and Werner Dietl. 2020. Precise inference of expres- sive units of measurement types. Proc. OOPSLA (2020). doi:10.1145/3428210