University of Cambridge > > Isaac Newton Institute Seminar Series > Synthesis United: Boolean Functional Synthesis: Some Recent Advances

Synthesis United: Boolean Functional Synthesis: Some Recent Advances

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2022, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity