Modular verification of DNA strand displacement networks via serializability analysis

Abstract. DNA strand displacement gates can be used to emulate arbi-trary chemical reactions, and a number of different schemes have been proposed to achieve this. Here we developmodular correctness proofs for strand displacement encodings of chemical reaction networks and show how they may be applied to two-domain strand displacement systems. Our notion of correctness is serializability of interleaved reaction encod-ings, andwe infer this global property from the properties of the gates that encode the individual chemical reactions. This allows correctness to be in-ferred for arbitrary systems constructed using these components, and we illustrate this by applying our results to a two-domain implementation of a well-known approximate majority voting system.