View all Seminars  |  Download ICal for this event

Specification Synthesis with Constrained Horn Clauses

Series: Department Seminar

Speaker: Ms.Sumanth Prabhu Ph.D student Department of Computer Science and Automation, IISc, and TCS Research

Date/Time: Jun 21 16:00:00

Location: Google Meet joining info: Video call link:

Faculty Advisor: Prof. Deepak DSouza

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. In this paper, we propose 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, our technique discovers not only specifications but also inductive invariants. Our iterative algorithm lazily generalizes non-vacuous specifications in a counterexample-guided loop. The key component of our technique is an effective non-vacuous specification synthesis algorithm. We have implemented the approach in a tool called HornSpec, taking as input systems of constrained Horn clauses. We have experimentally demonstrated the tools effectiveness, efficiency, and the quality of generated specifications, on a range of benchmarks.
This is joint work with Grigory Fedyukovich, Kumar Madhukar, and Deepak DSouza. The paper will be presented at the upcoming PLDI 2021 conference.
Google Meet joining info:
Video call link:

Speaker Bio:

Host Faculty: Prof. Deepak DSouza