I have enjoyed working as a research assistant since Fall 2019. Researching formal verification has allowed me to become a more precise, cautious engineer, and I am thrilled to have the research mentorship and opportunities I do. It is exciting to participate in programs and groups that allow young engineers to participate fully in the research process, and I look forward to conducting research throughout my career.
Fall 2023 (to appear)
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, as benchmarked in previous editions of QComp, the comparison of tools for the analysis of quantitative formal models. Many application scenarios, however, require more complex models and properties, for which 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 such as LTL and parameter synthesis queries as well as advanced models like stochastic games and partially observable MDPs. With tool support 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.TOOLympics 2023
In synthetic biological systems, rare events can cause undesirable behavior leading to pathological effects. Due to their low observability, rare events are challenging to analyze using existing stochastic simulation methods. Chemical Reac- tion Networks (CRNs) are a general-purpose formal language for modeling chemical kinetics. This paper presents a fully automated approach to efficiently construct a large number of concurrent traces by expanding a sample of known traces. These traces constitute a partial state space containing only traces leading to a rare event of interest. This state space is then used to compute a lower bound for the rare event's probability. We propose a novel approach for the analysis of highly concurrent CRNs, including a CRN reaction independence analysis and an algorithm that exploits CRN concurrency to rapidly enumerate parallel traces. We then present a novel algorithm to add cycles to a partial state space to further increase the rare event's probability lower bound to its actual value. The resulting prototype tool, RAGTIMER, demonstrates improvement over stochastic simulation and probabilistic model checking.Open-Access Paper
Rare-events are known to potentially cause pathologic behavior for biochemical reactions in systems and synthetic biology. 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 multi-layered 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.View Paper
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 safety-critical 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 two-dimensional 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.View Paper
My research interests include formal verification methods like model checking, Property-Directed Reachability (IC3), counterexample generation, and automated inductive proofs. My research currently focuses on verifying properties of probabilistic models as part of the multi-university FLUENT Verification Project. I am especially interested in the verification of large-scale and synthetic biological systems. This research is currently funded by the National Science Foundation and the College of Engineering at Utah State University. My work is overseen by Zhen Zhang at Utah State University.
I would be remiss if I did not express my immense gratitude for the generous support and mentorship I've received from Zhen Zhang at Utah State University. His research advisorship has impacted me professionally and personally more than I can express, and his careful mentorship has taught me to double-check my research, defend my results, and set meaningful professional goals.