Program Synthesis is the automated construction of a program that satisfies a given specification, often expressed in the form of input-output examples or formal logic. It leverages techniques from formal methods, machine learning, and artificial intelligence to generate code that can solve specific problems or automate tasks with minimal human intervention.