Select Page

PL Perspectives

Perspectives on computing and technology from and for those with an interest in programming languages.
Specification Synthesis with Constrained Horn Clauses

Specification Synthesis with Constrained Horn Clauses

The problem of program verification is to find whether a program meets its specification. But if a program calls functions whose bodies are missing, the verification aims at finding the most general implementations of these functions. In this post we show how advances in automated reasoning allow for doing it efficiently.

Read more...