BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//project/author//NONSGML v1.0//EN
CALSCALE:GREGORIAN
BEGIN:VEVENT
DTEND:20210621T120000Z
UID:0049e76651ac7380c9d8c9d2293dd702-159
DTSTAMP:19700101T120016Z
DESCRIPTION:Specification Synthesis with Constrained Horn Clauses
URL;VALUE=URI:https://www.csa.iisc.ac.in/newweb/event/159/specification-synthesis-with-constrained-horn-clauses/
SUMMARY: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="https://meet.google.com/fee-usjd-oxj">https://meet.google.com/fee-usjd-oxj</a>
DTSTART:20210621T120000Z
END:VEVENT
END:VCALENDAR