USU Formal Verification Research Logo

Formal Verification Research

Zhen Zhang's Research Group at Utah State University

Funded by the National Science Foundation

Nice to meet you!

We're a research lab based at Utah State University in Logan, Utah. We use formal methods to verify engineered systems. We're hard at work exploring a handful of topics:

  • Probabilistic verification of synthetic biology and biochemical reaction networks
    • STAMINA, a tool for probabilistic state space exploration
    • RAGTIMER, a tool for rare event verification
    • Wayfarer, a tool for rare event probability calculation
    • Exploration of multi-threaded state space exploration
    • Contributions to a large collection of Stochastic Model Case Studies
  • Formal verification of Network-on-Chip (NoC)
  • Deep Neural Network (DNN) verification for classification problems
    • Verapak, a tool for DNN adversarial example verification
  • Parameter optimization for biosynthetic pathway models
  • Stochastic modeling of age-related macular degenerative retinal angiogenesis
Our publications are listed below, and our projects are open-source at Github. Many of our group members also contribute to the FLUENT Verification group, a multi-university collaboration for stochastic system verification.

Meet the Team  

Zhen Zhang | Principal Investigator
My primary research interest is in the modeling and verification of concurrent and stochastic systems, ranging from asynchronous systems and distributed protocols to embedded software and biological systems. I am interested in developing theories and algorithms to advance techniques in the area of formal and semi-formal methods, and their applications in system diagnosis and embedded controller and parameter synthesis.            

Student Researchers

Beckey Hu | PhD Student
PMC Applications in Synthetic Biology

Josh Jeppson | PhD Student
Contact for the STAMINA tool
   


Landon Taylor | PhD Student
Chemical Reaction Networks
       

Mason Davis | MS Student
Neural Network Verification
   


Nick Waddoups | MS Student
Architecture Verification
 

Bennett DenBleyker | Undergrad
Neural Network Verification
 


Cassandra DuBose | Undergrad
Biological Systems

Lukas Keller | Undergrad
Stochastic Metabolic Model Verification
 


Easton McBeth | Undergrad
Concurrency Modeling in Dafny
 

Alumni

  • Jonah Boe, Probabilistic Network-on-Chip
  • Bryant Israelsen, Chemical Reaction Networks
  • Riley Roberts, Developer for STAMINA Tool
  • Thakur Neupane, Stochastic Model Checking
  • Joshua Smith, Neural Network Verification

Publications  

You can download a BibTeX file that contains references to all of these papers.

2008 2011 2012 2014 2015 2016 2017 2018 2019 2020 2021 2022 2023 2025

2025

2025 Modest Models and Tools for Real Stochastic Timed Systems Principles of Verification: Cycling the Probabilistic Landscape : Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part II Carlos E. Budde, Pedro R. D'Argenio, Juan A. Fraire, Arnd Hartmanns, and Zhen Zhang

BibTeX   View Paper  

2025 Tools at the Frontiers of Quantitative Verification TOOLympics Challenge 2023 Roman Andriushchenko, Alexander Bork, Carlos E. Budde, Milan Češka, Kush Grover, Ernst Moritz Hahn, Arnd Hartmanns, Bryant Israelsen, Nils Jansen, Joshua Jeppson, Sebastian Junges, Maximilian A. Köhl, Bettina Könighofer, Jan Křetínský, Tobias Meggendorfer, David Parker, Stefan Pranger, Tim Quatmann, Enno Ruijters, Landon Taylor, Matthias Volk, Maximilian Weininger, and Zhen Zhang

BibTeX   View Paper  

2023

2023 Cycle and Commute: Rare-Event Probability Verification for Chemical Reaction Networks Formal Methods in Computer-Aided Design Landon Taylor, Bryant Israelsen, and Zhen Zhang

BibTeX   View Paper  

2023 Efficient Trace Generation for Rare-Event Analysis in Chemical Reaction Networks Model Checking Software Bryant Israelsen, Landon Taylor, and Zhen Zhang

BibTeX   View Paper  

2023 STAMINA in C++: Modernizing an Infinite-State Probabilistic Model Checker Quantitative Evaluation of Systems Joshua Jeppson, Matthias Volk, Bryant Israelsen, Riley Roberts, Andrew Williams, Lukas Buecherl, Chris J. Myers, Hao Zheng, Chris Winstead, and Zhen Zhang

BibTeX   View Paper  

2022

2022 Scaling Up Livelock Verification for Network-on-Chip Routing Algorithms Verification, Model Checking, and Abstract Interpretation Landon Taylor and Zhen Zhang

BibTeX   View Paper  

2022 STAMINA 2.0: Improving Scalability of Infinite-State Stochastic Model Checking Verification, Model Checking, and Abstract Interpretation Riley Roberts, Thakur Neupane, Lukas Buecherl, Chris J. Myers, and Zhen Zhang

