# What's Decidable About Program Verification Modulo Axioms?

arXiv: https://arxiv.org/abs/1910.10889 · HTML: https://mlsanity.com/paper/1910.10889/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 24 Oct 2019.

## Built on by (most cited first, 1 of 1)

- [AutoReSpec: A Framework for Generating Specification using Large Language Models](https://mlsanity.com/paper/2604.03758/) (2026)

## Abstract (arXiv)

We consider the decidability of the verification problem of programs modulo axioms --- that is, verifying whether programs satisfy their assertions, when the functions and relations it uses are assumed to interpreted by arbitrary functions and relations that satisfy a set of first-order axioms. Unfortunately, verification of entirely uninterpreted programs (with the empty set of axioms) is already undecidable. A recent work introduced a subclass of coherent uninterpreted programs, and showed that they admit decidable verification citecoherence2019. We undertake a systematic study of various natural axioms for relations and functions, and study the decidability of the coherent verification problem. Axioms include relations being reflexive, symmetric, transitive, or total order relations, %and their combinations, functions restricted to being associative, idempotent or commutative, and combinations of such axioms as well. Our comprehensive results unearth a rich landscape that shows that though several axiom classes admit decidability for coherent programs, coherence is not a panacea as several others continue to be undecidable.