{"id":170870,"date":"2011-11-17T09:18:31","date_gmt":"2011-11-17T09:18:31","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/project\/z3-4biology\/"},"modified":"2019-01-10T09:05:12","modified_gmt":"2019-01-10T17:05:12","slug":"z3-4biology","status":"publish","type":"msr-project","link":"https:\/\/www.microsoft.com\/en-us\/research\/project\/z3-4biology\/","title":{"rendered":"Z3-4Biology"},"content":{"rendered":"<h2 class=\"asset-content\"><!-- .asset-content -->An SMT-based Framework for Analyzing Biological Computation<\/h2>\n<div id=\"en-usprojectsz3-4biologydefault\" class=\"page-content\">\n<p>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 (Z3 for Biology), a unifed SMT-based framework for the automated analysis of natural and engineered biological systems to enable\u00a0addressing important biological questions, and studying complex biological models.<\/p>\n<\/div>\n<div id=\"en-usprojectsz3-4biologydefault\" class=\"page-content\">\n<h3>Updates<\/h3>\n\t\t\t<div class=\"moray-accordion\" data-show=\"false\">\n\t\t\t\t\t\t\t<div class=\"clearfix\">\n\t\t\t\t\t<div\n\t\t\t\t\t\tclass=\"btn-group align-items-center mb-g float-sm-right\"\n\t\t\t\t\t\trole=\"group\"\n\t\t\t\t\t\tdata-mount=\"collapse-controls\"\n\t\t\t\t\t\tdata-bi-aN=\"accordion-collapse-controls\"\n\t\t\t\t\t\tdata-target=\"#accordion-1\">\n\t\t\t\t\t\t<button class=\"btn btn-link m-0\" aria-disabled=\"false\" aria-pressed=\"false\" data-action=\"expand\" type=\"button\" data-bi-cN=\"Expand all\">Expand all<\/button>\n\t\t\t\t\t\t<span aria-hidden=\"true\"> | <\/span>\n\t\t\t\t\t\t<button class=\"btn btn-link m-0\" aria-disabled=\"false\" aria-pressed=\"false\" data-action=\"collapse\" type=\"button\" data-bi-cN=\"Collapse all\">Collapse all<\/button>\n\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t\t\t<ul class=\"accordion\" id=\"accordion-1\">\n\t\t\t\t\t\t\t\t\t\u00a0 \t\t\t\t<li class=\"m-0\">\n\t\t\t<h4 class=\"accordion-header\">\n\t\t\t\t<button\n\t\t\t\t\tclass=\"btn btn-collapse m-0\"\n\t\t\t\t\ttype=\"button\"\n\t\t\t\t\tdata-mount=\"collapse\"\n\t\t\t\t\tdata-target=\"#collapse-2\"\n\t\t\t\t\taria-expanded=\"false\"\n\t\t\t\t\taria-controls=\"collapse-2\">\n\t\t2014\t\t\t\t<\/button>\n\t\t\t<\/h4>\n\t\t\t<div class=\"collapse\" id=\"collapse-2\">\n\t\t\t\t<div class=\"accordion-body\">\n\t\t\t\t\t\t\t\t\t\t<p>New paper in <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/publication\/analyzing-and-synthesizing-genomic-logic-functions\/\">CAV 2014<\/a>\u00a0on Analyzing Genomic Regulatory Networks in Development<\/p>\n<p>New paper in <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/publication\/symbolic-approximation-of-the-bounded-reachability-probability-in-large-markov-chains-extended\/\">QEST 2014<\/a> on Analyzing Probabilistic Models<\/p>\n<p>New paper in <em><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/www.sciencemag.org\/content\/344\/6188\/1156\/suppl\/DC1\" target=\"_self\">Science<\/a><\/em> on Defining an essential transcriptional factor program for na\u00efve pluripotency<\/p>\n\t\t\t\t<\/div>\n\t\t\t<\/div>\n\t\t<\/li>\n\t\t\t\t\t\t<li class=\"m-0\">\n\t\t\t<h4 class=\"accordion-header\">\n\t\t\t\t<button\n\t\t\t\t\tclass=\"btn btn-collapse m-0\"\n\t\t\t\t\ttype=\"button\"\n\t\t\t\t\tdata-mount=\"collapse\"\n\t\t\t\t\tdata-target=\"#collapse-3\"\n\t\t\t\t\taria-expanded=\"false\"\n\t\t\t\t\taria-controls=\"collapse-3\">\n\t\t2013\t\t\t\t<\/button>\n\t\t\t<\/h4>\n\t\t\t<div class=\"collapse\" id=\"collapse-3\">\n\t\t\t\t<div class=\"accordion-body\">\n\t\t\t\t\t\t\t\t\t\t<p>Paper in <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/publication\/smt-based-analysis-of-biological-computation\/\" target=\"_self\">NASA Formal Methods 2013<\/a>\u00a0(<a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/www.ustream.tv\/recorded\/32833853\" target=\"_self\">Talk<\/a>)<\/p>\n<p>You can try out several of the z3-4Biology examples directly from your browser in the rise4fun environment at <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/rise4fun.com\/Z34Biology\">http:\/\/rise4fun.com\/Z34Biology<\/a><\/p>\n<p>You can download all updated models and analysis problems, both\u00a0as simple textual representations or translated into\u00a0benchmarks using the SMT-LIB format. These examples include problems from the analysis of\u00a0Boolean networks such as gene regulation networks and chemical reaction networks such as DNA circuits. The benchmarks are available as a package from <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-z34bio_benchmarks.zip\" target=\"_self\">here<\/a>.<\/p>\n\t\t\t\t<\/div>\n\t\t\t<\/div>\n\t\t<\/li>\n\t\t\t\t\t\t\t\t\t<\/ul>\n\t\t<\/div>\n\t\t\n<\/div>\n<div id=\"en-usprojectsz3-4biologydefault\" class=\"page-content\">\n<h3 align=\"justify\">Motivation<\/h3>\n<p align=\"justify\">Many of the basic principles governing the development and function of living organisms remain poorly understood, despite the significant progress in molecular and cellular biology and breakthroughs in experimental methods. The development of computational models can improve our understanding of biological systems and biological computation and help address questions like what cells compute, how do they perform computation, and in what ways can such computation be modified or engineered, for example, to allow intervening with abnormal behavior (disease) or designing computational devices using biological principles. To answer such questions, model simulation is often not sufficient and more powerful analysis methods are needed.<\/p>\n<p align=\"justify\">Inspired by the study of engineered computational systems such as computer hardware and software, the application of formal methods has recently attracted attention in the context of biological computation. However, formal methods in biology are often implemented as stand-alone tools focused on specific problems, thereby hindering the reproducibility of results and the collaborative improvement of the procedures.<\/p>\n<p align=\"justify\">Here, we make available a collection of biological models from a variety of areas including gene regulation and signalling networks, developmental biology, synthetic biology and DNA computing. Despite the various formalisms used initially to construct these models, here they are encoded using a unified representation, allowing their analysis using SMT solvers such as Z3. The richness of the SMT problem can accommodate procedures to address a diverse set of biological questions. We demonstrate\u00a0potential application through several procedures\u00a0(also made available on this web site), which include system stability analysis,\u00a0identification of gene knockouts and\u00a0verification of\u00a0a type of\u00a0DNA computing circuits.<\/p>\n<\/div>\n<div id=\"en-usprojectsz3-4biologydefault\" class=\"page-content\">\n<h3>Model structure and file format<\/h3>\n<p>All models and analysis procedures are made available in the SMT-LIB format (as plain text files). Currently, the models are constructed using quantified\u00a0bit-vectors, which\u00a0are supported by the Z3 solver (to the best of our knowledge Z3 is currently the only solver which supports the UFBV logic).\u00a0A convenient way to get started is to use the online version of the Z3 solver available <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/rise4fun.com\/Z3\/\">here<\/a>. To do so, simply copy\u00a0the\u00a0SMT description of a model or procedure of interest from the appropriate file, paste it into the Z3 solver and press &#8220;ask Z3&#8221;. Note that there are some limitations to the online version of Z3.<\/p>\n<\/div>\n<div id=\"en-usprojectsz3-4biologydefault\" class=\"page-content\">\n<h3 align=\"left\">Boolean Networks<\/h3>\n<\/div>\n<div id=\"en-usprojectsz3-4biologydefault\" class=\"page-content\">\n\t\t\t<div class=\"moray-accordion\" data-show=\"false\">\n\t\t\t\t\t\t\t<div class=\"clearfix\">\n\t\t\t\t\t<div\n\t\t\t\t\t\tclass=\"btn-group align-items-center mb-g float-sm-right\"\n\t\t\t\t\t\trole=\"group\"\n\t\t\t\t\t\tdata-mount=\"collapse-controls\"\n\t\t\t\t\t\tdata-bi-aN=\"accordion-collapse-controls\"\n\t\t\t\t\t\tdata-target=\"#accordion-4\">\n\t\t\t\t\t\t<button class=\"btn btn-link m-0\" aria-disabled=\"false\" aria-pressed=\"false\" data-action=\"expand\" type=\"button\" data-bi-cN=\"Expand all\">Expand all<\/button>\n\t\t\t\t\t\t<span aria-hidden=\"true\"> | <\/span>\n\t\t\t\t\t\t<button class=\"btn btn-link m-0\" aria-disabled=\"false\" aria-pressed=\"false\" data-action=\"collapse\" type=\"button\" data-bi-cN=\"Collapse all\">Collapse all<\/button>\n\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t\t\t<ul class=\"accordion\" id=\"accordion-4\">\n\t\t\t\t\t\t\t\t\t\t\t\t\t<li class=\"m-0\">\n\t\t\t<h4 class=\"accordion-header\">\n\t\t\t\t<button\n\t\t\t\t\tclass=\"btn btn-collapse m-0\"\n\t\t\t\t\ttype=\"button\"\n\t\t\t\t\tdata-mount=\"collapse\"\n\t\t\t\t\tdata-target=\"#collapse-5\"\n\t\t\t\t\taria-expanded=\"false\"\n\t\t\t\t\taria-controls=\"collapse-5\">\n\t\tSynchronous models\t\t\t\t<\/button>\n\t\t\t<\/h4>\n\t\t\t<div class=\"collapse\" id=\"collapse-5\">\n\t\t\t\t<div class=\"accordion-body\">\n\t\t\t\t\t\t\t\t\t\t<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-toy1_sync.txt\" target=\"_self\">toy1<\/a><\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-toy2_sync.txt\" target=\"_self\">toy2<\/a><\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-toy3_sync.txt\" target=\"_self\">toy3<\/a><\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-arabidopsis_sync.txt\" target=\"_self\">arabidopsis<\/a><\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-budding_yeast_sync.txt\" target=\"_self\">budding yeast<\/a><\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-drosophila4_sync.txt\" target=\"_self\">drosophila<\/a><\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-fission_yeast_sync.txt\" target=\"_self\">fission yeast<\/a><\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-mammalian_sync.txt\" target=\"_self\">mammalian<\/a><\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-tcr_sync.txt\" target=\"_self\">tcr sync<\/a><\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-thelper_sync.txt\" target=\"_self\">t helper<\/a><\/p>\n\t\t\t\t<\/div>\n\t\t\t<\/div>\n\t\t<\/li>\n\t\t<\/pre><div id=\"en-usprojectsz3-4biologydefault\" class=\"page-content\">\t\t\t\t<li class=\"m-0\">\n\t\t\t<h4 class=\"accordion-header\">\n\t\t\t\t<button\n\t\t\t\t\tclass=\"btn btn-collapse m-0\"\n\t\t\t\t\ttype=\"button\"\n\t\t\t\t\tdata-mount=\"collapse\"\n\t\t\t\t\tdata-target=\"#collapse-6\"\n\t\t\t\t\taria-expanded=\"false\"\n\t\t\t\t\taria-controls=\"collapse-6\">\n\t\tAsynchronous models\t\t\t\t<\/button>\n\t\t\t<\/h4>\n\t\t\t<div class=\"collapse\" id=\"collapse-6\">\n\t\t\t\t<div class=\"accordion-body\">\n\t\t\t\t\t\t\t\t\t\t<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-toy1_async.txt\" target=\"_self\">toy1<\/a><\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-toy2_async.txt\" target=\"_self\">toy2<\/a><\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-toy3_async.txt\" target=\"_self\">toy3<\/a><\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-arabidopsis_async.txt\" target=\"_self\">arabidopsis<\/a><\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-budding_yeast_async.txt\" target=\"_self\">budding yeast<\/a><\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-drosophila4_async.txt\" target=\"_self\">drosophila<\/a><\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-fission_yeast_async.txt\" target=\"_self\">fission yeast<\/a><\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-mammalian_async.txt\" target=\"_self\">mammalian<\/a><\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-tcr_async.txt\" target=\"_self\">tcr<\/a><\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-thelper_async.txt\" target=\"_self\">t helper<\/a><\/pre>\n<pre>\n\t\t\t\t<\/div>\n\t\t\t<\/div>\n\t\t<\/li>\n\t\t<\/pre><\/div><div id=\"en-usprojectsz3-4biologydefault\" class=\"page-content\">\t\t\t\t<li class=\"m-0\">\n\t\t\t<h4 class=\"accordion-header\">\n\t\t\t\t<button\n\t\t\t\t\tclass=\"btn btn-collapse m-0\"\n\t\t\t\t\ttype=\"button\"\n\t\t\t\t\tdata-mount=\"collapse\"\n\t\t\t\t\tdata-target=\"#collapse-7\"\n\t\t\t\t\taria-expanded=\"false\"\n\t\t\t\t\taria-controls=\"collapse-7\">\n\t\tStability analysis\t\t\t\t<\/button>\n\t\t\t<\/h4>\n\t\t\t<div class=\"collapse\" id=\"collapse-7\">\n\t\t\t\t<div class=\"accordion-body\">\n\t\t\t\t\t\t\t\t\t\t<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-toy1.txt\" target=\"_self\">toy1<\/a><\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-toy2.txt\" target=\"_self\">toy2<\/a><\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-toy3.txt\" target=\"_self\">toy3<\/a><\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-arabidopsis.txt\">arabidopsis<\/a>        [<a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/rise4fun.com\/Z34Biology\/arabidopsis_st\">Ask Z3-4Bio<\/a>]<\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-budding_yeast.txt\" target=\"_self\">budding yeast<\/a>      [<a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/rise4fun.com\/Z34Biology\/budding_yeast_st\">Ask Z3-4Bio<\/a>]<\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-drosophila4.txt\" target=\"_self\">drosophila<\/a><\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-fission_yeast.txt\" target=\"_self\">fission yeast<\/a>      [<a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/rise4fun.com\/Z34Biology\/fission_yeast_st\">Ask Z3-4Bio<\/a>]<\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-mammalian.txt\" target=\"_self\">mammalian<\/a>          [<a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/www.rise4fun.com\/Z34Biology\/mammalian_st\">Ask Z3-4Bio<\/a>]<\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-tcr.txt\" target=\"_self\">tcr<\/a><\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-thelper.txt\" target=\"_self\">t helper<\/a>           <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/rise4fun.com\/Z34Biology\/t_helper_st\">[Ask Z3-4Bio]<\/a><\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-nature02456-s2_rev1.txt\" target=\"_self\">metabolic regulation<\/a><\/pre>\n<pre>\n\t\t\t\t<\/div>\n\t\t\t<\/div>\n\t\t<\/li>\n\t\t<\/pre><\/div><div id=\"en-usprojectsz3-4biologydefault\" class=\"page-content\">\t\t\t\t<li class=\"m-0\">\n\t\t\t<h4 class=\"accordion-header\">\n\t\t\t\t<button\n\t\t\t\t\tclass=\"btn btn-collapse m-0\"\n\t\t\t\t\ttype=\"button\"\n\t\t\t\t\tdata-mount=\"collapse\"\n\t\t\t\t\tdata-target=\"#collapse-8\"\n\t\t\t\t\taria-expanded=\"false\"\n\t\t\t\t\taria-controls=\"collapse-8\">\n\t\tIdentification of gene knockouts\t\t\t\t<\/button>\n\t\t\t<\/h4>\n\t\t\t<div class=\"collapse\" id=\"collapse-8\">\n\t\t\t\t<div class=\"accordion-body\">\n\t\t\t\t\t\t\t\t\t\t<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-toy1ko.txt\" target=\"_self\">toy1<\/a><\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-toy2ko.txt\" target=\"_self\">toy2<\/a><\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-toy3ko.txt\" target=\"_self\">toy3<\/a><\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-arabidopsisko.txt\" target=\"_self\">arabidopsis<\/a>        [<a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/rise4fun.com\/Z34Biology\/arabidopsis_KO\">Ask Z3-4Bio<\/a>]<\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-budding_yeastko.txt\" target=\"_self\">budding yeast<\/a>      [<a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/rise4fun.com\/Z34Biology\/budding_yeast_KO\">Ask Z3-4Bio<\/a>]<\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-drosophila4ko.txt\" target=\"_self\">drosophila<\/a><\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-fission_yeastko.txt\" target=\"_self\">fission yeast<\/a><\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-mammalianko.txt\" target=\"_self\">mammalian<\/a>          [<a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/www.rise4fun.com\/Z34Biology\/mammalian_cell_KO\">Ask Z3-4Bio<\/a>]<\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-tcrko.txt\" target=\"_self\">tcr<\/a><\/pre>\n<pre><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-thelperko.txt\" target=\"_self\">t helper<\/a>           [<a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/www.rise4fun.com\/Z34Biology\/mammalian_cell_KO\">Ask Z3-4Bio<\/a>]<\/pre>\n<pre>\n\t\t\t\t<\/div>\n\t\t\t<\/div>\n\t\t<\/li>\n\t\t<\/pre><\/div\t\t\t\t\t\t\t<\/ul>\n\t\t<\/div>\n\t\t\r\n<\/pre>\n<\/div>\n<div id=\"en-usprojectsz3-4biologydefault\" class=\"page-content\">\n<h3><\/h3>\n<h3>Chemical Reaction Networks<\/h3>\n\t\t\t<div class=\"moray-accordion\" data-show=\"false\">\n\t\t\t\t\t\t\t<div class=\"clearfix\">\n\t\t\t\t\t<div\n\t\t\t\t\t\tclass=\"btn-group align-items-center mb-g float-sm-right\"\n\t\t\t\t\t\trole=\"group\"\n\t\t\t\t\t\tdata-mount=\"collapse-controls\"\n\t\t\t\t\t\tdata-bi-aN=\"accordion-collapse-controls\"\n\t\t\t\t\t\tdata-target=\"#accordion-9\">\n\t\t\t\t\t\t<button class=\"btn btn-link m-0\" aria-disabled=\"false\" aria-pressed=\"false\" data-action=\"expand\" type=\"button\" data-bi-cN=\"Expand all\">Expand all<\/button>\n\t\t\t\t\t\t<span aria-hidden=\"true\"> | <\/span>\n\t\t\t\t\t\t<button class=\"btn btn-link m-0\" aria-disabled=\"false\" aria-pressed=\"false\" data-action=\"collapse\" type=\"button\" data-bi-cN=\"Collapse all\">Collapse all<\/button>\n\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t\t\t<ul class=\"accordion\" id=\"accordion-9\">\n\t\t\t\t\t\t\t\t\t\t\t\t\t<li class=\"m-0\">\n\t\t\t<h4 class=\"accordion-header\">\n\t\t\t\t<button\n\t\t\t\t\tclass=\"btn btn-collapse m-0\"\n\t\t\t\t\ttype=\"button\"\n\t\t\t\t\tdata-mount=\"collapse\"\n\t\t\t\t\tdata-target=\"#collapse-10\"\n\t\t\t\t\taria-expanded=\"false\"\n\t\t\t\t\taria-controls=\"collapse-10\">\n\t\tDNA Transducer gate cascade\t\t\t\t<\/button>\n\t\t\t<\/h4>\n\t\t\t<div class=\"collapse\" id=\"collapse-10\">\n\t\t\t\t<div class=\"accordion-body\">\n\t\t\t\t\t\t\t\t\t\t<table style=\"height: 479px\" width=\"372\">\n<tbody>\n<tr>\n<td>\n<p align=\"center\"><strong>N\u00a0<\/strong><\/p>\n<\/td>\n<td>\n<p align=\"center\"><strong>Bad<\/strong><\/p>\n<\/td>\n<td>\n<p align=\"center\"><strong>Good<\/strong><\/p>\n<\/td>\n<\/tr>\n<tr>\n<td>\n<p align=\"center\">1<\/p>\n<\/td>\n<td>\n<p align=\"center\"><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-trans_cascade1_bad.txt\" target=\"_self\">model<\/a><\/p>\n<\/td>\n<td>\n<p align=\"center\"><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-trans_cascade1_good.txt\" target=\"_self\">model<\/a><\/p>\n<\/td>\n<\/tr>\n<tr>\n<td>\n<p align=\"center\">2<\/p>\n<\/td>\n<td>\n<p align=\"center\"><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-trans_cascade2_bad.txt\" target=\"_self\">model<\/a><\/p>\n<\/td>\n<td>\n<p align=\"center\"><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-trans_cascade2_good.txt\" target=\"_self\">model<\/a><\/p>\n<\/td>\n<\/tr>\n<tr>\n<td>\n<p align=\"center\">3<\/p>\n<\/td>\n<td>\n<p align=\"center\"><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-trans_cascade3_bad.txt\" target=\"_self\">model<\/a><\/p>\n<\/td>\n<td>\n<p align=\"center\"><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-trans_cascade3_good.txt\" target=\"_self\">model<\/a><\/p>\n<\/td>\n<\/tr>\n<tr>\n<td>\n<p align=\"center\">4<\/p>\n<\/td>\n<td>\n<p align=\"center\"><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-trans_cascade4_bad.txt\" target=\"_self\">model<\/a><\/p>\n<\/td>\n<td>\n<p align=\"center\"><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-trans_cascade4_good.txt\" target=\"_self\">model<\/a><\/p>\n<\/td>\n<\/tr>\n<tr>\n<td>\n<p align=\"center\">5<\/p>\n<\/td>\n<td>\n<p align=\"center\"><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-trans_cascade5_bad.txt\" target=\"_self\">model<\/a><\/p>\n<\/td>\n<td>\n<p align=\"center\"><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-trans_cascade5_good.txt\" target=\"_self\">model<\/a><\/p>\n<\/td>\n<\/tr>\n<tr>\n<td>\n<p align=\"center\">6<\/p>\n<\/td>\n<td>\n<p align=\"center\"><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-trans_cascade6_bad.txt\" target=\"_self\">model<\/a><\/p>\n<\/td>\n<td>\n<p align=\"center\"><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-trans_cascade6_good.txt\" target=\"_self\">model<\/a><\/p>\n<\/td>\n<\/tr>\n<tr>\n<td>\n<p align=\"center\">7<\/p>\n<\/td>\n<td>\n<p align=\"center\"><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-trans_cascade7_bad.txt\" target=\"_self\">model<\/a><\/p>\n<\/td>\n<td>\n<p align=\"center\"><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-trans_cascade7_good.txt\" target=\"_self\">model<\/a><\/p>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n\t\t\t\t<\/div>\n\t\t\t<\/div>\n\t\t<\/li>\n\t\t\t\t\t\t\t\t\t<\/ul>\n\t\t<\/div>\n\t\t\n<\/div>\n<div id=\"en-usprojectsz3-4biologydefault\" class=\"page-content\">\n<h3>Scenario-based Models<\/h3>\n<p><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-vpc.txt\" target=\"_self\"><em>C. elegans<\/em> vulval cell fate specification model (VPC)<\/a><\/p>\n<\/div>\n<div id=\"en-usprojectsz3-4biologydefault\" class=\"page-content\">\n<h3>Gene circuits<\/h3>\n<p><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/02\/z3-4biology-genecirc.txt\" target=\"_self\">Simple gene circuit design problem<\/a><\/p>\n<\/div>\n","protected":false},"excerpt":{"rendered":"<p>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 [&hellip;]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"footnotes":""},"research-area":[13553],"msr-locale":[268875],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-170870","msr-project","type-msr-project","status-publish","hentry","msr-research-area-medical-health-genomics","msr-locale-en_us","msr-archive-status-active"],"msr_project_start":"2007-01-01","related-publications":[164938,166508,166733,167077,294995,164420,164795],"related-downloads":[],"related-videos":[],"related-groups":[],"related-events":[],"related-opportunities":[],"related-posts":[],"related-articles":[],"tab-content":[],"slides":[],"related-researchers":[],"msr_research_lab":[199561],"msr_impact_theme":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170870"}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-project"}],"version-history":[{"count":3,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170870\/revisions"}],"predecessor-version":[{"id":559761,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170870\/revisions\/559761"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=170870"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=170870"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=170870"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=170870"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=170870"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}