<?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%">Francisco J. Martín-Mateos</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%">Specification of Adleman's Restricted Model Using An Automated Reasoning System: Verification of Lipton's Experiment</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%">2002</style></year><pub-dates><date><style  face="normal" font="default" size="100%">01/2002</style></date></pub-dates></dates><urls><web-urls><url><style face="normal" font="default" size="100%">http://www.springerlink.com/content/hh5q5ruw9x28vdtn/?p=f8f56e08cfcc423f824fb537a05e8c00&pi=10</style></url></web-urls></urls><publisher><style face="normal" font="default" size="100%">Springer Berlin / Heidelberg</style></publisher><volume><style face="normal" font="default" size="100%">2509</style></volume><pages><style face="normal" font="default" size="100%">126-136</style></pages><isbn><style face="normal" font="default" size="100%">0302-9743</style></isbn><abstract><style face="normal" font="default" size="100%">The aim of this paper is to develop an executable prototype of an unconventional model of computation. Using the PVS verification system (an interactive environment for writing formal specifications and checking formal proofs), we formalize the restricted model, based on DNA, due to L. Adleman. Also, we design a formal molecular program in this model that solves SAT following Lipton’s ideas. We prove using PVS the soundness and completeness of this molecular program. This work is intended to give an approach to the opportunities offered by mecha nized analysis of unconventional model of computation in general. This approach opens up new possibilities of verifying molecular experiments before implementing them in a laboratory.</style></abstract></record></records></xml>