Given a Boolean relational specification G(X, Y), where X and Y are vectors of inputs and outputs respectively, we consider the problem of synthesizing functions F(X) for Y, such that Exists Y. G(X, Y) is semantically equivalent to G(X, F(X)). Such functions are also called Skolem functions for Y in G(X, Y). We focus on the case where G is given as a DAG (Boolean circuit, AIG, ROBDD, etc.), and present a compositional approach that exploits the structure of the DAG to partially solve the problem from (partial) solutions of sub-problems. The compositional step is computationally efficient, can be generalized to arbitrary Boolean operators, and always gives a function F'(X) that is either a Skolem function or an over-approximation of one. While the over-approximation can be refined by SAT-based counterexample guided abstraction refinement (CEGAR) at each step, we argue why it is beneficial to delay the application of CEGAR. We show the effectiveness of the lazy CEGAR approach by experiments on a suite of benchmarks. This talk is based on joint work with S. Akshay. Shetal Shah and Ajith John, and builds on our TACAS 2017 paper.
Supratik Chakraborty is Bajaj Group Chair Professor in Computer Science and Engineering at IIT Bombay. He received his B.Tech. in Computer Science and Engineering from IIT Kharagpur, where he was awarded the President of India Gold Medal. Subsequently, he did his MS and Ph.D. in Electrical Engineering from Stanford University, where he worked on polynomial time approximate algorithms for timing analysis of asynchronous systems. His current research interests include constrained sampling and counting and their applications, Boolean functional synthesis, formal methods for software, hardware and biological systems, and algorithmic issues in automata theory and logic. He also leads the Centre for Formal Design and Verification of Software at IIT Bombay.