java developers

Abstract: A dynamic invariant detector proposes invariants, such as method pre- and postconditions, and rules out those that do not hold at run time. Traditional detectors propose invariants from a fixed library of templates, which limits their expressiveness. A large language model (LLM) can propose invariants instead of, or in addition to, template-derived ones. With the right prompt and context choices, we found that this idea can both improve the invariants' expressiveness and reduce the cost of inferring the invariants. Greater expressiveness brings complications: an LLM-proposed invariant can execute arbitrary code during invariant evaluation, causing side effects or infinite loops. Our novel instrumentation strategies mitigate these problems. We wrap each candidate and evaluate only one invariant per thread at a time, so nested invariant evaluations cannot trigger one another indefinitely. To recover from non-nested hangs, we monitor each run for stalls and retry it under a growing time budget. Because we cannot prove a candidate side-effect-free in advance, we use delta debugging over the invariants evaluated during a failing test to isolate and disable a side-effecting candidate without discarding the rest of the run. We compared our implementation, Oca, to the popular template-based Daikon invariant detector on real open-source Java projects. Oca produces more expressive invariants: on average, 28% of its held invariants call a project-specific method, which Daikon's templates cannot express. Its invariants are more often valid, with a false-positive rate of 18% in a manual inspection, vs. 76% for Daikon, and more useful: as properties for property-based testing, they exposed 9 of 25 real bugs, compared with 4 for Daikon. Oca also costs less, using 566 minutes and 27 GB of disk, compared with 2,817 minutes and 827 GB for Daikon.

Abstract: Existing evaluation protocols for unit tests rely on aggregate metrics such as branch coverage and mutation score. These metrics quantify the extent to which a test suite exercises program behavior, but do not identify the behavioral obligations it systematically leaves unchecked. We propose BlindSpotEval, an obligation-based evaluation framework aligned with the Arrange-Act-Assert pattern. The framework comprises three metrics, Boundary-Value Adequacy, Control-Flow Adequacy, and Oracle Strength, complemented by an assessment of execution reliability. We also introduce ObligBench, a complexity-stratified Java benchmark comprising 895 complex and 700 low-complexity functions with source-side obligation annotations. Evaluating 14,320 tests from four LLMs under four prompting strategies reveals systematic blind spots. Incorrect assertions account for 15.6% of test failures, illustrating that coverage alone does not establish oracle correctness. Among executable tests, coverage of null, negative, and empty arguments reaches only 34.8%, 23.8%, and 38.8%, compared with average coverage above 93% for booleans. Catch blocks and default groups have Control-Flow Adequacy scores of only 0.100 and 0.312. Across both dimensions, LLM-generated tests exhibit the happy-path bias observed in human-written tests, concentrating on normal inputs and expected flows while leaving unusual values and exceptional paths unchecked. Oracle strength is high on average but uneven, with weaker assertions for object return property values and exceptions. These blind spots also occur in low-complexity functions, suggesting that code complexity alone does not explain them. BlindSpotEval provides construct-level adequacy profiles that identify under-tested obligation types and can guide targeted improvements beyond those supported by aggregate scores alone.

Abstract: Existing Java bug benchmarks offer limited method-level data for studying runtime-exception detection. Filtering Defects4J, Bugs.jar, Bears, and BugSwarm yields only 170 real buggy/fixed method pairs across seven unchecked exception types. We introduce RXSynth, a corpus of 4,275 synthetic Java method pairs generated from real bug/fix exemplars. We select the generator using structural alignment with real seeds and validate pairs using a two-stage patch-anchored procedure that identifies the labelled exception risk and checks whether the repair removes it. Independent JVM execution confirms patch-local validity for 84.2% of a stratified sample of 500 pairs. Provenance records enable evaluation without overlap between generation exemplars and test bugs. Structural analyses show good alignment within the represented size range, but compression of larger methods. We use RXSynth to compare isolated-method detection with pair discrimination when the repair is visible. Under provenance-controlled evaluation, supervised isolated-method ROC-AUC is about 0.55-0.64. Stronger zero-shot models reach about 69% accuracy but identify only 41.2% of repaired methods correctly. In contrast, fine-tuned encoders achieve 70.4-74.8% accuracy with both versions available. However, a simple token-growth rule achieves 84.7% expected accuracy, highlighting repair-direction cues. On 36 pairs without token growth, encoder accuracy falls to approximately chance, while GPT-5.5 and Gemini 3.1 Pro exceed 94%. RXSynth thus supports contrastive, patch-oriented, and context-aware studies; pairwise evaluations should control for provenance and directional surface cues before interpreting high accuracy as defect understanding.

