Logic, automata and decidability
Which questions about programs can an algorithm answer? Many fundamental verification and synthesis problems are undecidable in general. The challenge is to find meaningful restrictions under which automated reasoning becomes possible, without losing the behaviors we need to understand.
We use logic and automata to map this boundary. We identify decidable classes of programs and logical theories, develop decision procedures, and establish their computational complexity. These results explain both the limits of automated reasoning and the structure that makes new verification and synthesis algorithms possible.