The process of automatically constructing an executable program that provably satisfies a Specification.