index.html

<!DOCTYPE html><html lang="en-us" >


<head>
  <meta charset="utf-8" />
  <meta name="viewport" content="width=device-width, initial-scale=1" />
  <meta http-equiv="X-UA-Compatible" content="IE=edge" />
  
  
  
    <meta name="generator" content="Wowchemy 5.5.0 for Hugo" />
  

  
  










  







  
  

  
  
  

  
  
  
  
  
  

  

  
  
  
    
  
  <meta name="description" content="" />

  
  <link rel="alternate" hreflang="en-us" href="https://fluentverification.github.io/" />

  
  
  
    <meta name="theme-color" content="#EF525B" />
  

  
  

  

  <link rel="stylesheet" href="/css/vendor-bundle.min.c7b8d9abd591ba2253ea42747e3ac3f5.css" media="print" onload="this.media='all'">

  
  
  
    
    
      <link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/academicons@1.9.1/css/academicons.min.css" integrity="sha512-W0xM4mr6dEP9nREo7Z9z+9X70wytKvMGeDsj7ps2+xg5QPrEBXC8tAW1IFnzjR6eoJ90JmCnFzerQJTLzIEHjA==" crossorigin="anonymous" media="print" onload="this.media='all'">
    

    
    
    
    
      
      
      
      
        
      
        
      
        
      
        
      
        
      
        
      
    
    
    

    
    
    
      
    
    
    
    
    
    <link rel="stylesheet" href="/css/libs/chroma/github-light.min.css" title="hl-light" media="print" onload="this.media='all'" >
    <link rel="stylesheet" href="/css/libs/chroma/dracula.min.css" title="hl-dark" media="print" onload="this.media='all'" disabled>

    
    
    
      <link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/leaflet@1.7.1/dist/leaflet.min.css" integrity="" crossorigin="anonymous" media="print" onload="this.media='all'">
    

    

    
    
      
      

      
      

      
    
      
      

      
      

      
    
      
      

      
      

      
    
      
      

      
      

      
    
      
      

      
      

      
    
      
      

      
      

      
    
      
      

      
      

      
    
      
      

      
      

      
    
      
      

      
      

      
    
      
      

      
      

      
    
      
      

      
      
        
      

      
    
      
      

      
      

      
    
      
      

      
      

      
    
  

  
  
  
  
  
  <link rel="stylesheet" href="/css/wowchemy.6bbd0690bf5075e032dfd7ba87c5b3b2.css" />

  



  


  


  




  
  
  
    <script src="https://identity.netlify.com/v1/netlify-identity-widget.js"></script>
  

  
    <link rel="alternate" href="/index.xml" type="application/rss+xml" title="FLUENT Verification Project" />
  

  
    <link rel="manifest" href="/manifest.webmanifest" />
  

  <link rel="icon" type="image/png" href="/media/icon_hu153d4cd2b08a4d98b837bc6b658832e0_327877_32x32_fill_lanczos_center_3.png" />
  <link rel="apple-touch-icon" type="image/png" href="/media/icon_hu153d4cd2b08a4d98b837bc6b658832e0_327877_180x180_fill_lanczos_center_3.png" />

  <link rel="canonical" href="https://fluentverification.github.io/" />

  
  
  
  
  
  
  
  
    
    
  
  

  
  
    
    
  
  <meta property="twitter:card" content="summary" />
  
  <meta property="og:site_name" content="FLUENT Verification Project" />
  <meta property="og:url" content="https://fluentverification.github.io/" />
  <meta property="og:title" content="FLUENT Verification Project" />
  <meta property="og:description" content="" /><meta property="og:image" content="https://fluentverification.github.io/media/icon_hu153d4cd2b08a4d98b837bc6b658832e0_327877_512x512_fill_lanczos_center_3.png" />
    <meta property="twitter:image" content="https://fluentverification.github.io/media/icon_hu153d4cd2b08a4d98b837bc6b658832e0_327877_512x512_fill_lanczos_center_3.png" /><meta property="og:locale" content="en-us" />
  
    
      <meta property="og:updated_time" content="2024-06-17T12:00:00&#43;00:00" />
    
  

  

<script type="application/ld+json">
{
  "@context": "https://schema.org",
  "@type": "WebSite",
  "potentialAction": {
    "@type": "SearchAction",
    "target": "https://fluentverification.github.io/?q={search_term_string}",
    "query-input": "required name=search_term_string"
  },
  "url": "https://fluentverification.github.io/"
}
</script>


  
    <script type="application/ld+json">
{
  "@context": "https://schema.org",
  "@type": "Organization",
  "@id": "https://fluentverification.github.io/",
  "name": "FLUENT Verification Project",
  "logo": "https://fluentverification.github.io/media/icon_hu153d4cd2b08a4d98b837bc6b658832e0_327877_192x192_fill_lanczos_center_3.png",
  
  
  
  
  "url": "https://fluentverification.github.io/"
}
</script>

  

  

  





  <title>FLUENT Verification Project</title>
