{"id":165117,"date":"2013-09-01T00:00:00","date_gmt":"2013-09-01T00:00:00","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/msr-research-item\/modular-verification-of-dna-strand-displacement-networks-via-serializability-analysis\/"},"modified":"2018-10-16T20:13:11","modified_gmt":"2018-10-17T03:13:11","slug":"modular-verification-of-dna-strand-displacement-networks-via-serializability-analysis","status":"publish","type":"msr-research-item","link":"https:\/\/www.microsoft.com\/en-us\/research\/publication\/modular-verification-of-dna-strand-displacement-networks-via-serializability-analysis\/","title":{"rendered":"Modular verification of DNA strand displacement networks via serializability analysis"},"content":{"rendered":"<div class=\"asset-content\">\n<p>DNA strand displacement gates can be used to emulate arbitrary chemical reactions, and a number of different schemes have been proposed to achieve this. Here we develop modular correctness proofs for strand displacement emulations 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 encodings, and we infer this global property from the properties of the gates that emulate the individual chemical reactions. This allows correctness to be inferred 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.<\/p>\n<\/div>\n<p><!-- .asset-content --><\/p>\n","protected":false},"excerpt":{"rendered":"<p>DNA strand displacement gates can be used to emulate arbitrary chemical reactions, and a number of different schemes have been proposed to achieve this. Here we develop modular correctness proofs for strand displacement emulations of chemical reaction networks and show how they may be applied to two-domain strand displacement systems. Our notion of correctness is [&hellip;]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","msr-author-ordering":null,"msr_publishername":"Springer","msr_publisher_other":"","msr_booktitle":"","msr_chapter":"","msr_edition":"International Conference on DNA Computing and Molecular Programming","msr_editors":"","msr_how_published":"","msr_isbn":"","msr_issue":"","msr_journal":"International Conference on DNA Computing and Molecular Programming","msr_number":"","msr_organization":"","msr_pages_string":"133-146","msr_page_range_start":"133","msr_page_range_end":"146","msr_series":"","msr_volume":"8141","msr_copyright":"","msr_conference_name":"","msr_doi":"","msr_arxiv_id":"","msr_s2_paper_id":"","msr_mag_id":"","msr_pubmed_id":"","msr_other_authors":"Darko Stefanovic","msr_other_contributors":"","msr_speaker":"","msr_award":"","msr_affiliation":"","msr_institution":"","msr_host":"","msr_version":"","msr_duration":"","msr_original_fields_of_study":"","msr_release_tracker_id":"","msr_s2_match_type":"","msr_citation_count_updated":"","msr_published_date":"2013-09-01","msr_highlight_text":"","msr_notes":"","msr_longbiography":"","msr_publicationurl":"http:\/\/dx.doi.org\/10.1007\/978-3-319-01928-4_10","msr_external_url":"","msr_secondary_video_url":"","msr_conference_url":"","msr_journal_url":"","msr_s2_pdf_url":"","msr_year":2013,"msr_citation_count":0,"msr_influential_citations":0,"msr_reference_count":0,"msr_s2_match_confidence":0,"msr_microsoftintellectualproperty":true,"msr_s2_open_access":false,"msr_s2_author_ids":[],"msr_pub_ids":[],"msr_hide_image_in_river":0,"footnotes":""},"msr-research-highlight":[],"research-area":[13546],"msr-publication-type":[193715],"msr-publisher":[],"msr-focus-area":[],"msr-locale":[268875],"msr-post-option":[],"msr-field-of-study":[],"msr-conference":[],"msr-journal":[],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-165117","msr-research-item","type-msr-research-item","status-publish","hentry","msr-research-area-computational-sciences-mathematics","msr-locale-en_us"],"msr_publishername":"Springer","msr_edition":"International Conference on DNA Computing and Molecular Programming","msr_affiliation":"","msr_published_date":"2013-09-01","msr_host":"","msr_duration":"","msr_version":"","msr_speaker":"","msr_other_contributors":"","msr_booktitle":"","msr_pages_string":"133-146","msr_chapter":"","msr_isbn":"","msr_journal":"International Conference on DNA Computing and Molecular Programming","msr_volume":"8141","msr_number":"","msr_editors":"","msr_series":"","msr_issue":"","msr_organization":"","msr_how_published":"","msr_notes":"","msr_highlight_text":"","msr_release_tracker_id":"","msr_original_fields_of_study":"","msr_download_urls":"","msr_external_url":"","msr_secondary_video_url":"","msr_longbiography":"","msr_microsoftintellectualproperty":1,"msr_main_download":"205256","msr_publicationurl":"http:\/\/dx.doi.org\/10.1007\/978-3-319-01928-4_10","msr_doi":"","msr_publication_uploader":[{"type":"file","title":"DNA19.pdf","viewUrl":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/DNA19.pdf","id":205256,"label_id":0},{"type":"file","title":"DNA19%20-%20appendices.pdf","viewUrl":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/DNA1920-20appendices.pdf","id":205257,"label_id":0},{"type":"url","title":"http:\/\/dx.doi.org\/10.1007\/978-3-319-01928-4_10","viewUrl":false,"id":false,"label_id":0}],"msr_related_uploader":"","msr_citation_count":0,"msr_citation_count_updated":"","msr_s2_paper_id":"","msr_influential_citations":0,"msr_reference_count":0,"msr_arxiv_id":"","msr_s2_author_ids":[],"msr_s2_open_access":false,"msr_s2_pdf_url":null,"msr_attachments":[{"id":0,"url":"http:\/\/dx.doi.org\/10.1007\/978-3-319-01928-4_10"},{"id":205257,"url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/DNA1920-20appendices.pdf"},{"id":205256,"url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/DNA19.pdf"}],"msr-author-ordering":[{"type":"text","value":"Matthew R. Lakin","user_id":0,"rest_url":false},{"type":"user_nicename","value":"aphillip","user_id":31075,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=aphillip"},{"type":"text","value":"Darko Stefanovic","user_id":0,"rest_url":false}],"msr_impact_theme":[],"msr_research_lab":[],"msr_event":[],"msr_group":[],"msr_project":[544545,170217],"publication":[],"video":[],"msr-tool":[],"msr_publication_type":"article","related_content":{"projects":[{"ID":544545,"post_title":"Station B","post_name":"stationb","post_type":"msr-project","post_date":"2019-03-11 15:56:07","post_modified":"2021-09-28 09:10:36","post_status":"publish","permalink":"https:\/\/www.microsoft.com\/en-us\/research\/project\/stationb\/","post_excerpt":"Our work on the Station B project has now been retired. We continue to actively explore the exciting intersection of computing and life sciences, with other projects located on\u00a0www.microsoft.com\/research. Building a platform for programming biology The ability to program biology could enable fundamental breakthroughs across a broad range of industries, including medicine, agriculture, food, construction, textiles, materials and chemicals. It could also help lay the foundation for a future bioeconomy based on sustainable technology. Despite&hellip;","_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/544545"}]}},{"ID":170217,"post_title":"Programming DNA Circuits","post_name":"programming-dna-circuits","post_type":"msr-project","post_date":"2009-02-07 13:36:42","post_modified":"2020-03-06 10:49:40","post_status":"publish","permalink":"https:\/\/www.microsoft.com\/en-us\/research\/project\/programming-dna-circuits\/","post_excerpt":"Molecular devices made of nucleic acids show great potential for applications ranging from bio-sensing to intelligent nanomedicine. They allow computation to be performed at the molecular scale, while also interfacing directly with the molecular components of living systems. They form structures that are stable inside cells, and their interactions can be precisely controlled by modifying their nucleotide sequences. However, designing correct and robust nucleic acid devices is a major challenge, due to high system complexity&hellip;","_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170217"}]}}]},"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/165117","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-research-item"}],"version-history":[{"count":1,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/165117\/revisions"}],"predecessor-version":[{"id":524629,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/165117\/revisions\/524629"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=165117"}],"wp:term":[{"taxonomy":"msr-research-highlight","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-highlight?post=165117"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=165117"},{"taxonomy":"msr-publication-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publication-type?post=165117"},{"taxonomy":"msr-publisher","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publisher?post=165117"},{"taxonomy":"msr-focus-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-focus-area?post=165117"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=165117"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=165117"},{"taxonomy":"msr-field-of-study","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-field-of-study?post=165117"},{"taxonomy":"msr-conference","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-conference?post=165117"},{"taxonomy":"msr-journal","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-journal?post=165117"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=165117"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=165117"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}