Validity Checking for Finite Automata over Linear Arithmetic Constraints

Abstract 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 A. The parameters are: (1) the language formalism for A, (2) the theory under which each string in the language of 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...

• Type: Conference
• Year: 2006
• Where: FSTTCS
• Authors: Gary Wassermann, Zhendong Su
• Keywords: Decision Procedures, FSTTCS 2006, Program Analysis, Program Analysis Algorithms, Software Engineering