Re: [pl-seminar] CAV Practice Talk

[Qinheping HU <qhu28@xxxxxxxx>]

It should be in 2310

Sorry for the mistake

---

From: Pl-seminar <pl-seminar-bounces@xxxxxxxxxxx> on behalf of Loris D'Antoni <loris@xxxxxxxxxxx>
Sent: Monday, June 25, 2018 11:51:24 AM
To: pl-seminar@xxxxxxxxxxx
Subject: Re: [pl-seminar] CAV Practice Talk

 

Reminder that talk starts in 10 minutes in 4310

On Sat, Jun 23, 2018 at 12:43 AM Loris D'Antoni <loris@xxxxxxxxxxx> wrote:

Add to the cs calendar as well

On Sat, Jun 23, 2018 at 12:13 AM Qinheping HU <qhu28@xxxxxxxx> wrote:

Hi everyone,

I will be giving a practice talk for CAV this Monday at noon in 4310. If you are able to attend, I would very much value your feedback.

Title: Syntax-Guided Synthesis with Quantitative Syntactic Objectives

Abstract:  Automatic program synthesis promises to increase the productivity of programmers and end-users of computing devices by automating tedious and error-prone tasks. Despite the practical successes of program synthesis, we still do not have systematic frameworks to synthesize programs that are “good” according to certain metrics—e.g., produce programs of reasonable sizes or with good runtime—and to understand when synthesis can result in such good programs. In this paper, we propose QSyGuS, a unifying framework for describing syntax-guided synthesis problems with quantitative objectives over the syntax of the synthesized programs. QSyGuS builds on weighted (tree) grammars, a clean and foundational formalism that provides flexible support for different quantitative objectives, useful closure properties, and practical decision procedures. We then present an algorithm for solving QSyGuS. Our algorithm leverages closure properties of weighted grammars to generate intermediate problems that can be solved using non-quantitative SyGuS solvers. Finally, we implement our algorithm in a tool, QuaSi, and evaluate it on 26 quantitative extensions of existing SyGuS benchmarks. QuaSi can synthesize optimal solutions in 15/26 benchmarks with times comparable to those needed to find an arbitrary solution.

Paper: http://pages.cs.wisc.edu/~qhu28/papers/QSyGuS.pdf

Best,

Qinheping Hu

_______________________________________________
Pl-seminar mailing list
Pl-seminar@xxxxxxxxxxx
https://lists.cs.wisc.edu/mailman/listinfo/pl-seminar