Software synthesis is an attractive field of study that can promise a more safe and productive software development process. However, it is notoriously very difficult and few convincing applications have emerged so far. In this report, we present a series of works that explore different avenues of software synthesis. First we study the application of decision procedures for synthesis and provide an implementation in the Leon system. Then we look at interpolation and its possible application to component-based synthesis. Finally we present a new architecture in Leon with clear separation between synthesis and verification, as well as a new challenging text editor benchmark.