The ACM India 2024 Doctoral Dissertation Award goes to Priyanka Golia for her dissertation titled “Functional Synthesis via Formal Methods and Machine Learning.” Priyanka’s dissertation combines ideas from many areas—constraint sampling, machine learning, and formal methods, and based on this, she built a solver, Manthan, for synthesis of Boolean functions. Manthan is available as open-source and is currently the state-of-the-art tool for Boolean functional synthesis. Priyanka’s dissertation work was done at IIT Kanpur under the supervision of Prof. Subhajit Roy, IIT Kanpur and Prof. Kuldeep Meel of University of Toronto.
At its core, Manthan uses a data-driven approach to solve the problem. It works in four stages: (1) data generation, (2) learning an ML model, (3) translating ML model to Boolean functions, and (4) formal verification and repair. While her initial work on Manthan led to strong publications, Priyanka did not stop there. She improved Manthan via many strong algorithmic and engineering innovations: a pre-pass to identify uniquely determined Skolem functions, learning a multi-class decision tree instead of a binary classifier, and using lexicographical MaxSAT. After this, Priyanka further lifted Manthan to learning Boolean functions with explicit dependencies, addressing the well-known problem of learning Henkin functions for DQBF instances. After her stint with developing tools for functional synthesis, Priyanka explored applications for such functions, and the possibility of using similar approaches for real-world problems. Priyanka therefore receives the DDA award for her contributions to functional synthesis, building an open-source tool based on her ideas, and exploring the application of these ideas to real-world applications.