一句话：提出 U-Turn，将不正确性逻辑与充分不正确性逻辑结合，复用前者启发式指导后者，增强错误分析。
不正确性逻辑（IL）检测可达错误状态而非证明程序正确，可避免误报；现有工作多将正确性与不正确性统一到单一证明系统。本文采取互补策略，将 IL 与寻找可能导致错误的输入状态的充分不正确性逻辑（SIL）结合。关键创新不是简单串联，而是复用第一个分析的启发式选择来引导第二个分析，例如选择性析取剪枝与循环展开，并用第一个逻辑的推导对第二个逻辑的证明规则进行插桩，以归纳地指导规则选择与应用。作者称这是首个支持分析间插桩的规则格式。该组合分析能同时揭示可达错误及其原因，有助于调试与测试，并为嵌入可扩展、自动化的代码契约开辟新途径。
O’Hearn’s Incorrectness Logic (IL) has sparked renewed interest in static analyses that aim to detect program errors rather than prove their absence, thereby avoiding false alarms—a critical factor for practical adoption in industrial settings. As new incorrectness logics emerge to capture diverse error-related properties, a key question arises: can combining correctness and incorrectness techniques enhance precision, expressiveness, automation, or scalability? Notable frameworks, such as outcome logic, UNTer, local completeness logic, and exact separation logic, unify multiple analyses within a single proof system. In this work, we adopt a complementary strategy. Rather than designing a unified logic, we combine IL, which identifies reachable error states, with Sufficient Incorrectness Logic (SIL), which finds input states potentially leading to those errors. As a result, we get a more informative and effective analysis than either logic in isolation. Rather than sequencing them, our key innovation is reusing heuristic choices from the first analysis to steer the second. In fact, both IL and SIL rely on under-approximation and thus their automation legitimizes heuristics that avoid exhaustive path enumeration (e.g., selective disjunct pruning, loop unrolling). Concretely, we instrument the proof rules of the second logic with derivations from the first to inductively guide rule selection and application. To our knowledge, this is the first rule format enabling such inter-analysis instrumentation. This combined analysis aids debugging and testing by revealing both reachable errors and their causes, and opens new avenues for embedding incorrectness insights into scalable, expressive, automated code contracts.
@article{paperbot3852,
title = {U-Turn: Enhancing Incorrectness Analysis by Reversing Direction},
author = {Flavio Ascari and Roberto Bruni and Roberta Gori and Azalea Raad},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776688}
}