BibTeX   View Paper  

2021

2021 A Computational Metabolic Model for Engineered Production of Resveratrol in Escherichia Coli ACS Synthetic Biology Michael Cotner, Jixun Zhan, and Zhen Zhang

BibTeX   View Paper  

2021 On Correctness, Precision, and Performance in Quantitative Verification: QComp 2020 Competition Report Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends Carlos E. Budde, Arnd Hartmanns, Michaela Klauck, Jan Křetínský, David Parker, Tim Quatmann, Andrea Turrini, and Zhen Zhang

BibTeX   View Paper  

2021 Probabilistic Verification for Reliability of a Two-by-Two Network-on-Chip System Formal Methods for Industrial Critical Systems Riley Roberts, Benjamin Lewis, Arnd Hartmanns, Prabal Basu, Sanghamitra Roy, Koushik Chakraborty, and Zhen Zhang

BibTeX   View Paper  

2021 Refutation-Based Adversarial Robustness Verification of Deep Neural Networks Formal Methods for ML-Enabled Autonomous Systems (FoMLAS) Joshua Smith, Jarom Allan, Viswanathan Swaminathan, and Zhen Zhang

BibTeX   View Paper  

2021 Stochastic Hazard Analysis of Genetic Circuits in iBioSim and STAMINA ACS Synthetic Biology Lukas Buecherl, Riley Roberts, Pedro Fontanarrosa, Payton J. Thomas, Jeanet Mante, Zhen Zhang, and Chris J. Myers

BibTeX   View Paper  

2020

2020 (Abstract) A Computational Model of the Effect of VEGF Production in Wet Age-Related Macular Degeneration on Neovascularization Investigative Ophthalmology & Visual Science Kelsey Bradshaw, Elizabeth Vargis, and Zhen Zang

BibTeX   View Paper  

2020 (Abstract) Enhanced Microbial Production of Valuable Natural Products through Computational Metabolic Models International Workshop on Bio-Design Automation (IWBDA) Michael Cotner, Zhen Zhang, and Jixun Zhan

BibTeX   View Paper  

2020 (Abstract) Genetic Circuit Hazard Analysis Using STAMINA International Workshop on Bio-Design Automation (IWBDA) Lukas Bücherl, Jeanet Mante, Pedro Fontanarrosa, Zhen Zhang, Brett Jepsen, Riley Roberts, and Chris J. Myers

BibTeX   View Paper  

2020 EFFORT: Enhancing Energy Efficiency and Error Resilience of a Near-Threshold Tensor Processing Unit 2020 25th Asia and South Pacific Design Automation Conference (ASP-DAC) Noel Daniel Gundi, Tahmoures Shabanian, Prabal Basu, Pramesh Pandey, Sanghamitra Roy, Koushik Chakraborty, and Zhen Zhang

BibTeX   View Paper  

2019

2019 Approximation Techniques for Stochastic Analysis of Biological Systems Automated Reasoning for Systems Biology and Medicine Thakur Neupane, Zhen Zhang, Curtis Madsen, Hao Zheng, and Chris J. Myers

BibTeX   View Paper  

2019 iBioSim 3: A Tool for Model-Based Genetic Circuit Design ACS Synthetic Biology Leandro Watanabe, Tramy Nguyen, Michael Zhang, Zach Zundel, Zhen Zhang, Curtis Madsen, Nicholas Roehner, and Chris Myers

BibTeX   View Paper  

2019 Probabilistic Verification for Reliable Network-on-Chip System Design Formal Methods for Industrial Critical Systems Benjamin Lewis, Arnd Hartmanns, Prabal Basu, Rajesh Jayashankara Shridevi, Koushik Chakraborty, Sanghamitra Roy, and Zhen Zhang

BibTeX   View Paper  

2019 STAMINA: STochastic Approximate Model-Checker for INfinite-State Analysis Computer Aided Verification Thakur Neupane, Chris J. Myers, Curtis Madsen, Hao Zheng, and Zhen Zhang

BibTeX   View Paper  

2019 Synthetic Biology Open Language (SBOL) Version 2.3 Journal of Integrative Bioinformatics Curtis Madsen, Angel Goñi Moreno, Umesh P, Zachary Palchick, Nicholas Roehner, Christian Atallah, Bryan Bartley, Kiri Choi, Robert Sidney Cox, Thomas Gorochowski, Raik Grünberg, Chris Macklin, James McLaughlin, Xianwei Meng, Tramy Nguyen, Matthew Pocock, Meher Samineni, James Scott-Brown, Ysis Tarter, Michael Zhang, Zhen Zhang, Zach Zundel, Jacob Beal, Michael Bissell, Kevin Clancy, John H. Gennari, Goksel Misirli, Chris Myers, Ernst Oberortner, Herbert Sauro, and Anil Wipat

BibTeX   View Paper  

2018

