This thesis is about the development and usage of deductive methods in two main areas: (i) the deductive dis-verification of programs, i.e., how techniques for deductive verification of programs can be used to detect ...