Re: [pl-seminar] CAV practice talk reschedule

[Qinheping HU <qhu28@xxxxxxxx>]

Hi Everyone,

I am also going to give a practice talk tomorrow. My talk will be after Sam's talk, same room.

Proving Unrealizability for Syntax-Guided Synthesis

Abstract: We consider the problem of automatically establishing that a given syntax-guided-synthesis (SyGuS) problem is unrealizable (i.e., has no solution). Existing techniques have quite limited ability to establish unrealizability for general SyGuS instances in which the grammar describing the search space contains infinitely many programs. By encoding the synthesis problem's grammar G as a nondeterministic program P_G, we reduce the unrealizability problem to a reachability problem such that, if a standard program-analysis tool can establish that a certain assertion in P_G always holds, then the synthesis problem is unrealizable. Our method can be used to augment any existing SyGus tool so that it can establish that a successfully synthesized program q is optimal with respect to some syntactic cost -- e.g., q has the fewest possible if-then-else operators. Using known techniques, grammar G can be automatically transformed to generate exactly all programs with lower cost than q -- e.g., fewer conditional expressions. Our algorithm can then be applied to show that the resulting synthesis problem is unrealizable. We implemented the proposed technique in a tool called NOPE. NOPE can prove unrealizability for 59/134 variants of existing linear-integer-arithmetic SyGus benchmarks, whereas all existing SyGus solvers lack the ability to prove that these benchmarks are unrealizable, and time out on them.

---

From: Pl-seminar <pl-seminar-bounces@xxxxxxxxxxx> on behalf of Samuel Drews <pl-seminar-bounces@xxxxxxxxxxx>
Sent: Thursday, July 11, 2019 9:34 AM
To: pl-seminar@xxxxxxxxxxx
Subject: [pl-seminar] CAV practice talk reschedule

 

Hi Everyone,

Sorry for the inconvenience, but this talk will be Friday at 11:00am, still in 3310.

Best,

Samuel Drews

---

From: Pl-seminar <pl-seminar-bounces@xxxxxxxxxxx> on behalf of Samuel Drews <pl-seminar-bounces@xxxxxxxxxxx>
Sent: Wednesday, July 10, 2019 9:47 AM
To: pl-seminar@xxxxxxxxxxx
Subject: [pl-seminar] CAV practice talk tomorrow, 1:30pm rm 3310

 

Hi Everyone,

I hope the POPL deadline is treating you well.  As the subject line says, tomorrow I will be giving a practice talk for CAV at 1:30pm in room 3310; if you're awake/alive and are able to attend, I would appreciate the feedback!

Efficient Synthesis with Probabilistic Constraints.

ABSTRACT. We consider the problem of synthesizing a program given a probabilistic specification of its desired behavior. Specifically, we study the recent paradigm of distribution-guided inductive synthesis (digits), which iteratively calls a synthesizer on finite samplesets from a given distribution. We make theoretical and algorithmic contributions: (1) We prove the surprising result that digits only requires a polynomial number of synthesizer calls in the size of the samepleset, despite its ostensibly exponential behavior. (2) We present a property-directed version of digits that further reduces the number of synthesizer calls, drastically reducing synthesis time on a range of benchmarks.

Best,

Samuel Drews