2019/04/25 by Jochen Hoenicke, Hoenicke, Jochen, Tanja Schindler +1
Biochemistry, Genetics and Molecular Biology · Computer Science · #Algorithms and Data Compression #Cellular Automata and Applications #DNA and Biological Computing #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #cs.LO
paper · pdf · doi:10.48550/arxiv.1904.11381
arxiv created 2019/04/25 · openalex publication_date 2019/04/25 · arxiv updated 2019/04/26 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Interpolation based software model checkers have been successfully employed to automatically prove programs correct. Their power comes from interpolating SMT solvers that check the feasibility of potential counterexamples and compute candidate invariants, otherwise. This approach works well for quantifier-free theories, like equality theory or linear arithmetic. For quantified formulas, there are SMT solvers that can decide expressive fragments of quantified formulas, e. g., EPR, the array property fragment, and the finite almost uninterpreted fragment. However, these solvers do not support interpolation. It is already known that in general EPR does not allow for interpolation. In this paper, we show the same result for the array property fragment.