Recent Publications
Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report
TOOLympics – April 2024
Roman Andriushchenko, Alexander Bork, Carlos E. Budde, Milan Češka, 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, Zhen Zhang
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, 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.
Enhancing Property-Directed Reachability for Chemical Reaction Networks (Poster)
FMCAD Student Forum – October 2023
Landon Taylor and Zhen Zhang
Abstract. Property-Directed Reachability (PDR) is a scalable method for inductively checking reachability of system models. PDR is specialized for Boolean and integer systems, but it is currently unable to provide probability information for continuous-time systems like Chemical Reaction Networks (CRNs). This research advances PDR to bound variables in infinite-state CRNs and to estimate a target state’s reachability probability.
Cycle and Commute: Rare-Event Probability Verification for Chemical Reaction Networks
FMCAD – October 2023
Landon Taylor, Bryant Israelsen, and Zhen Zhang
Abstract. 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.
Efficient Trace Generation for Rare-Event Analysis in Chemical Reaction Networks
SPIN – April 2023
Bryant Israelsen, Landon Taylor, and Zhen Zhang
Abstract. 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.
Scaling Up Livelock Verification for Network-on-Chip Routing Algorithms
VMCAI – January 2022
Landon Taylor and Zhen Zhang
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 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.
Research Interests
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 (including synthetic biological systems) as part of the multi-university FLUENT Verification Project. I primarily research under the excellent mentorship of Zhen Zhang at Utah State University.
Acknowledgement
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.