See presentationsWe will show how Horn constraints can be used to describe verification and synthesis problems, and how such constraints can be solved efficiently. In particular we will demonstrate how cardinality operators help to reason about quantitative properties and carry out counting-based correctness arguments, which are useful for the verification of information flow properties and parametrized systems.