</head>


<body id="top" data-spy="scroll" data-offset="70" data-target="#TableOfContents" class="page-wrapper   "  >

  
  
  
  
  
  
  
  
  
  <script src="/js/wowchemy-init.min.d01667b8e31c51ada8e954590bead094.js"></script>

  


<aside class="search-modal" id="search">
  <div class="container">
    <section class="search-header">

      <div class="row no-gutters justify-content-between mb-3">
        <div class="col-6">
          <h1>Search</h1>
        </div>
        <div class="col-6 col-search-close">
          <a class="js-search" href="#" aria-label="Close"><i class="fas fa-times-circle text-muted" aria-hidden="true"></i></a>
        </div>
      </div>

      <div id="search-box">
        
        <input name="q" id="search-query" placeholder="Search..." autocapitalize="off"
        autocomplete="off" autocorrect="off" spellcheck="false" type="search" class="form-control"
        aria-label="Search...">
        
      </div>

      
      

      

    </section>
    <section class="section-search-results">

      <div id="search-hits">
        
      </div>

    </section>
  </div>
</aside>



  <div class="page-header">
    












<header class="header--fixed">
  <nav class="navbar navbar-expand-lg navbar-light compensate-for-scrollbar" id="navbar-main">
    <div class="container-xl">

      
      <div class="d-none d-lg-inline-flex">
        <a class="navbar-brand" href="/">FLUENT Verification Project</a>
      </div>
      

      
      <button type="button" class="navbar-toggler" data-toggle="collapse"
              data-target="#navbar-content" aria-controls="navbar-content" aria-expanded="false" aria-label="Toggle navigation">
      <span><i class="fas fa-bars"></i></span>
      </button>
      

      
      <div class="navbar-brand-mobile-wrapper d-inline-flex d-lg-none">
        <a class="navbar-brand" href="/">FLUENT Verification Project</a>
      </div>
      

      
      
      <div class="navbar-collapse main-menu-item collapse justify-content-end" id="navbar-content">

        
        <ul class="navbar-nav d-md-inline-flex">
          

          

          
          
          
            
          

          

          
          
          
          

          
            
              
              
            
            
          

          <li class="nav-item">
            <a class="nav-link " href="/people"><span>People</span></a>
          </li>

          
          

          

          
          
          
            
          

          

          
          
          
          

          
            
              
              
            
            
          

          <li class="nav-item">
            <a class="nav-link " href="/event"><span>Events</span></a>
          </li>

          
          

          

          
          
          
            
          

          

          
          
          
          

          
            
              
              
            
            
          

          <li class="nav-item">
            <a class="nav-link " href="/publication"><span>Publications</span></a>
          </li>

          
          

          

          
          
          
            
          

          

          
          
          
          

          
            
              
              
            
            
          

          <li class="nav-item">
            <a class="nav-link " href="/contact"><span>Contact</span></a>
          </li>

          
          

        

          
        </ul>
      </div>

      <ul class="nav-icons navbar-nav flex-row ml-auto d-flex pl-md-2">

        
        

        
        
        <li class="nav-item">
          <a class="nav-link js-search" href="#" aria-label="Search"><i class="fas fa-search" aria-hidden="true"></i></a>
        </li>
        

        
        
        
        <li class="nav-item dropdown theme-dropdown">
          <a href="#" class="nav-link" data-toggle="dropdown" aria-haspopup="true" aria-label="Display preferences">
            <i class="fas fa-moon" aria-hidden="true"></i>
          </a>
          <div class="dropdown-menu">
            <a href="#" class="dropdown-item js-set-theme-light">
              <span>Light</span>
            </a>
            <a href="#" class="dropdown-item js-set-theme-dark">
              <span>Dark</span>
            </a>
            <a href="#" class="dropdown-item js-set-theme-auto">
              <span>Automatic</span>
            </a>
          </div>
        </li>
        

        
        

      </ul>

    </div>
  </nav>
</header>


  </div>

  <div class="page-body">
    
    
    

    


  









  
<span class="js-widget-page d-none"></span>





  
  
  
  





  

  
  
  
  

  

  

  
  
  
  

  

  

  

  
  

  

  
  

  
  
  

  
  
  
  
  

  
  

  

  
  

  
  

  
  <section id="welcome" class="home-section wg-hero  "  >
   <div class="home-section-bg " >
     
   </div>
    <div class="container">

    

      




