Formal Verification Research

2026 A Standardized SBML/PRISM Benchmark Library for Stochastic Model Checking in Synthetic Biology Journal of Integrative Bioinformatics Mohammad Ahmadi, Bryant Israelsen, Josh Jeppson, Riley Roberts, Landon Taylor, Payton J. Thomas, Chris Winstead, Zhen Zhang, Hao Zheng, Chris J. Myers, and Lukas Buecherl

@article{Ahmadi_Standardized_2026,
	abstract = {Stochastic model checking is a powerful verification technique used in engineering to assess system reliability and correctness. Many synthetic biological systems, including chemical reaction networks, can be modeled as stochastic processes, making stochastic model checking well suited for evaluating and improving their performance. However, direct application in synthetic biology faces domain-specific challenges that often require adapting existing analysis techniques and developing new algorithms that scale to biological complexity. To support this software development, we present a curated library of case studies representing biologically inspired stochastic models with unbounded state spaces. Each case study is provided in both SBML and PRISM formats to support accessibility and interoperability. By openly releasing the library and encouraging community contributions, this work aims to improve reproducibility, enable meaningful tool comparisons, and accelerate development of robust software infrastructure for stochastic model checking in synthetic biology.},
	author = {Ahmadi, Mohammad and Israelsen, Bryant and Jeppson, Josh and Roberts, Riley and Taylor, Landon and Thomas, Payton J. and Winstead, Chris and Zhang, Zhen and Zheng, Hao and Myers, Chris J. and Buecherl, Lukas},
	copyright = {De Gruyter expressly reserves the right to use all content for commercial text and data mining within the meaning of Section 44b of the German Copyright Act.},
	doi = {10.1515/jib-2026-0002},
	file = {/home/landon/Zotero/storage/X6JLAK4B/Ahmadi et al. - 2026 - A standardized SBMLPRISM benchmark library for stochastic model checking in synthetic biology.pdf},
	issn = {1613-4516},
	journal = {Journal of Integrative Bioinformatics},
	langid = {english},
	month = {September},
	publisher = {De Gruyter},
	title = {A Standardized {{SBML}}/{{PRISM}} Benchmark Library for Stochastic Model Checking in Synthetic Biology},
	urldate = {2026-09-10},
	year = {2026}
}
					

2026 Probabilistic Verification for Modular Network-on-Chip Systems Verification, Model Checking, and Abstract Interpretation Nick Waddoups, Jonah Boe, Arnd Hartmanns, Prabal Basu, Sanghamitra Roy, Koushik Chakraborty, and Zhen Zhang

