Synthesis United: Boolean Functional Synthesis: Some Recent Advances

Add to your list(s) Download to your calendar using vCal

• Supratik Chakraborty (Indian Institute of Technology)
• Monday 18 July 2022, 13:00-13:45
• Seminar Room 2, Newton Institute.

If you have a question about this talk, please contact nobody.

VSO2 - Verified software

Suppose we want to design a system with inputs X and outputs Y, such that the relation between X and Y is specified as a Boolean formula \varphi(X, Y).  The problem of synthesizing Y as a function of X, say F(X),  s.t. that \varphi(X, F(X)) holds for all X is the classical synthesis problem.  We augment this problem definition to include cases where the specification is  ”unrealizable” in the classical sense, i.e. there exist some values of X for which no value of Y satisfies the spec.  Specificially, we ask if we can synthesize Y as a function F(X) such that \varphi(X, F(X)) holds for all values of X for which \exists Y \varphi(X, Y) holds.  It turns out thatthere are many interesting applications where this notion of synthesis is useful.  We present an overview of two different approaches that have been recently proposed to solve the above problem—one based on an iterative repair algorithm, and the other based on knowlege compilation. We present results obtained from each of these approaches and outline some future directions of research. 

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 2, Newton Institute
• bld31

Note that ex-directory lists are not shown.