IARCS Verification Seminar Series





Title: Boolean functional synthesis: A view from theory and practice

Speaker: S. Akshay    (bio) (bio)


S. Akshay is a faculty member in the Department of Computer Science and Engineering at IIT Bombay. His research interests span formal methods and AI with a focus on automata theory, quantitative (timed/probabilistic) verification and automated synthesis. He has given multiple recent tutorials on automated functional synthesis in venues including Highlights 2022, AAAI 2022 and IJCAI 2022.


When: Tuesday, 02 August 2022 at 1900 hrs (IST)   Video  

Abstract:
It is often easy to write down the specification of a system as a relation between inputs and outputs. But implementing it requires us to take a functional view, i.e., to have functions that produce outputs from inputs. The question we ask is if we can automatically synthesize such a function from the given relation? In this talk, we focus on this question in the Boolean setting.

We start by showing the centrality of this problem via a variety of examples and applications. We then look at theoretical hardness results and survey some algorithmic techniques that have been developed in recent years to tackle this problem. This leads us to examine the structure of specification in more depth and doing so we develop a theory of knowledge representations for efficient synthesis. We end with several open questions and avenues for future work.