<div class="row">
  <div class="col-12 col-md-6 text-center text-md-left">


    
      <h1 class="hero-title"><p>FLUENT</p>
<p>Verification Project</p>
</h1>
    

    
      <div class="hero-lead"><br>
<p>The <strong>(FL)orida-(U)tah (E)merging and (N)ano (T)echnologies Verification Project</strong> aims to develop an efficient framework for the stochastic verification of computation and communication systems using emerging technologies.</p>
</div>
    

    
    

    
    

  
  
  </div>
  <div class="col-12 mx-auto col-md-6  hero-media">
      
      

        
        
        
        

        
          
          
            
          
          
        
          
          
          
        
          
          
          
        
        

        <img src="/media/Group_huf90f4e817de21c898bbda3ed8102e210_2232964_400x0_resize_q75_lanczos.jpg" srcset="/media/Group_huf90f4e817de21c898bbda3ed8102e210_2232964_1200x0_resize_q75_lanczos.jpg 1200w,/media/Group_huf90f4e817de21c898bbda3ed8102e210_2232964_800x0_resize_q75_lanczos.jpg 800w,/media/Group_huf90f4e817de21c898bbda3ed8102e210_2232964_400x0_resize_q75_lanczos.jpg 400w" width="4062" height="2708" alt="FLUENT

Verification Project
">
      
    
  </div>
</div>



    

    </div>
  </section>

  

  
  
  
  

  

  

  
  
  
  

  

  

  

  
  

  

  
  

  
  
  

  
  
  
  
  

  
  

  

  
  

  
  

  
  <section id="introduction" class="home-section wg-blank  "  >
   <div class="home-section-bg " >
     
   </div>
    <div class="container">

    
      <div class="row  justify-content-center">
      
        
          <div class="section-heading col-12 mb-3 text-center">
            <h1 class="mb-0">Introduction</h1>
            
          </div>
        
      
    

      



  <div class="col-12">
    <p>This research aims at advancing probabilistic verification techniques for the rigorous design of dependable systems in synthetic biology and nanotechnology. Major goals of the project include the following. First, scale up stochastic model checking with efficient and accurate state space truncation techniques. Secondly, investigate practical stochastic counterexample generation techniques and utilize them to improve the accuracy of the state reductions. Thirdly, derive automated guidance mechanisms learned from stochastic counterexamples to improve the quality and efficiency of rare-event stochastic simulations. Lastly, integrate our proposed framework within existing state-of-the-art stochastic model checking tools, PRISM and STORM; and evaluate the proposed methodology on a wide range of case studies derived from synthetic biology and nanotechnology applications. The combination of these methods into this new methodology is being explored for the first time. Altogether, this research will improve the accuracy of analysis of infinite state stochastic systems with rare-event properties.</p>
<ul class="cta-group">
  <li>
    <a href="./people/"  class="btn btn-primary px-3 py-3">Meet the team →</a>
  </li>
</ul>

  </div>



    
      </div>
    

    </div>
  </section>

  

  
  
  
  

  

  

  
  
  
  

  

  

  

  
  

  

  
  

  
  
  

  
  
  
  
  

  
  

  

  
  

  
  

  
  <section id="nsf" class="home-section wg-blank  "  >
   <div class="home-section-bg " >
     
   </div>
    <div class="container">

    
      <div class="row  justify-content-center">
      
        
          <div class="section-heading col-12 mb-3 text-center">
            <h1 class="mb-0">NSF Acknowledgements</h1>
            
          </div>
        
      
    

      



  <div class="col-12">
    <p>This material is based upon work supported by the National Science Foundation under Grant Nos. 1856733, 1856740, and 1900542. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.</p>

  </div>



    
      </div>
    

    </div>
  </section>

  

  
  
  
  

  

  

  
  
  
  

  

  

  

  
  

  

  
  

  
  
  

  
  
  
  
  

  
  

  

  
  

  
  

  
  <section id="github" class="home-section wg-blank  "  >
   <div class="home-section-bg " >
     
   </div>
    <div class="container">

    
      <div class="row  justify-content-center">
      
        
          <div class="section-heading col-12 mb-3 text-center">
            <h1 class="mb-0">GitHub Repositroy</h1>
            
          </div>
        
      
    

      



  <div class="col-12">
    <p>All projects are open-source and available on GitHub:</p>
<ul class="cta-group">
  <li>
    <a href="https://github.com/fluentverification"  class="btn btn-primary px-3 py-3">GitHub Repositroy</a>
  </li>
