CSE FACULTY SEMINARS – Page 11 – Department of computer science and engineering

Boolean Functional Synthesis: Hardness and Practical Algorithms
Prof. Supratik Chakraborty, CSE, IIT Bombay Short Bio: Supratik Chakraborty is currently Bajaj Group Chair Professor in the Dept of Computer Sc. & Engg at IIT Bombay. He is a Principal Investigator in the Centre for Formal Design and Verification of Software at IIT Bombay. He received his B.Tech. from IIT Kharagpur, and an M.S. and Ph.D. from Stanford University. Subsequently, he spent a year working in industrial research at Fujitsu Laboratories of America before joining IIT Bombay as a faculty member. Supratik’s current research interests include scalable techniques for formal verification, algorithms for constrained sampling and counting, automata theory and logic, and static program analysis. He is particularly interested in bridging the gap between theory and practice of formal methods. He is a Fellow of INAE https://www.cse.iitb.ac.in/~supratik/ Date: May 27, 2020; Thursday Time: 4:00 PM IST	Abstract: Given a Boolean relation between inputs and outputs, Boolean Functional Synthesis seeks to represent the outputs as deterministic functions of the inputs. This problem, also known as Skolem function synthesis, has a wide range of applications, and is one of the key components of reactive controller synthesis techniques. An efficient solution to this problem can be shown to yield an efficient algorithm for prime factorization, thereby cracking RSA. In this talk, we will first present (conditional) lower bounds on the hardness of the problem, thereby showing that it is unlikely that there are time or space efficient algorithms for Boolean Functional Synthesis. We will then present work done in our group on developing algorithms that are practically efficient on a large class of benchmarks. This includes expansion-based algorithms and knowledge-compilation based algorithms. We will also discuss some intuition on why these algorithms work well in practice. Finally, we will discuss experimental results that illustrate the practical effectiveness of the algorithms and conclude by identifying key challenges in the road ahead.

Boolean Functional Synthesis: Hardness and Practical Algorithms

Prof. Supratik Chakraborty, CSE, IIT Bombay

Short Bio:
Supratik Chakraborty is currently Bajaj Group Chair Professor in the Dept of Computer Sc. & Engg at IIT Bombay. He is a Principal Investigator in the Centre for Formal Design and Verification of Software at IIT Bombay. He received his B.Tech. from IIT Kharagpur, and an M.S. and Ph.D. from Stanford University. Subsequently, he spent a year working in industrial research at Fujitsu Laboratories of America before joining IIT Bombay as a faculty member. Supratik’s current research interests include scalable techniques for formal verification, algorithms for constrained sampling and counting, automata theory and logic, and static program analysis. He is particularly interested in bridging the gap between theory and practice of formal methods. He is a Fellow of INAE
https://www.cse.iitb.ac.in/~supratik/

Date: May 27, 2020; Thursday
Time: 4:00 PM IST

Abstract:

Given a Boolean relation between inputs and outputs, Boolean Functional Synthesis seeks to represent the outputs as deterministic functions of the inputs. This problem, also known as Skolem function synthesis, has a wide range of applications, and is one of the key components of reactive controller synthesis techniques. An efficient solution to this problem can be shown to yield an efficient algorithm for prime factorization, thereby cracking RSA. In this talk, we will first present (conditional) lower bounds on the hardness of the problem, thereby showing that it is unlikely that there are time or space efficient algorithms for Boolean Functional Synthesis. We will then present work done in our group on developing algorithms that are practically efficient on a large class of benchmarks. This includes expansion-based algorithms and knowledge-compilation based algorithms. We will also discuss some intuition on why these algorithms work well in practice. Finally, we will discuss experimental results that illustrate the practical effectiveness of the algorithms and conclude by identifying key challenges in the road ahead.

1 2 3 4 5 6 7 8 9 10 11 12 13 14