Parameter verification and synthesis problems for stochastic systems are still hard challenges. The tasks become even more prohibitive when the systems are large-scale and the verification/synthesis are respect the satisfaction of some linear temporal logic formulae. In this paper, we review a number of techniques that we designed to tackle such problems.