FSU Computer Science Assistant Professor, Dr. Grigory Fedyukovich, has received the distinguished paper award at 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI ’21) for the paper “Specification Synthesis with Constrained Horn Clauses” (co-authored with researchers from TCS Research and IIS India).
The problem of synthesizing specifications of undefined procedures has a broad range of applications, but the usefulness of the generated specifications depends on their quality. The paper contributes a technique for finding maximal and non-vacuous specifications. Maximality allows for more choices for implementations of undefined procedures, and non-vacuity ensures that safety assertions are reachable. To handle programs with complex control flow, the technique discovers not only specifications but also inductive invariants. The iterative algorithm lazily generalizes non-vacuous specifications in a counterexample-guided loop, where the key component is an effective non-vacuous specification synthesis algorithm. The approach has been implementedÃin a tool called HornSpec, taking as input systems of constrained Horn clauses and experimentally evaluated on a range of public benchmarks.