Exploring synergies between program synthesis and machine learning

Program synthesis is a term that describes a family of techniques that enables automatic generation of code according to user-provided specifications. Search-based program synthesis offers numerous benefits in developing reliable and performant software and has successfully been deployed in several domains. However, searching through intractable program spaces remains a daunting challenge, precluding the widespread adoption of this technique. Machine learning has had remarkable success in accomplishing incredibly challenging tasks, especially in computer vision and language translation. This thesis introduces two learning-guided techniques which make the program synthesis search more efficient in navigating the program space. In the domain of superoptimization - a solver-aided search-based code optimization technique, we develop machine learning models which direct the enumerative search towards program spaces where an optimal solution is likely to exist. By integrating our models with a modern superoptimizer, we can make the search more efficient by reducing enumeration overheads. Deep learning compilers also incorporate a search-based approach to map computations onto the target hardware. These mappings, also called schedules, specify how the underlying loop-nests corresponding to each layer is mapped on the hardware. The search must navigate through an intractable space of schedules to determine an efficient mapping for a given deep-learning model. We develop a graph convolutional network-based analytical cost model which enables the schedule search to determine the performance of a candidate schedule without depending on slow and expensive executions on hardware. Incorporating a graph-based representation enables us to surpass the accuracy of existing cost models used in state-of-art compilers. In addition to learning-guided techniques, we also explore parallel execution to address the problem of state-space explosion. We study this in the context of symbolic execution, a search-based software testing technique. In this setting, multiple executors can work on non-overlapping regions of a program, thus covering more program space and finding bugs faster when compared to a single instance. While machine learning can help alleviate challenges encountered in program synthesis, we can also utilize program synthesis to construct machine learning models which provide certain correctness guarantees. We propose a novel approach to synthesizing binary classifiers, built using neural networks, from user-provided specifications. By adopting a synthesis-based approach instead of traditional learning using datasets, we can create networks that are correct-by-construction. The results show that our technique can create networks that are difficult to train using data.Electrical and Computer Engineerin