Validity checking for finite automata over linear arithmetic constraints

Decision procedures underlie many program analysis problems. Traditional program analysis algorithms attempt to prove some property about a single, statically-defined program by generating a single constraint. Accordingly, traditional decision procedures take single constraints as input. Extending these traditional program analysis algorithms to reason about potentially infinite languages of programs (as generated by a given metaprogram) requires a new class of decision procedures that reason about languages of constraints. This paper introduces the parameterized class of validity checking problems that take as input a language generator $\mathcal{A}$. The parameters are: (1) the language formalism for $\mathcal{A}$, (2) the theory under which each string in the language of $\mathcal{A}$ is interpretted, and (3) the quantification (existential/universal) of the constraints in the language to which the validity property applies. We introduce such decision problems by presenting an algorithm that decides whether a given finite state automaton $\mathcal{A}$ generates any valid linear arithmetic constraints.