<?xml version="1.0" encoding="UTF-8"?><xml><records><record><source-app name="Biblio" version="6.x">Drupal-Biblio</source-app><ref-type>13</ref-type><contributors><authors><author><style face="normal" font="default" size="100%">Carmen Graciani-Díaz</style></author><author><style face="normal" font="default" size="100%">Mario J. Pérez-Jiménez</style></author></authors><secondary-authors><author><style face="normal" font="default" size="100%">Mario J. Pérez-Jiménez</style></author><author><style face="normal" font="default" size="100%">Álvaro Romero-Jiménez</style></author><author><style face="normal" font="default" size="100%">Fernando Sancho-Caparrini</style></author></secondary-authors></contributors><titles><title><style face="normal" font="default" size="100%">Automated reasoning systems and molecular computing</style></title><secondary-title><style face="normal" font="default" size="100%">Recent Results in Natural Computing</style></secondary-title></titles><dates><year><style  face="normal" font="default" size="100%">2005</style></year></dates><urls><web-urls><url><style face="normal" font="default" size="100%">http://www.cs.us.es/~marper/investigacion/carmen-rsme.pdf</style></url></web-urls><related-urls><url><style face="normal" font="default" size="100%">http://cantor.cs.us.es/files/carmen-rsme.pdf</style></url></related-urls></urls><publisher><style face="normal" font="default" size="100%">Fénix Editora</style></publisher><pub-location><style face="normal" font="default" size="100%">Sevilla, Spain</style></pub-location><abstract><style face="normal" font="default" size="100%">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.</style></abstract></record></records></xml>