We'll still have Heping's talk at 1130 as scheduled
Actually I'm just cancelling mine altogether---sorry for the back and forth.
From: Qinheping HU
Sent: Thursday, July 11, 2019 8:25:46 PM
To: pl-seminar@xxxxxxxxxxx; Samuel Drews
Subject: Re: CAV practice talk reschedule
Â
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.
Hi Everyone,
Sorry for the inconvenience, but this talk will be
FridayÂat 11:00am, still in 3310.
Best,
Samuel Drews
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
_______________________________________________
Pl-seminar mailing list
Pl-seminar@xxxxxxxxxxx
https://lists.cs.wisc.edu/mailman/listinfo/pl-seminar
|