Horn constraints and quantifiers for verification and synthesis

Andrey Rybalchenko

We consider Horn constraints with recursion, well-roundedness, quantification, and background theories, and show how such constraints provide a platform for reasoning about verification and synthesis questions about software.