<?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></contributors><titles><title><style face="normal" font="default" size="100%">Using automated reasoning systems on molecular computing</style></title><secondary-title><style face="normal" font="default" size="100%">Lecture Notes in Computer Science</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.springerlink.com/content/hbgc18tyv7nap649/?p=421537edb83041aa94fcae99f6225d79&pi=10</style></url></web-urls></urls><publisher><style face="normal" font="default" size="100%">Springer</style></publisher><pub-location><style face="normal" font="default" size="100%">Amsterdam, The Netherlands</style></pub-location><volume><style face="normal" font="default" size="100%">3384</style></volume><pages><style face="normal" font="default" size="100%">128-137</style></pages><isbn><style face="normal" font="default" size="100%">978-3-540-26174-2</style></isbn><abstract><style face="normal" font="default" size="100%">This paper is focused on the interplay between automated reasoning systems (as theoretical and formal devices to study the correctness of a program) and DNA computing (as practical devices to handle DNA strands to solve classical hard problems with laboratory techniques). To illustrate this work we have proven in the PVS proof checker, the correctness of a program, in a sticker based model for DNA computation, solving the pairwise disjoint families problem. Also we introduce the formalization of the Floyd–Hoare logic for imperative programs.
</style></abstract></record></records></xml>