SeminarsView 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: https://meet.google.com/fee-usjd-oxj
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: https://meet.google.com/fee-usjd-oxj
Host Faculty: Prof. Deepak DSouza