Abstract: Current state of the art technology has fostered the pervasive use of microprocessors in our every day life. Examples include portable accessories such as mobile phones and PDA's; home appliances such as refrigerators, toasters and coffee machines; medical equipment such as defibrillators, dialysis machines and MRI's among many other systems. These embedded computing devices interact with the continuous environment in nontrivial ways that difficult its analysis and synthesis. In this talk I will focus on the problem of synthesizing embedded controllers that are provably correct by design. This approach contrasts with current techniques where verification plays an important role in ensuring correctness of a system. I will show how it is possible to automatically design controllers from temporal logic specifications for purely continuous systems and how these results can be extended to embedded systems. One novelty of the current approach is the fact that we synthesize both continuous control laws as well as the mode switching software from specifications.