Seminars

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: https://meet.google.com/fee-usjd-oxj

Faculty Advisor: Prof. Deepak DSouza

Abstract:
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.
<br>
This is joint work with Grigory Fedyukovich, Kumar Madhukar, and
Deepak DSouza. The paper will be presented at the upcoming PLDI 2021
conference.
<br>
Google Meet joining info:<br>
Video call link: <a href="Link

Host Faculty: Prof. Deepak DSouza