2025-05-142025-05-142005Graciani Díaz, C. y Pérez Jiménez, M.d.J. (2005). Automated reasoning systems and molecular computing. En Recent results in natural computing (pp. 47-78). Fénix Editora.84-609-6864-2https://hdl.handle.net/11441/172726This work was intended to show the possible advantges 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 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 tthe 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 PSV language. Also, in order to deal with imperative programs, we have studied a formalization of the Floyd-Hoare logic in the same system, PVS.application/pdfRecent results in natural computingengAttribution-NonCommercial-NoDerivatives 4.0 Internationalhttp://creativecommons.org/licenses/by-nc-nd/4.0/info:eu-repo/semantics/bookPartinfo:eu-repo/semantics/openAccess