2018 Synthetic Biology Open Language (SBOL) Version 2.2.0 Journal of Integrative Bioinformatics Robert Sidney Cox, Curtis Madsen, James Alastair McLaughlin, Tramy Nguyen, Nicholas Roehner, Bryan Bartley, Jacob Beal, Michael Bissell, Kiri Choi, Kevin Clancy, Raik Grünberg, Chris Macklin, Goksel Misirli, Ernst Oberortner, Matthew Pocock, Meher Samineni, Michael Zhang, Zhen Zhang, Zach Zundel, John H. Gennari, Chris Myers, Herbert Sauro, and Anil Wipat

BibTeX   View Paper  

2017

2017 A Validator and Converter for the Synthetic Biology Open Language ACS Synthetic Biology Zach Zundel, Meher Samineni, Zhen Zhang, and Chris J. Myers

BibTeX   View Paper  

2016

2016 An Improved Fault-Tolerant Routing Algorithm for a Network-on-Chip Derived with Formal Analysis Science of Computer Programming Zhen Zhang, Wendelin Serwe, Jian Wu, Tomohiro Yoneda, Hao Zheng, and Chris Myers

BibTeX   View Paper  

2016 Sharing Structure and Function in Biological Design with SBOL 2.0 ACS Synthetic Biology Nicholas Roehner, Jacob Beal, Kevin Clancy, Bryan Bartley, Goksel Misirli, Raik Grünberg, Ernst Oberortner, Matthew Pocock, Michael Bissell, Curtis Madsen, Tramy Nguyen, Michael Zhang, Zhen Zhang, Zach Zundel, Douglas Densmore, John H. Gennari, Anil Wipat, Herbert M. Sauro, and Chris J. Myers

BibTeX   View Paper  

2015

2015 Compositional Model Checking of Concurrent Systems IEEE Transactions on Computers Hao Zheng, Zhen Zhang, Chris J. Myers, Emmanuel Rodriguez, and Yingying Zhang

BibTeX   View Paper  

2015 Efficient Analysis Methods in Synthetic Biology Computational Methods in Synthetic Biology Curtis Madsen, Chris Myers, Nicholas Roehner, Chris Winstead, and Zhen Zhang

BibTeX   View Paper  

2015 Generating Systems Biology Markup Language Models from the Synthetic Biology Open Language ACS Synthetic Biology Nicholas Roehner, Zhen Zhang, Tramy Nguyen, and Chris J. Myers

BibTeX   View Paper  

2015 libSBOLj 2.0: A Java Library to Support SBOL 2.0 IEEE Life Sciences Letters Zhen Zhang, Tramy Nguyen, Nicholas Roehner, Göksel Misirli, Matthew Pocock, Ernst Oberortner, Meher Samineni, Zach Zundel, Jacob Beal, Kevin Clancy, Anil Wipat, and Chris J. Myers

BibTeX   View Paper  

2015 Synthetic Biology Open Language (SBOL) Version 2.0.0 Journal of Integrative Bioinformatics Bryan Bartley, Jacob Beal, Kevin Clancy, Goksel Misirli, Nicholas Roehner, Ernst Oberortner, Matthew Pocock, Michael Bissell, Curtis Madsen, Tramy Nguyen, Zhen Zhang, John H. Gennari, Chris Myers, Anil Wipat, and Herbert Sauro

BibTeX   View Paper  

2014

2014 Formal Analysis of a Fault-Tolerant Routing Algorithm for a Network-on-Chip Formal Methods for Industrial Critical Systems Zhen Zhang, Wendelin Serwe, Jian Wu, Tomohiro Yoneda, Hao Zheng, and Chris Myers

BibTeX   View Paper  

2014 Stochastic Model Checking of Genetic Circuits ACM Journal on Emerging Technologies in Computing Systems Curtis Madsen, Zhen Zhang, Nicholas Roehner, Chris Winstead, and Chris Myers

BibTeX   View Paper  

2012

2012 Utilizing Stochastic Model Checking to Analyze Genetic Circuits 2012 IEEE Symposium on Computational Intelligence in Bioinformatics and Computational Biology (CIBCB) Curtis Madsen, Chris J. Myers, Nicholas Roehner, Chris Winstead, and Zhen Zhang

BibTeX   View Paper  

2011

2011 A Fault-Tolerant Routing Algorithm for a Network-on-Chip Using a Link Fault Model Virtual Worldwide Forum for PhD Researchers in Electronic Design Automation Jian Wu, Zhen Zhang, and Chris Myers

BibTeX   View Paper  

2008

2008 Performance Analysis of Two Synchronizers 20th UK Asynchronous Forum Z. Zhang and J. Garside

BibTeX   View Paper  

Acknowledgements   

This material is based upon work supported by the National Science Foundation under Grant No. 1856740. 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.

This research is generously supported by Adobe Research.