More Like this

1. STAMINA 2.0: Improving Scalability of Infinite-State Stochastic Model Checking

   https://doi.org/https://doi.org/10.1007/978-3-030-94583-1_16  

   Roberts, R.; Neupane, T.; Buecherl, L.; Myers, C.J.; Zhang, Z. (June 2022, Lecture notes in computer science)

   Finkbeiner, B.; Wies, T. (Ed.)

   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. 

   more » « less
2. STAMINA in C++: Modernizing an Infinite-State Probabilistic Model Checker

   https://doi.org/10.1007/978-3-031-43835-6_7  

   Jeppson, Josh; Volk, Matthias; Israelsen, Bryant; Roberts, Riley; Williams, Andrew; Buecherl, Lukas; Myers, Chris J; Zheng, Hao; Winstead, Chris; Zhang, Zhen (September 2023, Lecture notes in computer science)

   Jansen, N; Tribastone, M (Ed.)

   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. 

   more » « less
3. iBioSim 3: A Tool for Model-Based Genetic Circuit Design

   https://doi.org/https://doi.org/10.1021/acssynbio.8b00078  

   Watanabe, Leandro; Nguyen, Tramy; Zhang, Michael; Zundel, Zach; Zhang, Zhen; Madsen, Curtis; Roehner, Nicholas; Myers, Chris (January 2019, ACS synthetic biology)

   The iBioSim tool has been developed to facilitate the design of genetic circuits via a model-based design strategy. This paper illustrates the new features incorporated into the tool for DNA circuit design, design analysis, and design synthesis, all of which can be used in a workflow for the systematic construction of new genetic circuits. 

   more » « less
4. Analyzing Multilevel Stochastic Circuits using Correlation Matrices

   Hoffend, Owen; Hayes, John P. (April 2022, 2022 25th International Symposium on Design and Diagnostics of Electronic Circuits & Systems (DDECS))

   Stochastic computing (SC) is a digital design paradigm that foregoes the conventional binary encoding in favor of pseudo-random bitstreams. Stochastic circuits operate on the probability values of bitstreams, and often achieve low power, low area, and fault-tolerant computation. Most SC designs rely on the input bitstreams being independent or uncorrelated to obtain the best results. However, circuits have also been proposed that exploit deliberately correlated bitstreams to improve area or accuracy. In such cases, different sub-circuits may have different correlation requirements. A major barrier to multi-layer or hierarchical stochastic circuit design has been understanding how correlation propagates while meeting the correlation requirements for all its sub-circuits. In this paper, we introduce correlation matrices and extensions to probability transfer matrix (PTM) algebra to analyze complex correlation behavior, thereby alleviating the need for computationally intensive bit-wise simulation. We apply our new correlation analysis to two multi-layer SC image processing and neural network circuits and show that it helps designers to systematically reduce correlation error. 

   more » « less
5. Functional Verification of Arithmetic Circuits: Survey of Formal Methods

   https://doi.org/10.1109/DDECS54261.2022.9770161  

   Ciesielski, Maciej; Yasin, Atif; Dasari, Jiteshri (April 2022, 25th International Symposium on Design and Diagnostics of Electronic Circuits and Systems)

   This paper gives a brief survey of current state-of-the-art techniques for formal verification of arithmetic circuits with suggestions for future work. In contrast to standard BDD or SAT-based approach that require a reference circuit it concentrates on Symbolic Computer Algebra (SCA) and related techniques that verify the circuits w.r.t. its abstract arithmetic specification. We examine the original computer algebra method; review the algebraic techniques of forward and backward rewriting; and AIG rewriting. We also propose a "hardware rewriting" method, which replaces algebraic rewriting by hardware synthe- sis of the circuit under verification appended with an inverse of the circuit, expecting it to be reduced to a redundant one. 

   more » « less