USU Formal Verification Research Logo

Formal Verification Research

Zhen Zhang's Research Group at Utah State University

Funded by the National Science Foundation

Introduction

We use formal methods to verify a variety of systems. Our projects include STAMINA, neural network verification, network-on-chip verification, and others. Our publications are listed below, and our projects are at Github.

Faculty  

Zhen Zhang | Utah State University
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.

Publications  

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

2021

2021 On Correctness, Precision, and Performance in Quantitative Verification International Symposium On Leveraging Applications of Formal Methods, Verification and Validation Carlos E. Budde, Arnd Hartmanns, Michaela Klauck, Jan Kretinsky, David Parker, Tim Quatmann, Andrea Turrini, and Zhen Zhang

BibTeX   Awaiting Publication  

2020

2020 Genetic circuit hazard analys is using STAMINA International Workshop on Bio-Design Automation Lukas Bücherl, Jeanet Mante, Pedro Fontanarrosa, Zhen Zhang, Brett Jepsen, Riley Roberts, and Chris J. Myers

BibTeX   Awaiting Publication  

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

BibTeX   View Paper  

2019

2019 Automated Reasoning for Systems Biology and Medicine Computational Biology, Springer Pietro Liò and Paolo Zuliani, editors.

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 JayashankaraShridevi, Koushik Chakraborty, Sanghamitra Roy, 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, Sidney Cox Robert, 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  

2019 Improving Deep Neural Network Verification Using Specification-Guided Search 2nd Workshop on Formal Methods for ML-Enabled Autonomous Systems Joshua Smith, Xiaowei Huang, Viswanathan Swaminathan, and Zhen Zhang

BibTeX   View Paper  

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 STAMINA: STochastic Approximate Model-Checker for INfinite-State Analysi Computer Aided Verification Thakur Neupane, Chris J. Myers, Curtis Madsen, Hao Zheng, and Zhen Zhang

BibTeX   View Paper  

2018

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

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  

2015

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

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 Z. Zhang, T. Nguyen, N. Roehner, G. Misirli, M. Pocock, E. Oberortner, M. Samineni, Z. Zundel, J. Beal, K. Clancy, A. Wipat and C. J. Myers

BibTeX   View Paper  

2015 Compositional Model Checking of Concurrent Systems IEEE Transactions on Computers H. Zheng, Z. Zhang, C. J. Myers, E. Rodriguez and Y. Zhang

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 J. Emerg. Technol. Comput. Syst. Curtis Madsen, Zhen Zhang, Nicholas Roehner, and 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) C. Madsen, C. J. Myers, N. Roehner, C. Winstead and Z. 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.