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.