Formal Verification of Programs in Molecular Models with Random Access Memory

Abstract

Formal verification of molecular programs is a first step towards their automatic processing by means of reasoning systems (ACL2, PVS, etc). In this paper a systematic method to establish verifications of these programs within molecular models with memory, that is, molecular computing models where some operations modifying the inner structure of molecules exist, is proposed. The method presented in this work is applied to relevant problems for the design of molecular programs solving some well-known numerical NP-complete problems: the Generating Cover Families problem, the Set Covering problem and the Minimal Set Cover Selection Problem.