Comprehensive Reachability Refutation and Witnesses Generation via Language and Tooling Co-Design

This paper presents a core programming language calculus, BosqeIR, that is uniquely suited for automated reasoning. The co-design of the language and associated strategy for encoding the program semantics into first order logic enables the translation of BosqeIR programs, including the use of collections and dynamic data structures, into decidable fragments of logic that are efficiently dischargeable using modern SMT solvers. This encoding is semantically precise and logically complete for the majority of the language and, even in the cases where completeness is not possible, we use heuristics to precisely encode common idiomatic uses. Using this encoding we construct a program checker BSQChk that is focused on the pragmatic task of providing actionable results to a developer for possible program errors. Depending on the program and the error at hand this could be a full proof of infeasibility, generating a witness input that triggers the error, or a report that, in a simplified partial model of the program, the error could not be triggered.