{"id":164420,"date":"2013-05-01T00:00:00","date_gmt":"2013-05-01T00:00:00","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/msr-research-item\/smt-based-analysis-of-biological-computation\/"},"modified":"2018-10-16T20:18:11","modified_gmt":"2018-10-17T03:18:11","slug":"smt-based-analysis-of-biological-computation","status":"publish","type":"msr-research-item","link":"https:\/\/www.microsoft.com\/en-us\/research\/publication\/smt-based-analysis-of-biological-computation\/","title":{"rendered":"SMT-based Analysis of Biological Computation"},"content":{"rendered":"<div class=\"asset-content\">\n<p>Synthetic biology focuses on the re-engineering of living organisms for useful purposes while DNA computing targets the construction of therapeutics and computational circuits directly from DNA strands. The complexity of biological systems is a major engineering challenge and their modeling relies on a number of diverse formalisms. Moreover, many applications are mission-critical&#8221; (e.g. as recognized by NASA&#8217;s Synthetic Biology Initiative) and require robustness which is difficult to obtain. The ability to formally specify desired behavior and perform automated computational analysis of system models can help address these challenges, but today there are no unifying scalable analysis frameworks capable of dealing with this complexity. In this work, we study pertinent problems and modeling formalisms for DNA computing and synthetic biology and describe how they can be formalized and encoded to allow analysis using Satisfiability Modulo Theories (SMT). This work highlights biological engineering as a domain that can benefit extensively from the application of formal methods. It provides a step towards the use of such methods in computational design frameworks for biology and is part of a more general effort towards the formalization of biology and the study of biological computation.<\/p>\n<\/div>\n<p><!-- .asset-content --><\/p>\n","protected":false},"excerpt":{"rendered":"<p>Synthetic biology focuses on the re-engineering of living organisms for useful purposes while DNA computing targets the construction of therapeutics and computational circuits directly from DNA strands. The complexity of biological systems is a major engineering challenge and their modeling relies on a number of diverse formalisms. Moreover, many applications are mission-critical&#8221; (e.g. as recognized [&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":[{"type":"user_nicename","value":"yordanov","user_id":"35043"},{"type":"user_nicename","value":"cwinter","user_id":"31491"},{"type":"user_nicename","value":"youssefh","user_id":"35047"},{"type":"user_nicename","value":"hkugler","user_id":"32012"}],"msr_publishername":"Springer Verlag","msr_publisher_other":"","msr_booktitle":"","msr_chapter":"","msr_edition":"NASA Formal Methods Symposium 2013","msr_editors":"","msr_how_published":"","msr_isbn":"","msr_issue":"","msr_journal":"","msr_number":"","msr_organization":"","msr_pages_string":"78-92","msr_page_range_start":"78","msr_page_range_end":"92","msr_series":"LNCS","msr_volume":"7871","msr_copyright":"","msr_conference_name":"NASA Formal Methods Symposium 2013","msr_doi":"","msr_arxiv_id":"","msr_s2_paper_id":"","msr_mag_id":"","msr_pubmed_id":"","msr_other_authors":"","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-05-01","msr_highlight_text":"","msr_notes":"","msr_longbiography":"","msr_publicationurl":"","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":[13553],"msr-publication-type":[193716],"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-164420","msr-research-item","type-msr-research-item","status-publish","hentry","msr-research-area-medical-health-genomics","msr-locale-en_us"],"msr_publishername":"Springer Verlag","msr_edition":"NASA Formal Methods Symposium 2013","msr_affiliation":"","msr_published_date":"2013-05-01","msr_host":"","msr_duration":"","msr_version":"","msr_speaker":"","msr_other_contributors":"","msr_booktitle":"","msr_pages_string":"78-92","msr_chapter":"","msr_isbn":"","msr_journal":"","msr_volume":"7871","msr_number":"","msr_editors":"","msr_series":"LNCS","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":"218566","msr_publicationurl":"","msr_doi":"","msr_publication_uploader":[{"type":"file","title":"NFM2013.pdf","viewUrl":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2013\/05\/NFM2013.pdf","id":218566,"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":218566,"url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2013\/05\/NFM2013.pdf"}],"msr-author-ordering":[{"type":"user_nicename","value":"yordanov","user_id":35043,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=yordanov"},{"type":"user_nicename","value":"cwinter","user_id":31491,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=cwinter"},{"type":"user_nicename","value":"youssefh","user_id":35047,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=youssefh"},{"type":"user_nicename","value":"hkugler","user_id":32012,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=hkugler"}],"msr_impact_theme":[],"msr_research_lab":[],"msr_event":[],"msr_group":[],"msr_project":[544545,170870],"publication":[],"video":[],"msr-tool":[],"msr_publication_type":"inproceedings","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":170870,"post_title":"Z3-4Biology","post_name":"z3-4biology","post_type":"msr-project","post_date":"2011-11-17 09:18:31","post_modified":"2019-01-10 09:05:12","post_status":"publish","permalink":"https:\/\/www.microsoft.com\/en-us\/research\/project\/z3-4biology\/","post_excerpt":"An SMT-based Framework for Analyzing Biological Computation The basic principles governing the development and function of living organisms remain only partially understood, despite significant progress in molecular and cellular biology and tremendous breakthroughs in experimental methods. The development of system-level, mechanistic, computational models has the potential to become a foundation for improving our understanding of natural biological systems, and for designing engineered biological systems with wide-ranging applications in nanomedicine, nanomaterials and computing. We developed Z34Bio&hellip;","_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170870"}]}}]},"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/164420","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\/164420\/revisions"}],"predecessor-version":[{"id":526140,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/164420\/revisions\/526140"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=164420"}],"wp:term":[{"taxonomy":"msr-research-highlight","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-highlight?post=164420"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=164420"},{"taxonomy":"msr-publication-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publication-type?post=164420"},{"taxonomy":"msr-publisher","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publisher?post=164420"},{"taxonomy":"msr-focus-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-focus-area?post=164420"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=164420"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=164420"},{"taxonomy":"msr-field-of-study","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-field-of-study?post=164420"},{"taxonomy":"msr-conference","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-conference?post=164420"},{"taxonomy":"msr-journal","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-journal?post=164420"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=164420"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=164420"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}