Invited Talk: Specification Synthesis with Constrained Horn Clauses

The problem of synthesizing specifications of undefined procedures has a broad range of applications.However, the usefulness of the generated specifications depends on their quality.In this talk, I will present our work on finding correct and maximal specifications using an approach called infer-check-weaken.This approach first infers a correct specification through a logical synthesis technique.A maximality check follows to determine whether the specification is the weakest.If not, the specification is weakened.We observe that our approach is effective across a range of benchmarks, including those with arrays.