Safety-critical software systems can only support a limited number of failures. Extensive testing is good at catching errors, however that will never certify their absence. Formal verification is an alternative to testing that can (automatically) provide a mathematical proof of correctness of programs. In this thesis, we present a verification procedure for imperative programs. Our procedure reduces imperative programming to functional programming and uses a semi-decision procedure that can reason modulo recursive functions. As a complementary method, we propose an algorithm to generate test cases that attain a high coverage of the program statements or can force the execution of some very refined control paths. We have implemented these algorithms and have integrated them in the Leon verification system. Leon can be used to verify programs written in a proper subset of Scala.