Abstract: Method preconditions define the conditions that must be satisfied before a method is called. Often, such conditions are not documented and must be inferred. We present Prex, a pattern-based static analysis approach that infers preconditions from explicit checks in Java source code. For each precondition, Prex reports the condition required for a valid call and the reported exception in the case of a violation. Prex also attempts code transformations to convert the condition detected within a method's implementation into an expression that can be evaluated by client code. It leverages the concept of a mutation boundary to separate precondition checks from exceptions that may occur after the method changes the program state. We evaluated Prex from 46 open source Java projects and manually reviewed independent samples of 150 reports. Among the 150 Prex reports, 149 were correct and 125 of the correct reports were executable by client code. In a systematic comparison with an alternative approach based on path expansion, Prex provided more precise results. In total, 122 of the 149 correct reports had no relevant method documentation, and 41 required nontrivial source code analysis to recover manually. Overall, explicit source-code checks provide precondition information that can be absent from method documentation, and Prex can help recover it.

Abstract: Pluggable type systems extend the basic type system of a programming language by introducing additional type hierarchies to specify more complex properties and dependencies between variables. We consider the Constant Value Checker, a pluggable type checker for Java implemented using the Checker Framework, which provides various pluggable type systems and corresponding checkers. The Constant Value Checker lets users specify restrictions on the values a primitive integer or boolean variable can hold using a set or range of constant values. However, the current implementation of the Value Checker makes use of a limited set of syntactic typing rules that, in practice, often fail to verify well-typedness of more complex code. In this paper, we introduce an extension to the Checker Framework using Satisfiability Modulo Theories (SMT) solvers to address these limitations by creating corresponding first-order logic formulas for expressions whose type checks fail with the current syntactic typing rules and determining their well-typedness based on the satisfiability of these formulas. Furthermore, we introduce new dependent types for specifying allowed values with expressions that can depend on other variables in the program.

Abstract: Exception Related Code (ERC), which includes throw statements, conditions (if statements) that guard those throw statements, and try/catch blocks, is an essential component of software systems, allowing developers to detect and handle exceptional states that deviate from the expected program behavior. However, manually writing ERC across large codebases is tedious. We propose a novel task: retrofitting existing code with ERC. Namely, given code (without ERC) and Exceptional Behavior Tests (EBTs) (e.g., check if method throws InvalidArgumentException if null is given as the value to the argument) we aim to automatically generate missing ERC, such that the given tests pass. We design and implement Exception Coder (EXCODER) that performs context engineering to help Large Language Models (LLMs) tackle this task. EXCODER integrates static and dynamic program analysis with LLMs by providing the extracted contextual information to the LLMs. To evaluate EXCODER, we build a benchmark constructed from GitHub Java repositories, where we systematically remove ERC in 304 methods from 75 projects. Our results demonstrate that EXCODER provides an effective, though imperfect, solution to this problem in automated code generation, offering developers the first way to implement ERC following test-driven development. When combined with Qwen 2.5 Coder 32b, EXCODER achieves pass@1, 5, and 10 rates of 85.92% (12.56 percentage points over baseline), 86.18% (12.82 p.p. over baseline), and 86.51% (13.15 p.p. over baseline), respectively, on developer-written test suites. Our manual inspection of the generated code further reveals limitations of EXCODER, pointing to directions for future work.