@inproceedings{Waddoups_Probabilistic_2026,
	abstract = {Quantitative verification can provide deep insights~into reliable Network-On-Chip (NoC) designs. It is critical~to understanding and mitigating operational issues caused by~power supply noise (PSN) early in the design process: fluctuations~in network traffic in modern NoC designs cause dramatic variations~in power delivery across the network, leading to unreliability~and errors in data transfers. Further complicating these challenges,~NoC designs vary widely in size, usage, and implementation. This~case study paper presents a principled, systematic, and modular~NoC modeling approach using the Modest language that closely reflects the standard hierarchical design approach in digital systems.~Using the Modest Toolset, functional and quantitative correctness~was established for several NoC models, all of which were instantiated from a generic modular router model. Specifically, this~work verifies the functional correctness of a generic router, inter-router communication, and the entire NoC. Statistical~model checking was used to verify PSN-related properties for NoCs of~size up to \$\$\textbraceleft 8\textbraceright\textbackslash!\textbackslash times \textbackslash!\textbraceleft 8\textbraceright\$\$8\texttimes 8.},
	address = {Cham},
	author = {Waddoups, Nick and Boe, Jonah and Hartmanns, Arnd and Basu, Prabal and Roy, Sanghamitra and Chakraborty, Koushik and Zhang, Zhen},
	booktitle = {Verification, {{Model Checking}}, and {{Abstract Interpretation}}},
	doi = {10.1007/978-3-032-15700-3_18},
	editor = {Chen, Yu-Fang and Jensen, Thomas and Leng{\'a}l, Ond{\v r}ej},
	isbn = {978-3-032-15700-3},
	langid = {english},
	pages = {383--407},
	publisher = {Springer Nature Switzerland},
	title = {Probabilistic {{Verification}} for~{{Modular Network-on-Chip Systems}}},
	year = {2026}
}
					

2026 Ragtimer 1.0: Rapid Rare-Event Partial State Space Construction for Stochastic VAS Proceedings of the 24th International Symposium on Automated Technology for Verification and Analysis (ATVA) Landon Taylor, Joshua Jeppson, Bingqing Hu, Lukas Buecherl, and Zhen Zhang

@inproceedings{zotero-item-3760,
	author = {Taylor, Landon and Jeppson, Joshua and Hu, Bingqing and Buecherl, Lukas and Zhang, Zhen},
	booktitle = {Proceedings of the 24th {{International Symposium}} on {{Automated Technology}} for {{Verification}} and {{Analysis}} ({{ATVA}})},
	publisher = {(To Appear)},
	title = {Ragtimer 1.0: {{Rapid Rare-Event Partial State Space Construction}} for {{Stochastic VAS}}},
	year = {2026}
}
					

2025 (Abstract) Degradation-Driven Failure Minimization in Genetic Circuits Through Model Checking International Workshop on Bio-Design Automation (IWBDA) Landon Taylor, Lukas Buecherl, and Zhen Zhang

@inproceedings{Taylor_Abstract_2025,
	author = {Taylor, Landon and Buecherl, Lukas and Zhang, Zhen},
	booktitle = {International Workshop on Bio-Design Automation ({{IWBDA}})},
	month = {August},
	title = {({{Abstract}}) {{Degradation-Driven Failure Minimization}} in {{Genetic Circuits Through Model Checking}}},
	year = {2025}
}
					

2025 (Abstract) Stochastic Modeling and Experimental Validation of Cannabinoid Biosynthesis in Saccharomyces Cerevisae Innovation through Biological Engineering (IBE) Bingqing Hu, Ammar Mussaji, Joshua Jeppson, Landon Taylor, Jixun Zhan, and Zhen Zhang

@inproceedings{Hu_Abstract_2025,
	author = {Hu, Bingqing and Mussaji, Ammar and Jeppson, Joshua and Taylor, Landon and Zhan, Jixun and Zhang, Zhen},
	booktitle = {Innovation through {{Biological Engineering}} ({{IBE}})},
	month = {September},
	title = {({{Abstract}}) {{Stochastic Modeling}} and {{Experimental Validation}} of {{Cannabinoid Biosynthesis}} in {{Saccharomyces}} Cerevisae},
	year = {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

@incollection{Budde_Modest_2025,
	abstract = {We depend on the safe, reliable, and timely operation~of cyber-physical systems ranging from smart grids to avionics components. Many of them involve time-dependent behaviours and~are subject to randomness. Modelling languages and verification~tools thus need to support these quantitative aspects. This paper gives~an introduction to quantitative verification using the Modest modelling language and the Modest Toolset. It highlights three recent~case studies with increasing demands on model expressiveness and~tool capabilities: A case of power supply noise in a network-on-chip modelled as a Markov chain; a case of message routing in satellite constellations that needs Markov decision processes with distributed information; and a case of optimising an attack on Bitcoin~via Markov automata model checking. For each, we explain the particular conceptual and technical challenges in modelling and verification, and point out open problems for future work.},
	address = {Cham},
	author = {Budde, Carlos E. and D'Argenio, Pedro R. and Fraire, Juan A. and Hartmanns, Arnd and Zhang, Zhen},
	booktitle = {Principles of {{Verification}}: {{Cycling}} the {{Probabilistic Landscape}} : {{Essays Dedicated}} to {{Joost-Pieter Katoen}} on the {{Occasion}} of {{His}} 60th {{Birthday}}, {{Part II}}},
	doi = {10.1007/978-3-031-75775-4_6},
	editor = {Jansen, Nils and Junges, Sebastian and Kaminski, Benjamin Lucien and Matheja, Christoph and Noll, Thomas and Quatmann, Tim and Stoelinga, Mari{\"e}lle and Volk, Matthias},
	isbn = {978-3-031-75775-4},
	langid = {english},
	pages = {115--142},
	publisher = {Springer Nature Switzerland},
	title = {Modest {{Models}} and {{Tools}} for {{Real Stochastic Timed Systems}}},
	urldate = {2024-11-18},
	year = {2025}
}
					

2025 Prefix Trees Improve Memory Consumption in Large-Scale Continuous-Time Stochastic Models arXiv preprint Landon Taylor, Joshua Jeppson, Ahmed Irfan, Lukas Buecherl, Chris Myers, and Zhen Zhang

@misc{Taylor_Prefix_2025,
	abstract = {Highly-concurrent system models with vast state spaces like Chemical Reaction Networks (CRNs) that model biological and chemical systems pose a formidable challenge to cutting-edge formal analysis tools. Although many symbolic approaches have been presented, transient probability analysis of CRNs, modeled as Continuous-Time Markov Chains (CTMCs), requires explicit state representation. For that purpose, current cutting-edge methods use hash maps, which boast constant average time complexity and linear memory complexity. However, hash maps often suffer from severe memory limitations on models with immense state spaces. To address this, we propose using prefix trees to store states for large, highly concurrent models (particularly CRNs) for memory savings. We present theoretical analyses and benchmarks demonstrating the favorability of prefix trees over hash maps for very large state spaces. Additionally, we propose using a Bounded Model Checking (BMC) pre-processing step to impose a variable ordering to further improve memory usage along with preliminary evaluations suggesting its effectiveness. We remark that while our work is motivated primarily by the challenges posed by CRNs, it is generalizable to all CTMC models.},
	archiveprefix = {arXiv},
	author = {Taylor, Landon and Jeppson, Joshua and Irfan, Ahmed and Buecherl, Lukas and Myers, Chris and Zhang, Zhen},
	doi = {10.48550/arXiv.2512.17892},
	eprint = {2512.17892},
	file = {/home/landon/Zotero/storage/REULV7U6/Taylor et al. - 2025 - Prefix Trees Improve Memory Consumption in Large-Scale Continuous-Time Stochastic Models.pdf;/home/landon/Zotero/storage/F4GQ6YED/2512.html},
	month = {December},
	number = {arXiv:2512.17892},
	primaryclass = {cs},
	publisher = {arXiv},
	title = {Prefix {{Trees Improve Memory Consumption}} in {{Large-Scale Continuous-Time Stochastic Models}}},
	urldate = {2026-01-26},
	year = {2025}
}
					

2025 Prefix Trees Improve Memory Consumption in Large-Scale Continuous-Time Stochastic Models arXiv preprint Landon Taylor, Joshua Jeppson, Ahmed Irfan, Lukas Buecherl, Chris Myers, and Zhen Zhang

@misc{taylorPrefixTreesImprove2025,
	abstract = {Highly-concurrent system models with vast state spaces like Chemical Reaction Networks (CRNs) that model biological and chemical systems pose a formidable challenge to cutting-edge formal analysis tools. Although many symbolic approaches have been presented, transient probability analysis of CRNs, modeled as Continuous-Time Markov Chains (CTMCs), requires explicit state representation. For that purpose, current cutting-edge methods use hash maps, which boast constant average time complexity and linear memory complexity. However, hash maps often suffer from severe memory limitations on models with immense state spaces. To address this, we propose using prefix trees to store states for large, highly concurrent models (particularly CRNs) for memory savings. We present theoretical analyses and benchmarks demonstrating the favorability of prefix trees over hash maps for very large state spaces. Additionally, we propose using a Bounded Model Checking (BMC) pre-processing step to impose a variable ordering to further improve memory usage along with preliminary evaluations suggesting its effectiveness. We remark that while our work is motivated primarily by the challenges posed by CRNs, it is generalizable to all CTMC models.},
	archiveprefix = {arXiv},
	author = {Taylor, Landon and Jeppson, Joshua and Irfan, Ahmed and Buecherl, Lukas and Myers, Chris and Zhang, Zhen},
	doi = {10.48550/arXiv.2512.17892},
	eprint = {2512.17892},
	file = {/home/landon/Zotero/storage/E83SZ48X/Taylor et al. - 2025 - Prefix Trees Improve Memory Consumption in Large-Scale Continuous-Time Stochastic Models.pdf;/home/landon/Zotero/storage/S55BMBD8/2512.html},
	month = {December},
	number = {arXiv:2512.17892},
	primaryclass = {cs},
	publisher = {arXiv},
	title = {Prefix {{Trees Improve Memory Consumption}} in {{Large-Scale Continuous-Time Stochastic Models}}},
	urldate = {2026-01-26},
	year = {2025}
}
					

2025 Reasoning about Rare-Event Reachability in Stochastic Vector Addition Systems via Affine Vector Spaces arXiv preprint Joshua Jeppson, Landon Taylor, Bingqing Hu, and Zhen Zhang

@misc{Jeppson_Reasoning_2025,
	abstract = {Rare events in Stochastic Vector Addition System (VAS) are of significant interest because, while extremely unlikely, they may represent undesirable behavior that can have adverse effects. Their low probabilities and potentially extremely large state spaces challenge existing probabilistic model checking and stochastic rare-event simulation techniques. In particular, in Chemical Reaction Networks (CRNs), a chemical kinetic language often represented as VAS, rare event effects may be pathological. We present two novel heuristics for priority-first partial state space expansion and trace generation tuned to the transient analysis of rare-event probability in VAS: Iterative Subspace Reduction (ISR) and Single Distance Priority (SDP). Both methods construct a closed vector space containing all solution states. SDP then simply prioritizes shorter distances to this ``solution space'', while ISR constructs a set of nested subspaces, where short and highly-probable satisfying traces are likely to pass through in sequence. The resulting partial state graph from each method contains likely traces to rare-event states, allowing efficient probabilistic model checking to compute a lower-bound probability of a rare event of interest. These methods are deterministic, fast, and demonstrate marked performance on challenging CRN models.},
	archiveprefix = {arXiv},
	author = {Jeppson, Joshua and Taylor, Landon and Hu, Bingqing and Zhang, Zhen},
	doi = {10.48550/arXiv.2507.17711},
	eprint = {2507.17711},
	file = {/home/landon/Zotero/storage/TKK9CG8F/Jeppson et al. - 2025 - Reasoning about Rare-Event Reachability in Stochastic Vector Addition Systems via Affine Vector Spac.pdf;/home/landon/Zotero/storage/GFTDVYSG/2507.html},
	month = {July},
	number = {arXiv:2507.17711},
	primaryclass = {cs},
	publisher = {arXiv},
	title = {Reasoning about {{Rare-Event Reachability}} in {{Stochastic Vector Addition Systems}} via {{Affine Vector Spaces}}},
	urldate = {2025-12-09},
	year = {2025}
}
					

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

@inproceedings{Andriushchenko_Tools_2025,
	abstract = {The analysis of formal models that include quantitative aspects such as timing or probabilistic choices is performed by quantitative verification tools. Broad and mature tool support is available for computing basic properties such as expected rewards on basic models such as Markov chains. Previous editions of QComp, the comparison of tools for the analysis of quantitative formal models, focused on this setting. Many application scenarios, however, require more advanced property types such as LTL and parameter synthesis queries as well as advanced models like stochastic games and partially observable MDPs. For these, tool support is in its infancy today. This paper presents the outcomes of QComp 2023: a survey of the state of the art in quantitative verification tool support for advanced property types and models. With tools ranging from first research prototypes to well-supported integrations into established toolsets, this report highlights today's active areas and tomorrow's challenges in tool-focused research for quantitative verification.},
	address = {Cham},
	author = {Andriushchenko, Roman and Bork, Alexander and Budde, Carlos E. and {\v C}e{\v s}ka, Milan and Grover, Kush and Hahn, Ernst Moritz and Hartmanns, Arnd and Israelsen, Bryant and Jansen, Nils and Jeppson, Joshua and Junges, Sebastian and K{\"o}hl, Maximilian A. and K{\"o}nighofer, Bettina and K{\v r}et{\'i}nsk{\'y}, Jan and Meggendorfer, Tobias and Parker, David and Pranger, Stefan and Quatmann, Tim and Ruijters, Enno and Taylor, Landon and Volk, Matthias and Weininger, Maximilian and Zhang, Zhen},
	booktitle = {{{TOOLympics Challenge}} 2023},
	doi = {10.1007/978-3-031-67695-6_4},
	editor = {Beyer, Dirk and Hartmanns, Arnd and Kordon, Fabrice},
	isbn = {978-3-031-67695-6},
	langid = {english},
	pages = {90--146},
	publisher = {Springer Nature Switzerland},
	title = {Tools at~the~{{Frontiers}} of~{{Quantitative Verification}}},
	year = {2025}
}
					

2024 Rare-Event Guided Analysis of Infinite-State Chemical Reaction Networks Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems Mohammad Ahmadi, Lukas Buecherl, Chris J. Myers, Zhen Zhang, Chris Winstead, and Hao Zheng

@inproceedings{Ahmadi_RareEventGuidedAnalysis_2024,
	address = {Cham},
	author = {Ahmadi, Mohammad and Buecherl, Lukas and Myers, Chris J. and Zhang, Zhen and Winstead, Chris and Zheng, Hao},
	booktitle = {Quantitative {{Evaluation}} of {{Systems}} and {{Formal Modeling}} and {{Analysis}} of {{Timed Systems}}},
	doi = {10.1007/978-3-031-68416-6_12},
	editor = {Hillston, Jane and Soudjani, Sadegh and Waga, Masaki},
	file = {/home/landon/Zotero/storage/4ISLNL8P/Ahmadi et al. - 2024 - Rare-Event Guided Analysis of Infinite-State Chemical Reaction Networks.pdf},
	isbn = {978-3-031-68415-9 978-3-031-68416-6},
	langid = {english},
	pages = {196--212},
	publisher = {Springer Nature Switzerland},
	title = {Rare-{{Event Guided Analysis}} of {{Infinite-State Chemical Reaction Networks}}},
	urldate = {2024-12-17},
	volume = {14996},
	year = {2024}
}
					

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

@inproceedings{Taylor_CycleCommuteRareEvent_2023,
	author = {Taylor, Landon and Israelsen, Bryant and Zhang, Zhen},
	booktitle = {Formal {{Methods}} in {{Computer-Aided Design}}},
	copyright = {http://creativecommons.org/licenses/by/4.0/},
	doi = {10.34727/2023/isbn.978-3-85448-060-0_37},
	file = {/home/landon/Zotero/storage/HC9LIZCC/Taylor2023_Cycle_and_Commute.pdf},
	isbn = {978-3-85448-060-0},
	langid = {english},
	month = {October},
	pages = {284--293},
	publisher = {TU Wien Academic Press},
	shorttitle = {Cycle and {{Commute}}},
	title = {Cycle and {{Commute}}: {{Rare-Event Probability Verification}} for {{Chemical Reaction Networks}}},
	urldate = {2023-11-08},
	year = {2023}
}
					

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

@inproceedings{Israelsen_EfficientTraceGeneration_2023,
	abstract = {Rare events are known to potentially cause pathological behavior in biochemical reaction systems. It is important to understand the cause. However, rare events are challenging to analyze due to their extremely low observability. This paper presents a fully automated approach that rapidly generates a large number of execution traces guaranteed to reach user-specified rare-event states for Chemical Reaction Network (CRN) models. It is enabled by a unique combination of a multilayered and service-oriented CRN formal modeling approach, a dependency graph method to aid the shortest rare-event trace generation, and randomized compositional testing. The resulting prototype tool shows marked improvement over stochastic simulation and probabilistic model checking and it offers insights into a CRN.},
	address = {Cham},
	author = {Israelsen, Bryant and Taylor, Landon and Zhang, Zhen},
	booktitle = {Model {{Checking Software}}},
	copyright = {All rights reserved},
	doi = {10.1007/978-3-031-32157-3_5},
	editor = {Caltais, Georgiana and Schilling, Christian},
	file = {/home/landon/Zotero/storage/KVTDH4D9/Israelsen et al. - 2023 - Efficient Trace Generation for Rare-Event Analysis.pdf},
	isbn = {978-3-031-32156-6 978-3-031-32157-3},
	langid = {english},
	month = {May},
	pages = {83--102},
	publisher = {Springer Nature Switzerland},
	title = {Efficient {{Trace Generation}} for {{Rare-Event Analysis}} in {{Chemical Reaction Networks}}},
	urldate = {2023-11-08},
	volume = {13872},
	year = {2023}
}
					

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

@inproceedings{Jeppson_STAMINAModernizingInfiniteState_2023,
	abstract = {Improving the scalability of probabilistic model checking (PMC) tools is crucial to the verification of real-world system designs. The Stamina infinite-state PMC tool achieves scalability by iteratively constructing a partial state space for an unbounded continuous-time Markov chain model, where a majority of the probability mass resides. It then performs time-bounded transient PMC. It can efficiently produce an accurate probability bound to the property under verification. We present a new software architecture design and the C++ implementation of the Stamina 2.0 algorithm, integrated with the Storm model checker. This open-source Stamina implementation offers a high degree of modularity and provides significant optimizations to the Stamina 2.0 algorithm. Performance improvements are demonstrated on multiple challenging benchmark examples, including hazard analysis of infinite-state combinational genetic circuits, over the previous Stamina implementation. Additionally, its design allows for future customizations and optimizations to the Stamina algorithm.},
	address = {Cham},
	author = {Jeppson, Joshua and Volk, Matthias and Israelsen, Bryant and Roberts, Riley and Williams, Andrew and Buecherl, Lukas and Myers, Chris J. and Zheng, Hao and Winstead, Chris and Zhang, Zhen},
	booktitle = {Quantitative {{Evaluation}} of {{Systems}}},
	doi = {10.1007/978-3-031-43835-6_7},
	editor = {Jansen, Nils and Tribastone, Mirco},
	file = {/home/landon/Zotero/storage/B5UC9GC4/Jeppson et al. - 2023 - STAMINA in C++ Modernizing an Infinite-State Probabilistic Model Checker.pdf;/home/landon/Zotero/storage/PKWKL3P8/Jeppson et al. - 2023 - STAMINA in C++ Modernizing an Infinite-State Probabilistic Model Checker.pdf},
	isbn = {978-3-031-43835-6},
	langid = {english},
	month = {September},
	pages = {101--109},
	publisher = {Springer Nature Switzerland},
	series = {Lecture {{Notes}} in {{Computer Science}}},
	shorttitle = {{{STAMINA}} in~{{C}}++},
	title = {{{STAMINA}} in~{{C}}++: {{Modernizing}} an~{{Infinite-State Probabilistic Model Checker}}},
	year = {2023}
}
					

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

@inproceedings{Taylor_Scaling_2022,
	abstract = {As an efficient interconnection network, Network-on-Chip (NoC) provides significant flexibility for increasingly prevalent many-core systems. It is desirable to deploy fault-tolerance in a dependable safetycritical NoC design. However, this process can easily introduce deeply buried flaws that traditional simulation-based NoC design approaches may miss. This paper presents a case study on applying scalable formal verification that detects, corrects, and proves livelock in a dependable fault-tolerant NoC using the IVy verification tool. We formally verify correctness at the routing algorithm level. We first present livelock verification using refutation-based simulation scaled to a 15-by-15 twodimensional NoC. We then present a novel zone-based approach to livelock verification in which finite coordinate-based routing conditions are abstracted as positional zones relative to a packet's destination. This abstraction allows us to detect and remove livelock patterns on an arbitrarily large network. The resultant improved routing algorithm is free of livelock and maintains a high level of fault tolerance.},
	address = {Cham},
	author = {Taylor, Landon and Zhang, Zhen},
	booktitle = {Verification, {{Model Checking}}, and {{Abstract Interpretation}}},
	copyright = {All rights reserved},
	doi = {10.1007/978-3-030-94583-1_19},
	editor = {Finkbeiner, Bernd and Wies, Thomas},
	file = {/home/landon/Zotero/storage/9WPCGC3T/Taylor and Zhang - 2022 - Scaling Up Livelock Verification for Network-on-Ch.pdf},
	isbn = {978-3-030-94582-4 978-3-030-94583-1},
	langid = {english},
	pages = {378--399},
	publisher = {Springer International Publishing},
	title = {Scaling {{Up Livelock Verification}} for {{Network-on-Chip Routing Algorithms}}},
	urldate = {2023-11-08},
	volume = {13182},
	year = {2022}
}
					

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

@inproceedings{Roberts_STAMINA_2022,
	abstract = {Stochastic model checking (SMC) is a formal verification technique for the analysis of systems with probabilistic behavior. Scalability has been a major limiting factor for SMC tools to analyze real-world systems with large or infinite state spaces. The infinite-state Continuous-time Markov Chain (CTMC) model checker, STAMINA, tackles this problem by selectively exploring only a portion of a model's state space, where a majority of the probability mass resides, to efficiently give an accurate probability bound to properties under verification. In this paper, we present two major improvements to STAMINA, namely, a method of calculating and distributing estimated state reachability probabilities that improves state space truncation efficiency and combination of the previous two CTMC analyses into one for generating the probability bound. Demonstration of the improvements on several benchmark examples, including hazard analysis of infinite-state combinational genetic circuits, yield significant savings in both run-time and state space size (and hence memory), compared to both the previous version of STAMINA and the infinite-state CTMC model checker INFAMY. The improved STAMINA demonstrates significant scalability to allow for the verification of complex real-world infinite-state systems.},
	address = {Cham},
	author = {Roberts, Riley and Neupane, Thakur and Buecherl, Lukas and Myers, Chris J. and Zhang, Zhen},
	booktitle = {Verification, {{Model Checking}}, and {{Abstract Interpretation}}},
	doi = {10.1007/978-3-030-94583-1_16},
	editor = {Finkbeiner, Bernd and Wies, Thomas},
	file = {/home/landon/Zotero/storage/UCRVVG32/Roberts2022_STAMINA_2.pdf},
	isbn = {978-3-030-94583-1},
	langid = {english},
	pages = {319--331},
	publisher = {Springer International Publishing},
	series = {Lecture {{Notes}} in {{Computer Science}}},
	shorttitle = {{{STAMINA}} 2.0},
	title = {{{STAMINA}} 2.0: {{Improving Scalability}} of~{{Infinite-State Stochastic Model Checking}}},
	year = {2022}
}
					

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

@article{Cotner_Computational_2021,
	author = {Cotner, Michael and Zhan, Jixun and Zhang, Zhen},
	doi = {10.1021/acssynbio.1c00163},
	file = {/home/landon/Zotero/storage/8RYSLPDW/Cotner et al. - 2021 - A Computational Metabolic Model for Engineered Production of Resveratrol in Escherichia coli.pdf},
	journal = {ACS Synthetic Biology},
	month = {August},
	number = {8},
	pages = {1992--2001},
	publisher = {American Chemical Society},
	title = {A {{Computational Metabolic Model}} for {{Engineered Production}} of {{Resveratrol}} in {{Escherichia}} Coli},
	urldate = {2023-02-22},
	volume = {10},
	year = {2021}
}
					

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

@incollection{Budde_Correctness_2021,
	address = {Cham},
	author = {Budde, Carlos E. and Hartmanns, Arnd and Klauck, Michaela and K{\v r}et{\'i}nsk{\'y}, Jan and Parker, David and Quatmann, Tim and Turrini, Andrea and Zhang, Zhen},
	booktitle = {Leveraging {{Applications}} of {{Formal Methods}}, {{Verification}} and {{Validation}}: {{Tools}} and {{Trends}}},
	doi = {10.1007/978-3-030-83723-5_15},
	editor = {Margaria, Tiziana and Steffen, Bernhard},
	file = {/home/landon/Zotero/storage/DDW2SZCB/Budde2021_On_Correctness,_Precision,_and_Performance_in_Quantitative_Verification.pdf},
	isbn = {978-3-030-83722-8 978-3-030-83723-5},
	langid = {english},
	pages = {216--241},
	publisher = {Springer International Publishing},
	shorttitle = {On {{Correctness}}, {{Precision}}, and {{Performance}} in {{Quantitative Verification}}},
	title = {On {{Correctness}}, {{Precision}}, and {{Performance}} in {{Quantitative Verification}}: {{QComp}} 2020 {{Competition Report}}},
	urldate = {2022-06-07},
	volume = {12479},
	year = {2021}
}
					

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

@inproceedings{Roberts_Probabilistic_2021,
	address = {Cham},
	author = {Roberts, Riley and Lewis, Benjamin and Hartmanns, Arnd and Basu, Prabal and Roy, Sanghamitra and Chakraborty, Koushik and Zhang, Zhen},
	booktitle = {Formal {{Methods}} for {{Industrial Critical Systems}}},
	doi = {10.1007/978-3-030-85248-1_16},
	editor = {Lluch Lafuente, Alberto and Mavridou, Anastasia},
	file = {/home/landon/Zotero/storage/KFA5K2FI/Roberts2021_Probabilistic_Verification_for_Reliability_of_a_Two-by-Two_Network-on-Chip.pdf},
	isbn = {978-3-030-85248-1},
	langid = {english},
	pages = {232--248},
	publisher = {Springer International Publishing},
	series = {Lecture {{Notes}} in {{Computer Science}}},
	title = {Probabilistic {{Verification}} for {{Reliability}} of a {{Two-by-Two Network-on-Chip System}}},
	year = {2021}
}
					

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

@inproceedings{Smith_Refutationbased_2021,
	author = {Smith, Joshua and Allan, Jarom and Swaminathan, Viswanathan and Zhang, Zhen},
	booktitle = {Formal {{Methods}} for {{ML-Enabled Autonomous Systems}} ({{FoMLAS}})},
	month = {July},
	title = {Refutation-Based Adversarial Robustness Verification of Deep Neural Networks},
	year = {2021}
}
					

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

@article{Buecherl_StochasticHazardAnalysis_2021,
	abstract = {In synthetic biology, combinational circuits are used to program cells for various new applications like biosensors, drug delivery systems, and biofuels. Similar to asynchronous electronic circuits, some combinational genetic circuits may show unwanted switching variations (glitches) caused by multiple input changes. Depending on the biological circuit, glitches can cause irreversible effects and jeopardize the circuit's functionality. This paper presents a stochastic analysis to predict glitch propensities for three implementations of a genetic circuit with known glitching behavior. The analysis uses STochastic Approximate Model-checker for INfinite-state Analysis (STAMINA), a tool for stochastic verification. The STAMINA results were validated by comparison to stochastic simulation in iBioSim resulting in further improvements of STAMINA. This paper demonstrates that stochastic verification can be utilized by genetic designers to evaluate design choices and input restrictions to achieve a desired reliability of operation.},
	author = {Buecherl, Lukas and Roberts, Riley and Fontanarrosa, Pedro and Thomas, Payton J. and Mante, Jeanet and Zhang, Zhen and Myers, Chris J.},
	doi = {10.1021/acssynbio.1c00159},
	file = {/home/landon/Zotero/storage/5H8DPLQ8/Buecherl2021_Stochastic_Hazard_Analysis_of_Genetic_Circuits_in_iBioSim_and_STAMINA.pdf;/home/landon/Zotero/storage/YC65BH6V/Buecherl2021_Stochastic_Hazard_Analysis_of_Genetic_Circuits_in_iBioSim_and_STAMINA.pdf},
	journal = {ACS Synthetic Biology},
	month = {October},
	number = {10},
	pages = {2532--2540},
	pmid = {https://pubmed.ncbi.nlm.nih.gov/34606710},
	publisher = {American Chemical Society},
	title = {Stochastic {{Hazard Analysis}} of {{Genetic Circuits}} in {{iBioSim}} and {{STAMINA}}},
	urldate = {2023-11-08},
	volume = {10},
	year = {2021}
}
					

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

@article{Bradshaw_Abstract_2020,
	author = {Bradshaw, Kelsey and Vargis, Elizabeth and Zang, Zhen},
	issn = {1552-5783},
	journal = {Investigative Ophthalmology \& Visual Science},
	month = {June},
	number = {7},
	pages = {5404},
	title = {({{Abstract}}) {{A}} Computational Model of the Effect of {{VEGF}} Production in Wet Age-Related Macular Degeneration on Neovascularization},
	volume = {61},
	year = {2020}
}
					

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

@inproceedings{Cotner_Abstract_2020,
	author = {Cotner, Michael and Zhang, Zhen and Zhan, Jixun},
	booktitle = {International Workshop on Bio-Design Automation ({{IWBDA}})},
	file = {/home/landon/Zotero/storage/KSACAPAW/Cotner2020_(Abstract)_Enhanced_microbial_production_of_valuable_natural_products_through.pdf},
	pages = {82--83},
	title = {({{Abstract}}) {{Enhanced}} Microbial Production of Valuable Natural Products through Computational Metabolic Models},
	year = {2020}
}
					

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

@inproceedings{Bucherl_Abstract_2020,
	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 ({{IWBDA}})},
	file = {/home/landon/Zotero/storage/KH2PRQIA/Bücherl2020_(Abstract)_Genetic_circuit_hazard_analysis_using_STAMINA.pdf},
	month = {August},
	pages = {39--40},
	title = {({{Abstract}}) {{Genetic}} Circuit Hazard Analysis Using {{STAMINA}}},
	year = {2020}
}
					

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

@inproceedings{Gundi_EFFORT_2020,
	author = {Gundi, Noel Daniel and Shabanian, Tahmoures and Basu, Prabal and Pandey, Pramesh and Roy, Sanghamitra and Chakraborty, Koushik and Zhang, Zhen},
	booktitle = {2020 25th {{Asia}} and {{South Pacific Design Automation Conference}} ({{ASP-DAC}})},
	doi = {10.1109/ASP-DAC47756.2020.9045479},
	file = {/home/landon/Zotero/storage/5G392697/Gundi2020_EFFORT.pdf},
	issn = {2153-697X},
	month = {January},
	pages = {241--246},
	shorttitle = {{{EFFORT}}},
	title = {{{EFFORT}}: {{Enhancing Energy Efficiency}} and {{Error Resilience}} of a {{Near-Threshold Tensor Processing Unit}}},
	year = {2020}
}
					

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{Neupane_Approximation_2019,
	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}}},
	doi = {10.1007/978-3-030-17297-8_12},
	editor = {Li{\`o}, Pietro and Zuliani, Paolo},
	file = {/home/landon/Zotero/storage/GFLLLDL6/Neupane2019_Approximation_Techniques_for_Stochastic_Analysis_of_Biological_Systems.pdf},
	isbn = {978-3-030-17296-1 978-3-030-17297-8},
	langid = {english},
	pages = {327--348},
	publisher = {Springer International Publishing},
	title = {Approximation {{Techniques}} for {{Stochastic Analysis}} of {{Biological Systems}}},
	urldate = {2022-04-05},
	volume = {30},
	year = {2019}
}
					

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{Watanabe_IBioSim_2019,
	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},
	file = {/home/landon/Zotero/storage/ADZIPZ7Y/Watanabe et al. - 2019 - iBioSim 3 A Tool for Model-Based Genetic Circuit Design.pdf},
	journal = {ACS Synthetic Biology},
	month = {July},
	number = {7},
	pages = {1560--1563},
	publisher = {American Chemical Society},
	shorttitle = {{{iBioSim}} 3},
	title = {{{iBioSim}} 3: {{A Tool}} for {{Model-Based Genetic Circuit Design}}},
	urldate = {2023-02-22},
	volume = {8},
	year = {2019}
}
					

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{ImprovingDeepNeural,
	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 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

@inproceedings{Lewis_Probabilistic_2019,
	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}}},
	doi = {10.1007/978-3-030-27008-7_7},
	editor = {Larsen, Kim Guldstrand and Willemse, Tim},
	file = {/home/landon/Zotero/storage/YMKD57YW/Lewis2019_Probabilistic_Verification_for_Reliable_Network-on-Chip_System_Design.pdf},
	isbn = {978-3-030-27007-0 978-3-030-27008-7},
	langid = {english},
	pages = {110--126},
	publisher = {Springer International Publishing},
	title = {Probabilistic {{Verification}} for {{Reliable Network-on-Chip System Design}}},
	urldate = {2022-04-05},
	volume = {11687},
	year = {2019}
}
					

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

@inproceedings{Neupane_STAMINA_2019,
	address = {Cham},
	author = {Neupane, Thakur and Myers, Chris J. and Madsen, Curtis and Zheng, Hao and Zhang, Zhen},
	booktitle = {Computer {{Aided Verification}}},
	doi = {10.1007/978-3-030-25540-4_31},
	editor = {Dillig, Isil and Tasiran, Serdar},
	file = {/home/landon/Zotero/storage/EAKGB9M9/Neupane2019_STAMINA.pdf},
	isbn = {978-3-030-25539-8 978-3-030-25540-4},
	langid = {english},
	pages = {540--549},
	publisher = {Springer International Publishing},
	shorttitle = {{{STAMINA}}},
	title = {{{STAMINA}}: {{STochastic Approximate Model-Checker}} for {{INfinite-State Analysis}}},
	urldate = {2022-04-05},
	volume = {11561},
	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, 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

@article{Madsen_Synthetic_2019,
	author = {Madsen, Curtis and Moreno, Angel Go{\~n}i 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},
	file = {/home/landon/Zotero/storage/IHBHLKHT/Madsen2019_Synthetic_Biology_Open_Language_(SBOL)_Version_2.pdf},
	issn = {1613-4516},
	journal = {Journal of Integrative Bioinformatics},
	langid = {english},
	month = {June},
	number = {2},
	publisher = {De Gruyter},
	title = {Synthetic {{Biology Open Language}} ({{SBOL}}) {{Version}} 2.3},
	urldate = {2023-03-06},
	volume = {16},
	year = {2019}
}
					

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

@article{Cox_Synthetic_2018,
	author = {Cox, Robert Sidney and Madsen, Curtis and McLaughlin, James Alastair and Nguyen, Tramy and Roehner, Nicholas and Bartley, Bryan and Beal, Jacob and Bissell, Michael and Choi, Kiri and Clancy, Kevin and Gr{\"u}nberg, Raik and Macklin, Chris and Misirli, Goksel and Oberortner, Ernst and Pocock, Matthew and Samineni, Meher and Zhang, Michael and Zhang, Zhen and Zundel, Zach and Gennari, John H. and Myers, Chris and Sauro, Herbert and Wipat, Anil},
	doi = {10.1515/jib-2018-0001},
	file = {/home/landon/Zotero/storage/MM2I24NG/Cox2018_Synthetic_Biology_Open_Language_(SBOL)_Version_2.pdf},
	issn = {1613-4516},
	journal = {Journal of Integrative Bioinformatics},
	langid = {english},
	month = {March},
	number = {1},
	publisher = {De Gruyter},
	title = {Synthetic {{Biology Open Language}} ({{SBOL}}) {{Version}} 2.2.0},
	urldate = {2023-03-06},
	volume = {15},
	year = {2018}
}
					

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{Zundel_Validator_2017,
	author = {Zundel, Zach and Samineni, Meher and Zhang, Zhen and Myers, Chris J.},
	doi = {10.1021/acssynbio.6b00277},
	file = {/home/landon/Zotero/storage/CPHFU99A/Zundel et al. - 2017 - A Validator and Converter for the Synthetic Biology Open Language.pdf},
	journal = {ACS Synthetic Biology},
	month = {July},
	number = {7},
	pages = {1161--1168},
	publisher = {American Chemical Society},
	title = {A {{Validator}} and {{Converter}} for the {{Synthetic Biology Open Language}}},
	urldate = {2023-02-22},
	volume = {6},
	year = {2017}
}
					

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{Zhang_Improved_2016,
	author = {Zhang, Zhen and Serwe, Wendelin and Wu, Jian and Yoneda, Tomohiro and Zheng, Hao and Myers, Chris},
	doi = {10.1016/j.scico.2016.01.002},
	file = {/home/landon/Zotero/storage/ERQ4GBSW/Zhang2016_An_improved_fault-tolerant_routing_algorithm_for_a_Network-on-Chip_derived_with.pdf},
	issn = {0167-6423},
	journal = {Science of Computer Programming},
	langid = {english},
	month = {March},
	pages = {24--39},
	series = {Formal {{Methods}} for {{Industrial Critical Systems}} ({{FMICS}}'2014)},
	title = {An Improved Fault-Tolerant Routing Algorithm for a {{Network-on-Chip}} Derived with Formal Analysis},
	urldate = {2021-03-05},
	volume = {118},
	year = {2016}
}
					

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

@article{Roehner_Sharing_2016,
	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},
	file = {/home/landon/Zotero/storage/UWRFB52G/Roehner et al. - 2016 - Sharing Structure and Function in Biological Design with SBOL 2.0.pdf},
	journal = {ACS Synthetic Biology},
	month = {June},
	number = {6},
	pages = {498--506},
	publisher = {American Chemical Society},
	title = {Sharing {{Structure}} and {{Function}} in {{Biological Design}} with {{SBOL}} 2.0},
	urldate = {2023-03-06},
	volume = {5},
	year = {2016}
}
					

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

@article{Zheng_Compositional_2015,
	author = {Zheng, Hao and Zhang, Zhen and Myers, Chris J. and Rodriguez, Emmanuel and Zhang, Yingying},
	doi = {10.1109/TC.2014.2329701},
	file = {/home/landon/Zotero/storage/54KQYDR6/Zheng2015_Compositional_Model_Checking_of_Concurrent_Systems.pdf},
	issn = {1557-9956},
	journal = {IEEE Transactions on Computers},
	month = {June},
	number = {6},
	pages = {1607--1621},
	title = {Compositional {{Model Checking}} of {{Concurrent Systems}}},
	volume = {64},
	year = {2015}
}
					

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

@incollection{Madsen_Efficient_2015,
	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},
	langid = {english},
	pages = {217--257},
	publisher = {Springer},
	series = {Methods in {{Molecular Biology}}},
	title = {Efficient {{Analysis Methods}} in {{Synthetic Biology}}},
	urldate = {2023-02-22},
	year = {2015}
}
					

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{Roehner_Generating_2015,
	author = {Roehner, Nicholas and Zhang, Zhen and Nguyen, Tramy and Myers, Chris J.},
	doi = {10.1021/sb5003289},
	file = {/home/landon/Zotero/storage/LYVJAFWF/Roehner et al. - 2015 - Generating Systems Biology Markup Language Models from the Synthetic Biology Open Language.pdf},
	journal = {ACS Synthetic Biology},
	month = {August},
	number = {8},
	pages = {873--879},
	publisher = {American Chemical Society},
	title = {Generating {{Systems Biology Markup Language Models}} from the {{Synthetic Biology Open Language}}},
	urldate = {2023-02-22},
	volume = {4},
	year = {2015}
}
					

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

@article{Zhang_LibSBOLj_2015,
	author = {Zhang, Zhen and Nguyen, Tramy and Roehner, Nicholas and Misirli, G{\"o}ksel and Pocock, Matthew and Oberortner, Ernst and Samineni, Meher and Zundel, Zach and Beal, Jacob and Clancy, Kevin and Wipat, Anil and Myers, Chris J.},
	doi = {10.1109/LLS.2016.2546546},
	file = {/home/landon/Zotero/storage/XZY54GU5/Zhang2015_libSBOLj_2.pdf},
	issn = {2332-7685},
	journal = {IEEE Life Sciences Letters},
	month = {December},
	number = {4},
	pages = {34--37},
	shorttitle = {{{libSBOLj}} 2.0},
	title = {{{libSBOLj}} 2.0: {{A Java Library}} to {{Support SBOL}} 2.0},
	volume = {1},
	year = {2015}
}
					

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

@article{Bartley_Synthetic_2015,
	author = {Bartley, Bryan and Beal, Jacob and Clancy, Kevin and Misirli, Goksel and Roehner, Nicholas and Oberortner, Ernst and Pocock, Matthew and Bissell, Michael and Madsen, Curtis and Nguyen, Tramy and Zhang, Zhen and Gennari, John H. and Myers, Chris and Wipat, Anil and Sauro, Herbert},
	doi = {10.1515/jib-2015-272},
	file = {/home/landon/Zotero/storage/DXTSAMNK/Bartley2015_Synthetic_Biology_Open_Language_(SBOL)_Version_2.pdf},
	issn = {1613-4516},
	journal = {Journal of Integrative Bioinformatics},
	langid = {english},
	month = {June},
	number = {2},
	pages = {902--991},
	publisher = {De Gruyter},
	title = {Synthetic {{Biology Open Language}} ({{SBOL}}) {{Version}} 2.0.0},
	urldate = {2023-03-06},
	volume = {12},
	year = {2015}
}
					

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{Zhang_Formal_2014,
	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}}},
	doi = {10.1007/978-3-319-10702-8_4},
	editor = {Lang, Fr{\'e}d{\'e}ric and Flammini, Francesco},
	file = {/home/landon/Zotero/storage/2K63JJJP/Zhang2014_Formal_Analysis_of_a_Fault-Tolerant_Routing_Algorithm_for_a_Network-on-Chip.pdf},
	isbn = {978-3-319-10702-8},
	langid = {english},
	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 ACM Journal on Emerging Technologies in Computing Systems Curtis Madsen, Zhen Zhang, Nicholas Roehner, Chris Winstead, and Chris Myers

@article{Madsen_Stochastic_2014,
	author = {Madsen, Curtis and Zhang, Zhen and Roehner, Nicholas and Winstead, Chris and Myers, Chris},
	doi = {10.1145/2644817},
	file = {/home/landon/Zotero/storage/JASBMXSX/Madsen et al. - 2014 - Stochastic Model Checking of Genetic Circuits.pdf},
	issn = {1550-4832, 1550-4840},
	journal = {ACM Journal on Emerging Technologies in Computing Systems},
	langid = {english},
	month = {December},
	number = {3},
	pages = {1--21},
	title = {Stochastic {{Model Checking}} of {{Genetic Circuits}}},
	urldate = {2022-04-05},
	volume = {11},
	year = {2014}
}
					

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

@inproceedings{Madsen_Utilizing_2012,
	author = {Madsen, Curtis and Myers, Chris J. and Roehner, Nicholas and Winstead, Chris and Zhang, Zhen},
	booktitle = {2012 {{IEEE Symposium}} on {{Computational Intelligence}} in {{Bioinformatics}} and {{Computational Biology}} ({{CIBCB}})},
	doi = {10.1109/CIBCB.2012.6217255},
	file = {/home/landon/Zotero/storage/5TDDFL5S/Madsen et al. - 2012 - Utilizing stochastic model checking to analyze genetic circuits.pdf},
	month = {May},
	pages = {379--386},
	title = {Utilizing Stochastic Model Checking to Analyze Genetic Circuits},
	year = {2012}
}
					

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

@inproceedings{Wu_FaultTolerant_2011,
	author = {Wu, Jian and Zhang, Zhen and Myers, Chris},
	booktitle = {Virtual Worldwide Forum for {{PhD}} Researchers in Electronic Design Automation},
	file = {/home/landon/Zotero/storage/U68EVGLY/Wu2011_A_Fault-Tolerant_Routing_Algorithm_for_a_Network-on-Chip_Using_a_Link_Fault.pdf},
	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{Zhang_Performance_2008,
	author = {Zhang, Z. and Garside, J.},
	booktitle = {20th {{UK}} Asynchronous Forum},
	file = {/home/landon/Zotero/storage/QWB9GT27/Zhang2008_Performance_analysis_of_two_synchronizers.pdf},
	title = {Performance Analysis of Two Synchronizers},
	year = {2008}
}
					

1975 Effect of Chloroquine on Cultured Fibroblasts: Release of Lysosomal Hydrolases and Inhibition of Their Uptake Biochemical and Biophysical Research Communications U. N. Wiesmann, S. DiDonato, and N. N. Herschkowitz

@article{wiesmannEffectChloroquineCultured1975,
	author = {Wiesmann, U. N. and DiDonato, S. and Herschkowitz, N. N.},
	doi = {10.1016/0006-291x(75)90506-9},
	issn = {1090-2104},
	journal = {Biochemical and Biophysical Research Communications},
	langid = {english},
	month = {October},
	number = {4},
	pages = {1338--1343},
	pmid = {4},
	shorttitle = {Effect of Chloroquine on Cultured Fibroblasts},
	title = {Effect of Chloroquine on Cultured Fibroblasts: Release of Lysosomal Hydrolases and Inhibition of Their Uptake},
	volume = {66},
	year = {1975}
}
					

1975 Formation of Transient Complexes in the Glutamate Dehydrogenase Catalyzed Reaction Biochemistry T. Sanner

@article{sannerFormationTransientComplexes1975,
	abstract = {The reaction of glutamate dehydrogenase and glutamate (gl) with NAD+ and NADP+ has been studied with stopped-flow techniques. The enzyme was in all experiments present in excess of the coenzyme. The results indicate that the ternary complex (E-NAD(P)H-kg) is present as an intermediate in the formation of the stable complex (E-NAD(P)H-gl). The identification of the complexes is based on their absorption spectra. The binding of the coenzyme to (E-gl) is the rate-limiting step in the formation of (E-NAD(P)H-kg) while the dissociation of alpha-ketoglutarate (kg) from this complex is the rate-limiting step in the formation of (E-NAD(P)H-gl). The Km for glutamate was 20-25 mM in the first reaction and 3 mM in the formation of the stable complex. The Km values were independent of the coenzyme. The reaction rates with NAD+ were approximately 50\% greater than those with NADP+. Furthermore, high glutamate concentration inhibited the formation of (E-NADH-kg) while no substrate inhibition was found with NADP+ as coenzyme. ADP enhanced while GTP reduced the rate of (E-NAD(P)H-gl) formation. The rate of formation of (E-NAD(P)H-kg) was inhibited by ADP, while it increased at high glutamate concentration when small amounts of GTP were added. The results show that the higher activity found with NAD+ compared to NADP+ under steady-state assay conditions do not necessarily involve binding of NAD+ to the ADP activating site of the enzyme. Moreover, the substrate inhibition found at high glutamate concentration under steady-state assay condition is not due to the formation of (E-NAD(P)H-gl) as this complex is formed with Km of 3 mM glutamate, and the substrate inhibition is only significant at 20-30 times this concentration.},
	author = {Sanner, T.},
	doi = {10.1021/bi00694a011},
	issn = {0006-2960},
	journal = {Biochemistry},
	langid = {english},
	month = {November},
	number = {23},
	pages = {5094--5098},
	pmid = {39},
	title = {Formation of Transient Complexes in the Glutamate Dehydrogenase Catalyzed Reaction},
	volume = {14},
	year = {1975}
}