This work was intended as an attempt to show the possible advantages provided by bringing together two areas, automated reasoning systems and DNA computing. The former as theoretical and formal devices to study the correctness of a program. The latter as practical devices to handle DNA strands to solve classical hard problems using laboratory techniques. To illustrate this approximation we present how we have obtained in the PVS proof checker the correctness of a program in a sticker based model for DNA computation. This result required a previous work: the formalization of the elected model within the PVS language. Also, in order to deal with imperative programs, we have studied a formalization of the Floyd-Hoare logic in the same system, PVS.