Abstract
This paper explores the challenges of transitioning precise static analysis and verification techniques from specialized research tools to practical use by real-world programmers. A critical barrier is the inevitable loss of precision when analyzing complex, real-world programs, resulting in either excessive false positives or unsound analyses that leave errors undetected. We hypothesize that this precision loss is predominantly caused by a small subset of the code. To test this, we developed Concord, a prototype verifier based on the Compass tool, and validated this hypothesis on real-world code. Our findings highlight two key challenges: identifying where precision loss originates, often far from reported errors, and enabling non-expert programmers to specify correct alternatives for problematic code segments. To address these issues, we propose leveraging logical abduction to locate imprecision sources and introducing property programming, where programmers rewrite or annotate small, complex sections of code. These approaches aim to bridge the gap between advanced verification techniques and practical adoption in real-world programming environments.