In this talk I will briefly explain how refinement types can are used for program verification. Refinement types use the modularity of types to reduce program verification into SMT decidable queries. The talk relies on a PLMW@ICFP 30 minutes presentation, so there will be plenty of time for Q&A.