Defunctionalization

Building on the successes of satisfiability modulo theories (SMT), Bjorner et al. initiated a research programme advocating Horn constraints as a suitable basis for automatic program verification. The notion of first-order constrained Horn clauses …