Efficient and Effective Software Verifications for Scientific Applications using Static Analyses and Code Instrumentation