FUNCTIONAL SYNTHESIS VIA FORMAL METHODS AND MACHINE LEARNING

Abstract

Functional synthesis, a fundamental task in computer science, involves automatically generating functions that meet specific user requirements. Its practical applications span a wide range, from automatically repairing programs to cryptanalysis. While theoretical investigations have shown that certain instances of functional synthesis can be exceptionally time-consuming, the need for practical usability has spurred the development of algorithms that showcase remarkable scalability. Despite these significant strides, practical challenges persist, and there are still real-world situations where current methods encounter limitations.

In this thesis, we explore functional synthesis using machine learning and formal methods. Our novel approach, Manthan, treats it as a classification problem. Manthan uses innovative data generation and formal methods to guide repair and verification, surpassing previous methods by handling 40% more instances.

Manthan's scalability opens doors to broader applications. We propose reducing program synthesis to functional synthesis, making Manthan a powerful tool for synthesizing programs based on bit-vector theory. Recognizing the need for adaptability, we introduce a synthesis framework that ensures compliance with strict constraints and strives to meet predefined goodness measures for soft constraints.