Formal methods is an umbrella term for rigorous techniques for specifying and verifying computer systems, or building such systems with mathematical guarantees on their correctness, or on the absence of bugs of a given kind. Model checking is a set of techniques that can formally prove properties of a given model; while controller synthesis consists, using similar techniques, in completing the decription of an open system to ensure a given property by construction. One of the targets of formal methods is systems with quantitative aspects such as real-time constraints and probabilities. In this thesis I summarize my contributions on algorithms for model checking and controller synthesis on timed and probabilistic systems, focusing on timed automaton and Markov decision process formalisms.