Repositorio de producción científica de la Universidad de Sevilla

Specification of Adleman’s Restricted Model Using an Automated Reasoning System: Verification of Lipton’s Experiment

 

Advanced Search
 
Opened Access Specification of Adleman’s Restricted Model Using an Automated Reasoning System: Verification of Lipton’s Experiment
Cites

Show item statistics
Icon
Export to
Author: Graciani Díaz, Carmen
Martín Mateos, Francisco Jesús
Pérez Jiménez, Mario de Jesús
Department: Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial
Date: 2002
Published in: Unconventional Models of Computation Volume 2509 of the series Lecture Notes in Computer Science pp 126-136
ISBN/ISSN: 978-3-540-44311-7
0302-9743
Document type: Chapter of Book
Abstract: The aim ofthis paper is to develop an executable prototype ofan unconventional model ofcomputation. 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 ofthis molecular program. This work is intended to give an approach to the opportunities offered by mechanized analysis ofuncon ventional model ofcomputation in general. This approach opens up new possibilities ofv erifying molecular experiments before implementing them in a laboratory.
Size: 206.0Kb
Format: PDF

URI: http://hdl.handle.net/11441/44991

DOI: 10.1007/3-540-45833-6_11

See editor´s version

This work is under a Creative Commons License: 
Attribution-NonCommercial-NoDerivatives 4.0 Internacional

This item appears in the following Collection(s)