Formal Verification Research

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

						@inproceedings{Budde2021,
							Author = {Budde, Carlos E. and Hartmanns, Arnd and Klauck, Michaela and Kretinsky, Jan and Parker, David, and Quatmann, Tim and Turrini, Andrea and Zhang, Zhen},
							Booktitle = {International Symposium On Leveraging Applications of Formal Methods, Verification and Validation},
							Title = {On Correctness, Precision, and Performance in Quantitative Verification},
							Year = {2021}
						}
					

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

						@inproceedings{Bucherl2020,
							Author = {B\"{u}cherl, Lukas and Mante, Jeanet and Fontanarrosa, Pedro and Zhang, Zhen and Jepsen, Brett and Roberts, Riley and Myers, Chris J.},
							Booktitle = {International Workshop on Bio-Design Automation},
							Pages = {39--40},
							Title = {Genetic Circuit Hazard Analysis Using {STAMINA}},
							Year = {2020}
						}
					

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

						@inproceedings{Noel2020,
							Author = {Daniel, Noel and Shabanian, Tahmoures and Basu, Prabal and Chakraborty, Koushik and Roy, Sanghamitra and Zhang, Zhen},
							Booktitle = {Asia and South Pacific Design Automation Conference},
							Title = {EFFORT: Enhancing Energy Efficiency and Error Resilience of a Near-Threshold Tensor Processing Unit},
							Year = {2020}
						}
					

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

						@book{DBLP:series/cb/30,
							Bibsource = {dblp computer science bibliography, https://dblp.org},
							Biburl = {https://dblp.org/rec/bib/series/cb/30},
							Doi = {10.1007/978-3-030-17297-8},
							Editor = {Pietro Li{\`{o}} and Paolo Zuliani},
							Isbn = {978-3-030-17296-1},
							Publisher = {Springer},
							Series = {Computational Biology},
							Timestamp = {Thu, 13 Jun 2019 09:13:47 +0200},
							Title = {Automated Reasoning for Systems Biology and Medicine},
							Url = {https://doi.org/10.1007/978-3-030-17297-8},
							Volume = {30},
							Year = {2019},
							Bdsk-Url-1 = {https://doi.org/10.1007/978-3-030-17297-8}
						}
					

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

						@inproceedings{Lewis2019,
							Abstract = {The design of modern network-on-chip (NoC) systems faces reliability challenges due to process and environmental variations. Peak power supply noise (PSN) in the power delivery network of a NoC device plays a critical role in determining reliable operations: PSN typically leads to voltage droop, which can cause timing errors in the NoC router pipelines. Existing simulation-based approaches cannot provide rigorous, worst-case reliability guarantees on the probabilistic behaviors of PSN. To address this problem, this paper takes a significant step in formally analyzing PSN in modern NoCs. Specifically, we present a probabilistic model checking approach for the rigorous characterization of PSN for a generic central router of a large mesh-NoC system, under the Round Robin scheduling mechanism with a uniform random network traffic load. Defining features for PSN are extracted at the behavioral level to facilitate property formulation. Several abstract models have been derived for the central router's concrete model based on the observations of its arbiter's conflict resolution behavior. Probabilistic modeling and verification are performed using the Modest  Toolset. Results show significant scalability of our abstract models, and reveal key PSN characteristics that are indicative of NoC design and optimization.},
							Address = {Cham},
							Author = {Lewis, Benjamin and Hartmanns, Arnd and Basu, Prabal and Jayashankara Shridevi, Rajesh and Chakraborty, Koushik and Roy, Sanghamitra and Zhang, Zhen},
							Booktitle = {Formal Methods for Industrial Critical Systems},
							Editor = {Larsen, Kim Guldstrand and Willemse, Tim},
							Isbn = {978-3-030-27008-7},
							Pages = {110--126},
							Publisher = {Springer International Publishing},
							Title = {Probabilistic Verification for Reliable Network-on-Chip System Design},
							Year = {2019}
						}
					

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

						@article{Madsen2019,
							Author = {Madsen, Curtis and Go{\~n}i Moreno, Angel and P, Umesh and Palchick, Zachary and Roehner, Nicholas and Atallah, Christian and Bartley, Bryan and Choi, Kiri and Cox Robert, Sidney and Gorochowski, Thomas and Gr{\"u}nberg, Raik and Macklin, Chris and McLaughlin, James and Meng, Xianwei and Nguyen, Tramy and Pocock, Matthew and Samineni, Meher and Scott-Brown, James and Tarter, Ysis and Zhang, Michael and Zhang, Zhen and Zundel, Zach and Beal, Jacob and Bissell, Michael and Clancy, Kevin and Gennari, John H. and Misirli, Goksel and Myers, Chris and Oberortner, Ernst and Sauro, Herbert and Wipat, Anil},
							Doi = {10.1515/jib-2019-0025},
							Isbn = {16134516},
							J2 = {jib},
							Journal = {Journal of Integrative Bioinformatics},
							M1 = {2},
							Month = {2019-08-21},
							Title = {Synthetic Biology Open Language ({SBOL}) Version 2.3},
							Ty = {GENERIC},
							Url = {https://www.degruyter.com/view/j/jib.2019.16.issue-2/jib-2019-0025/jib-2019-0025.xml},
							Volume = {16},
							Year = {2019},
							Year1 = {2019},
							Bdsk-Url-1 = {https://www.degruyter.com/view/j/jib.2019.16.issue-2/jib-2019-0025/jib-2019-0025.xml%20%20},
							Bdsk-Url-2 = {https://doi.org/10.1515/jib-2019-0025%20}
						}
					

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

						@inproceedings{Smith2019,
							Author = {Smith, Joshua and Huang, Xiaowei and Swaminathan, Viswanathan and Zhang, Zhen},
							Booktitle = {2nd Workshop on Formal Methods for ML-Enabled Autonomous Systems},
							Title = {Improving Deep Neural Network Verification Using Specification-Guided Search},
							Year = {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

						@incollection{Neupane2019,
							Abstract = {There has been an increasing demand for formal methods in the design process of safety-critical synthetic genetic circuitsGenetic circuit. Probabilistic modelProbabilistic model checking checkingModel checking techniques have demonstrated significant potential in analyzing the intrinsic probabilistic behaviors of complex genetic circuitGenetic circuit designs. However, its inability to scale limits its applicability in practice. This chapter addresses the scalability problem by presenting a state-space approximation method to remove unlikely states resulting in a reduced, finite state representation of the infinite-state continuous-time Markov chainMarkov chain that is amenable to probabilistic modelProbabilistic model checking checkingModel checking. The proposed method is evaluated on a design of a genetic toggle switchToggle switch. Comparisons with another state-of-the-art tool demonstrate both accuracy and efficiency of the presented method.},
							Address = {Cham},
							Author = {Neupane, Thakur and Zhang, Zhen and Madsen, Curtis and Zheng, Hao and Myers, Chris J.},
							Booktitle = {Automated Reasoning for Systems Biology and Medicine},
							Chapter = {12},
							Doi = {10.1007/978-3-030-17297-8_12},
							Editor = {Li{\`o}, Pietro and Zuliani, Paolo},
							Isbn = {978-3-030-17297-8},
							Pages = {327--348},
							Publisher = {Springer International Publishing},
							Title = {Approximation Techniques for Stochastic Analysis of Biological Systems},
							Url = {https://doi.org/10.1007/978-3-030-17297-8_12},
							Volume = {30},
							Year = {2019},
							Bdsk-Url-1 = {https://doi.org/10.1007/978-3-030-17297-8_12}
						}
					

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

						@article{Watanabe2019,
							Author = {Watanabe, Leandro and Nguyen, Tramy and Zhang, Michael and Zundel, Zach and Zhang, Zhen and Madsen, Curtis and Roehner, Nicholas and Myers, Chris},
							Doi = {10.1021/acssynbio.8b00078},
							Eprint = {https://doi.org/10.1021/acssynbio.8b00078},
							Journal = {ACS Synthetic Biology},
							Note = {PMID: 29944839},
							Number = {7},
							Pages = {1560-1563},
							Title = {{iBioSim} 3: A Tool for Model-Based Genetic Circuit Design},
							Url = {https://doi.org/10.1021/acssynbio.8b00078},
							Volume = {8},
							Year = {2019},
							Bdsk-Url-1 = {https://doi.org/10.1021/acssynbio.8b00078}
						}
					

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

						@inproceedings{Neupane2019a,
							Abstract = {Stochastic model checking is a technique for analyzing systems that possess probabilistic characteristics. However, its scalability is limited as probabilistic models of real-world applications typically have very large or infinite state space. This paper presents a new infinite state CTMC model checker, STAMINA, with improved scalability. It uses a novel state space approximation method to reduce large and possibly infinite state CTMC models to finite state representations that are amenable to existing stochastic model checkers. It is integrated with a new property-guided state expansion approach that improves the analysis accuracy. Demonstration of the tool on several benchmark examples shows promising results in terms of analysis efficiency and accuracy compared with a state-of-the-art CTMC model checker that deploys a similar approximation method.},
							Address = {Cham},
							Author = {Neupane, Thakur and Myers, Chris J. and Madsen, Curtis and Zheng, Hao and Zhang, Zhen},
							Booktitle = {Computer Aided Verification},
							Editor = {Dillig, Isil and Tasiran, Serdar},
							Isbn = {978-3-030-25540-4},
							Pages = {540--549},
							Publisher = {Springer International Publishing},
							Title = {{STAMINA}: STochastic Approximate Model-Checker for INfinite-State Analysis},
							Year = {2019}
						}
					

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

						@article{Cox2018,
							Author = {Sidney, Cox Robert and Curtis, Madsen and Alastair, McLaughlin James and Tramy, Nguyen and Nicholas, Roehner and Bryan, Bartley and Jacob, Beal and Michael, Bissell and Kiri, Choi and Kevin, Clancy and Raik, Gr{\"u}nberg and Chris, Macklin and Goksel, Misirli and Ernst, Oberortner and Matthew, Pocock and Meher, Samineni and Michael, Zhang and Zhen, Zhang and Zach, Zundel and H., Gennari John and Chris, Myers and Herbert, Sauro and Anil, Wipat},
							Day = {10-23T07:23:46.069+02:00},
							Doi = {10.1515/jib-2018-0001},
							Journal = {Journal of Integrative Bioinformatics},
							Month = {10},
							Note = {1},
							Title = {Synthetic Biology Open Language (SBOL) Version 2.2.0},
							Url = {https://doi.org/10.1515/jib-2018-0001},
							Volume = {15},
							Year = {2018},
							Bdsk-Url-1 = {https://doi.org/10.1515/jib-2018-0001}
						}
					

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

						@article{Zundel2017,
							Abstract = { This paper presents a new validation and conversion utility for the Synthetic Biology Open Language (SBOL). This utility can be accessed directly in software using the libSBOLj library, through a web interface, or using a web service via RESTful API calls. The validator checks all required and best practice rules set forth in the SBOL specification document, and it reports back to the user the location within the document of any errors found. The converter is capable of translating from/to SBOL 1, GenBank, and FASTA formats to/from SBOL 2. The SBOL Validator/Converter utility is released freely and open source under the Apache 2.0 license. The online version of the validator/converter utility can be found here: http://www.async.ece.utah.edu/sbol-validator/. The source code for the validator/converter can be found here: http://github.com/SynBioDex/SBOL-Validator/. },
							Author = {Zundel, Zach and Samineni, Meher and Zhang, Zhen and Myers, Chris J.},
							Doi = {10.1021/acssynbio.6b00277},
							Eprint = {https://doi.org/10.1021/acssynbio.6b00277},
							Journal = {ACS Synthetic Biology},
							Note = {PMID: 28033703},
							Number = {7},
							Pages = {1161-1168},
							Title = {A Validator and Converter for the Synthetic Biology Open Language},
							Url = {https://doi.org/10.1021/acssynbio.6b00277},
							Volume = {6},
							Year = {2017},
							Bdsk-Url-1 = {https://doi.org/10.1021/acssynbio.6b00277}
						}
					

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

						@article{Zhang2016,
							Abstract = {A fault-tolerant routing algorithm in Network-on-Chip (NoC) architectures provides adaptivity for on-chip communications. Adding fault-tolerance adaptivity to a routing algorithm increases its design complexity and makes it prone to deadlock and other problems if improperly implemented. Formal verification techniques are needed to check the correctness of the design. This paper describes the discovery of a potential livelock problem through formal analysis on an extension of the link-fault tolerant NoC architecture introduced by Wu et al. In the process of eliminating this problem, an improved routing architecture is derived. The improvement simplifies the routing architecture, enabling successful verification using the CADP verification toolbox. The routing algorithm is proven to have several desirable properties including deadlock and livelock freedom, and tolerance to a single-link-fault.},
							Author = {Zhen Zhang and Wendelin Serwe and Jian Wu and Tomohiro Yoneda and Hao Zheng and Chris Myers},
							Doi = {https://doi.org/10.1016/j.scico.2016.01.002},
							Issn = {0167-6423},
							Journal = {Science of Computer Programming},
							Keywords = {Fault-tolerant routing, Formal methods, Model checking, Network-on-chip, Process calculus},
							Note = {Formal Methods for Industrial Critical Systems (FMICS'2014)},
							Pages = {24 - 39},
							Title = {An improved fault-tolerant routing algorithm for a Network-on-Chip derived with formal analysis},
							Url = {http://www.sciencedirect.com/science/article/pii/S0167642316000125},
							Volume = {118},
							Year = {2016},
							Bdsk-Url-1 = {http://www.sciencedirect.com/science/article/pii/S0167642316000125},
							Bdsk-Url-2 = {https://doi.org/10.1016/j.scico.2016.01.002}
						}
					

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

						@article{Roehner2015a,
							Abstract = { The Synthetic Biology Open Language (SBOL) is a standard that enables collaborative engineering of biological systems across different institutions and tools. SBOL is developed through careful consideration of recent synthetic biology trends, real use cases, and consensus among leading researchers in the field and members of commercial biotechnology enterprises. We demonstrate and discuss how a set of SBOL-enabled software tools can form an integrated, cross-organizational workflow to recapitulate the design of one of the largest published genetic circuits to date, a 4-input AND sensor. This design encompasses the structural components of the system, such as its DNA, RNA, small molecules, and proteins, as well as the interactions between these components that determine the system's behavior/function. The demonstrated workflow and resulting circuit design illustrate the utility of SBOL 2.0 in automating the exchange of structural and functional specifications for genetic parts, devices, and the biological systems in which they operate. },
							Author = {Roehner, Nicholas and Beal, Jacob and Clancy, Kevin and Bartley, Bryan and Misirli, Goksel and Gr{\"u}nberg, Raik and Oberortner, Ernst and Pocock, Matthew and Bissell, Michael and Madsen, Curtis and Nguyen, Tramy and Zhang, Michael and Zhang, Zhen and Zundel, Zach and Densmore, Douglas and Gennari, John H. and Wipat, Anil and Sauro, Herbert M. and Myers, Chris J.},
							Doi = {10.1021/acssynbio.5b00215},
							Eprint = {https://doi.org/10.1021/acssynbio.5b00215},
							Journal = {ACS Synthetic Biology},
							Note = {PMID: 27111421},
							Number = {6},
							Pages = {498-506},
							Title = {Sharing Structure and Function in Biological Design with SBOL 2.0},
							Url = {https://doi.org/10.1021/acssynbio.5b00215},
							Volume = {5},
							Year = {2016},
							Bdsk-Url-1 = {https://doi.org/10.1021/acssynbio.5b00215}
						}
					

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

						@inbook{Madsen2015,
							Abstract = {This chapter describes new analysis and verification techniques for synthetic genetic circuits. In particular, it applies stochastic model checking techniques to models of genetic circuits in order to ensure that they behave correctly and are as robust as possible for a variety of different inputs and parameter settings. In addition to stochastic model checking, this chapter proposes new variants to the incremental stochastic simulation algorithm (iSSA) that are capable of presenting a researcher with a simulation trace of the typical behavior of the system. Before the development of this algorithm, discerning this information was extremely error-prone as it involved performing many simulations and attempting to wade through the massive amounts of data. This algorithm greatly aids researchers in designing genetic circuits as it efficiently shows the researcher the most likely behavior of the circuit. Both the iSSA and stochastic model checking can be used in concert to give a researcher the likelihood that the system exhibits its most typical behavior, as well as, non-typical behaviors. This methodology is applied to several genetic circuits leading to new understanding of the effects of various parameters on the behavior of these circuits.},
							Address = {New York, NY},
							Author = {Madsen, Curtis and Myers, Chris and Roehner, Nicholas and Winstead, Chris and Zhang, Zhen},
							Booktitle = {Computational Methods in Synthetic Biology},
							Doi = {10.1007/978-1-4939-1878-2_11},
							Editor = {Marchisio, Mario Andrea},
							Isbn = {978-1-4939-1878-2},
							Pages = {217--257},
							Publisher = {Springer New York},
							Title = {Efficient Analysis Methods in Synthetic Biology},
							Url = {https://doi.org/10.1007/978-1-4939-1878-2_11},
							Year = {2015},
							Bdsk-Url-1 = {https://doi.org/10.1007/978-1-4939-1878-2_11}
						}
					

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

						@article{Bartley2015,
							Author = {Bryan, Bartley and Jacob, Beal and Kevin, Clancy and Goksel, Misirli and Nicholas, Roehner and Ernst, Oberortner and Matthew, Pocock and Michael, Bissell and Curtis, Madsen and Tramy, Nguyen and Zhen, Zhang and H., Gennari John and Chris, Myers and Anil, Wipat and Herbert, Sauro},
							Day = {10-23T06:23:35.006+02:00},
							Doi = {10.1515/jib-2015-272},
							Journal = {Journal of Integrative Bioinformatics},
							Month = {12},
							Note = {2},
							Pages = {902},
							Title = {Synthetic Biology Open Language (SBOL) Version 2.0.0},
							Url = {https://doi.org/10.1515/jib-2015-272},
							Volume = {12},
							Year = {2015},
							Bdsk-Url-1 = {https://doi.org/10.1515/jib-2015-272}
						}
					

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

						@article{Roehner2015,
							Abstract = { In the context of synthetic biology, model generation is the automated process of constructing biochemical models based on genetic designs. This paper discusses the use cases for model generation in genetic design automation (GDA) software tools and introduces the foundational concepts of standards and model annotation that make this process useful. Finally, this paper presents an implementation of model generation in the GDA software tool iBioSim and provides an example of generating a Systems Biology Markup Language (SBML) model from a design of a 4-input AND sensor written in the Synthetic Biology Open Language (SBOL). },
							Author = {Roehner, Nicholas and Zhang, Zhen and Nguyen, Tramy and Myers, Chris J.},
							Doi = {10.1021/sb5003289},
							Eprint = {https://doi.org/10.1021/sb5003289},
							Journal = {ACS Synthetic Biology},
							Note = {PMID: 25822671},
							Number = {8},
							Pages = {873-879},
							Title = {Generating Systems Biology Markup Language Models from the Synthetic Biology Open Language},
							Url = {https://doi.org/10.1021/sb5003289},
							Volume = {4},
							Year = {2015},
							Bdsk-Url-1 = {https://doi.org/10.1021/sb5003289}
						}
					

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

						@article{Zhang2015,
							Abstract = {The Synthetic Biology Open Language (SBOL) is an emerging data standard for representing synthetic biology designs. The goal of SBOL is to improve the reproducibility of these designs and their electronic exchange between researchers and/or genetic design automation tools. The latest version of the standard, SBOL 2.0, enables the annotation of a large variety of biological components (e.g., DNA, RNA, proteins, complexes, small molecules, etc.) and their interactions. SBOL 2.0 also allows researchers to organize components into hierarchical modules, to specify their intended functions, and to link modules to models that describe their behavior mathematically. To support the use of SBOL 2.0, we have developed thelibSBOLj 2.0Java library, which provides an easy to use Application Programming Interface (API) for developers, including manipulation of SBOL constructs, serialization to and from an RDF/XML file format, and migration support in the form of conversion from the prior SBOL 1.1 standard to SBOL 2.0. This letter describes thelibSBOLj 2.0library and key engineering decisions involved in its design.},
							Author = {Z. Zhang and T. Nguyen and N. Roehner and G. Misirli and M. Pocock and E. Oberortner and M. Samineni and Z. Zundel and J. Beal and K. Clancy and A. Wipat and C. J. Myers},
							Doi = {10.1109/LLS.2016.2546546},
							Issn = {2332-7685},
							Journal = {IEEE Life Sciences Letters},
							Keywords = {Software tools;Synthetic biology;Software libraries;Java;Computational biology;Application programming interfaces;;Application programming interfaces;computational biology;software libraries;software tools;synthetic biology},
							Month = {Dec},
							Number = {4},
							Pages = {34-37},
							Title = {{libSBOLj} 2.0: A Java Library to Support SBOL 2.0},
							Volume = {1},
							Year = {2015},
							Bdsk-Url-1 = {https://doi.org/10.1109/LLS.2016.2546546}
						}
					

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

						@article{Zheng2015,
							Abstract = {This paper presents a compositional framework to address the state explosion problem in model checking of concurrent systems. This framework takes as input a system model described as a network of communicating components in a high-level description language, finds the local state transition models for each individual component where local properties can be verified, and then iteratively reduces and composes the component state transition models to form a reduced global model for the entire system where global safety properties can be verified. The state space reductions used in this framework result in a reduced model that contains the exact same set of observably equivalent executions as in the original model, therefore, no false counter-examples result from the verification of the reduced model. This approach allows designs that cannot be handled monolithically or with partial-order reduction to be verified without difficulty. The experimental results show significant scale-up of this compositional verification framework on a number of non-trivial concurrent system models.},
							Author = {H. Zheng and Z. Zhang and C. J. Myers and E. Rodriguez and Y. Zhang},
							Doi = {10.1109/TC.2014.2329701},
							Issn = {0018-9340},
							Journal = {IEEE Transactions on Computers},
							Keywords = {concurrency (computers);formal verification;compositional model checking;concurrent systems;state explosion problem;high-level description language;local state transition models;component state transition models;reduced global model;global safety properties;state space reductions;partial-order reduction;compositional verification framework;Model checking;Integrated circuit modeling;Approximation methods;Safety;Silicon;Concrete;Complexity theory;Formal verification, model checking, compositional reasoning, minimization, concurrency},
							Month = {June},
							Number = {6},
							Pages = {1607-1621},
							Title = {Compositional Model Checking of Concurrent Systems},
							Volume = {64},
							Year = {2015},
							Bdsk-Url-1 = {https://doi.org/10.1109/TC.2014.2329701}
						}
					

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

						@inproceedings{Zhang2014,
							Abstract = {A fault-tolerant routing algorithm in Network-on-Chip architectures provides adaptivity for on-chip communications. Adding fault-tolerance adaptivity to a routing algorithm increases its design complexity and makes it prone to deadlock and other problems if improperly implemented. Formal verification techniques are needed to check the correctness of the design. This paper performs formal analysis on an extension of the link-fault tolerant Network-on-Chip architecture introduced by Wu et al that supports multiflit wormhole routing. This paper describes several lessons learned during the process of constructing a formal model of this routing architecture. Finally, this paper presents how the deadlock freedom and tolerance to a single-link fault is verified for a two-by-two mesh version of this routing architecture.},
							Address = {Cham},
							Author = {Zhang, Zhen and Serwe, Wendelin and Wu, Jian and Yoneda, Tomohiro and Zheng, Hao and Myers, Chris},
							Booktitle = {Formal Methods for Industrial Critical Systems},
							Editor = {Lang, Fr{\'e}d{\'e}ric and Flammini, Francesco},
							Isbn = {978-3-319-10702-8},
							Pages = {48--62},
							Publisher = {Springer International Publishing},
							Title = {Formal Analysis of a Fault-Tolerant Routing Algorithm for a Network-on-Chip},
							Year = {2014}
						}
					

2014 Stochastic Model Checking of Genetic Circuits J. Emerg. Technol. Comput. Syst. Curtis Madsen, Zhen Zhang, Nicholas Roehner, and Chris Winstead and Chris Myers

						@article{Madsen2014,
							Acmid = {2644817},
							Address = {New York, NY, USA},
							Articleno = {23},
							Author = {Madsen, Curtis and Zhang, Zhen and Roehner, Nicholas and Winstead, Chris and Myers, Chris},
							Doi = {10.1145/2644817},
							Issn = {1550-4832},
							Issue_Date = {December 2014},
							Journal = {J. Emerg. Technol. Comput. Syst.},
							Keywords = {Markov chain analysis, Stochastic model checking, continuous stochastic logic, design space exploration, synthetic genetic circuits},
							Month = dec,
							Number = {3},
							Numpages = {21},
							Pages = {23:1--23:21},
							Publisher = {ACM},
							Title = {Stochastic Model Checking of Genetic Circuits},
							Url = {http://doi.acm.org/10.1145/2644817},
							Volume = {11},
							Year = {2014},
							Bdsk-Url-1 = {http://doi.acm.org/10.1145/2644817},
							Bdsk-Url-2 = {https://doi.org/10.1145/2644817}
						}
					

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

						@inproceedings{Madsen2012,
							Abstract = {When designing and analyzing genetic circuits, researchers are often interested in the probability of the system reaching a given state within a certain amount of time. Usually, this involves simulating the system to produce some time series data and analyzing this data to discern the state probabilities. However, as the complexity of models of genetic circuits grow, it becomes more difficult for researchers to reason about the different states by looking only at time series simulation results of the models. To address this problem, this paper employs the use of stochastic model checking, a method for determining the likelihood that certain events occur in a system, with continuous stochastic logic (CSL) properties to obtain similar results. This goal is accomplished by the introduction of a methodology for converting a genetic circuit model (GCM) into a continuous-time Markov chain (CTMC). This CTMC is analyzed using transient Markov chain analysis to determine the likelihood that the circuit satisfies a given CSL property in a finite amount of time. This paper illustrates a use of this methodology to determine the likelihood of failure in a genetic toggle switch and compares these results to stochastic simulation-based analysis of this same circuit. Our results show that this method results in a substantial speedup as compared with conventional simulation-based approaches.},
							Author = {C. Madsen and C. J. Myers and N. Roehner and C. Winstead and Z. Zhang},
							Booktitle = {2012 IEEE Symposium on Computational Intelligence in Bioinformatics and Computational Biology (CIBCB)},
							Doi = {10.1109/CIBCB.2012.6217255},
							Keywords = {complex networks;equivalent circuits;genetics;Markov processes;molecular biophysics;stochastic model checking;genetic circuit analysis;genetic circuit design;genetic circuit complexity;continuous stochastic logic;CSL properties;continuous time Markov chain;CTMC;transient Markov chain analysis;genetic toggle switch;Integrated circuit modeling;Genetics;Stochastic processes;Production;Analytical models;Computational modeling;Switches;stochastic model checking;genetic circuits;markov chain analysis;continuous stochastic logic;synthetic biology},
							Month = {May},
							Pages = {379-386},
							Title = {Utilizing stochastic model checking to analyze genetic circuits},
							Year = {2012},
							Bdsk-Url-1 = {https://doi.org/10.1109/CIBCB.2012.6217255}
						}
					

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

						@misc{Wu2011,
							Abstract = {Adaptive routing is a sensible approach to enhance fault-tolerance in Network-on-Chip (NoC) architectures, but can cause deadlock if implemented improperly. Glass and Ni proposed an adaptive routing algorithm based on a turn model which is proven to tolerate at least one fault in each routing process and is free of deadlock. However, when faults happen on links of a network instead of on nodes, these two claims are no longer true. This paper proposes an improved routing algorithm based on the Glass/Ni protocol which tolerates a single link fault while still avoiding deadlock in a mesh network. Simulation results indicate that this improved algorithm provides significant improvements in network reliability with minimal cost.},
							Author = {Jian Wu and Zhen Zhang and Chris Myers},
							Howpublished = {Virtual Worldwide Forum for PhD researchers in Electronic Design Automation},
							Month = {November},
							Title = {A Fault-Tolerant Routing Algorithm for a Network-on-Chip Using a Link Fault Model},
							Year = {2011}
						}
					

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

						@inproceedings{Zhang2008,
							Abstract = {Synchronizers are necessary when importing signals into any clocked domain. As multiple different clocks become increasingly common on chips, synchronizers also proliferate. To achieve high performance it is important that the system designer is aware of the timing characteristics of different synchronizers -which are non-deterministic by nature -- and can choose a design to meet their system requirements. This paper Presents a method for analyzing and depicting behavior of synchronizers and applies this to two recognized designs. A detailed analysis of timing boundaries of the two synchronizers is Presented.  The probabilistic behavior of data cycle is then investigated. Analytical expressions for the average data cycle are also derived.},
							Author = {Z. Zhang and J. Garside},
							Booktitle = {20th UK Asynchronous Forum},
							Title = {Performance Analysis of Two Synchronizers},
							Year = {2008}
						}