</ul>

  </div>



    
      </div>
    

    </div>
  </section>







  </div>

  <div class="page-footer">
    
    
    <div class="container">
      <footer class="site-footer">

  



  

  

  

  
  






  
  
  

  
  
    
  
  
    
  

  

  
  <p class="powered-by copyright-license-text">
    © 2024 Me. This work is licensed under <a href="https://creativecommons.org/licenses/by-nc-nd/4.0" rel="noopener noreferrer" target="_blank">CC BY NC ND 4.0</a>
  </p>
  

  <p class="powered-by footer-license-icons">
    <a href="https://creativecommons.org/licenses/by-nc-nd/4.0" rel="noopener noreferrer" target="_blank" aria-label="Creative Commons">
      <i class="fab fa-creative-commons fa-2x" aria-hidden="true"></i>
      <i class="fab fa-creative-commons-by fa-2x" aria-hidden="true"></i>
      
        <i class="fab fa-creative-commons-nc fa-2x" aria-hidden="true"></i>
      
      
        <i class="fab fa-creative-commons-nd fa-2x" aria-hidden="true"></i>
      
    </a>
  </p>




  <p class="powered-by">
    
    
    
      
      
      
      
      
      
      Published with <a href="https://wowchemy.com/?utm_campaign=poweredby" target="_blank" rel="noopener">Wowchemy</a> — the free, <a href="https://github.com/wowchemy/wowchemy-hugo-themes" target="_blank" rel="noopener">open source</a> website builder that empowers creators.
    
  </p>
</footer>

    </div>
    
  </div>

      

    
    <script src="/js/vendor-bundle.min.d26509351aa0ff874abbee824e982e9b.js"></script>

    
    
    
      

      
      

      

    

    
    
    
      <script src="https://cdn.jsdelivr.net/npm/leaflet@1.7.1/dist/leaflet.min.js" integrity="" crossorigin="anonymous"></script>
    

    
    

    
    
    
      
      <script id="search-hit-fuse-template" type="text/x-template">
        <div class="search-hit" id="summary-{{key}}">
          <div class="search-hit-content">
            <div class="search-hit-name">
              <a href="{{relpermalink}}">{{title}}</a>
              <div class="article-metadata search-hit-type">{{type}}</div>
              <p class="search-hit-description">{{snippet}}</p>
            </div>
          </div>
        </div>
      </script>
      
        <script src="https://cdn.jsdelivr.net/gh/krisk/Fuse@v3.2.1/dist/fuse.min.js" integrity="sha512-o38bmzBGX+hD3JHWUFCDA09btWaqrNmoJ3RXLlrysA7PP01Kgs4UlE4MhelE1v5dJR3+cxlR4qQlotsW7jKsnw==" crossorigin="anonymous"></script>
        <script src="https://cdn.jsdelivr.net/gh/julmot/mark.js@8.11.1/dist/jquery.mark.min.js" integrity="sha512-mhbv5DqBMgrWL+32MmsDOt/OAvqr/cHimk6B8y/bx/xS88MVkYGPiVv2ixKVrkywF2qHplNRUvFsAHUdxZ3Krg==" crossorigin="anonymous"></script>
      
    

    
    

    
    
    
    

    
    
      
      
      
      
      
      
      
    

    

    
    
    
    <script id="page-data" type="application/json">{"use_headroom":false}</script>

    
    
    
    
    
    
    
    
    
    
      
      
    
    
    <script src="/en/js/wowchemy.min.992ab4bf929c75fb2aff9ec73febac85.js"></script>

    
    
      <script src="/js/wowchemy-map.a26e9d2f7238ba5b868384f1c5bc6477.js" type="module"></script>
    
    
    
    
      
<div id="modal" class="modal fade" role="dialog">
  <div class="modal-dialog">
    <div class="modal-content">
      <div class="modal-header">
        <h5 class="modal-title">Cite</h5>
        <button type="button" class="close" data-dismiss="modal" aria-label="Close">
          <span aria-hidden="true">&times;</span>
        </button>
      </div>
      <div class="modal-body">
        <pre><code class="tex hljs"></code></pre>
      </div>
      <div class="modal-footer">
        <a class="btn btn-outline-primary my-1 js-copy-cite" href="#" target="_blank">
          <i class="fas fa-copy"></i> Copy
        </a>
        <a class="btn btn-outline-primary my-1 js-download-cite" href="#" target="_blank">
          <i class="fas fa-download"></i> Download
        </a>
        <div id="modal-error"></div>
      </div>
    </div>
  </div>
</div>

      <script src="/js/wowchemy-publication.68f8d7090562ca65fc6d3cb3f8f2d2cb.js" type="module"></script>






</body>
</html>