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. Verisig 2.0: Verification of Neural Network Controllers Using Taylor Model Preconditioning.

   https://doi.org/10.1007/978-3-030-81685-8_11  

   Ivanov, R. (July 2021, Computer Aided Verification (CAV))

   Silva, A. (Ed.)

   This paper presents Verisig 2.0, a verification tool for closed-loop systems with neural network (NN) controllers. We focus on NNs with tanh/sigmoid activations and develop a Taylor-model-based reachability algorithm through Taylor model preconditioning and shrink wrapping. Furthermore, we provide a parallelized implementation that allows Verisig 2.0 to efficiently handle larger NNs than existing tools can. We provide an extensive evaluation over 10 benchmarks and compare Verisig 2.0 against three state-of-the-art verification tools. We show that Verisig 2.0 is both more accurate and faster, achieving speed-ups of up to 21x and 268x against different tools, respectively. 

   more » « less
3. Aragog: Scalable Runtime Verification of Shardable Networked Systems

   Yaseen, Nofel; Arzani, Behnaz; Beckett, Ryan; Ciraci, Selim; Liu, Vincent (November 2020, 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20))

   null (Ed.)

   Network functions like firewalls, proxies, and NATs are instances of distributed systems that lie on the critical path for a substantial fraction of today's cloud applications. Unfortunately, validating these systems remains difficult due to their complex stateful, timed, and distributed behaviors. In this paper, we present the design and implementation of Aragog, a runtime verification system for distributed network functions that achieves high expressiveness, fidelity, and scalability. Given a property of interest, Aragogefficiently checks running systems for violations of the property with a scale-out architecture consisting of a collection of global verifiers and local monitors. To improve performance and reduce communication overhead, Aragog includes an array of optimizations that leverage properties of networked systems to suppress provably unnecessary system events and to shard verification over every available local and global component. We evaluate Aragog over several network functions including a NAT Gateway that powers Azure, identifying both design and implementation bugs in the process. 

   more » « less
4. IJIT: An API for Boolean Program Analysis with Just-in-Time Translation

   https://doi.org/https://doi.org/10.1007/978-3-319-66197-1_20  

   Liu, Peizun; Wahl, Thomas (January 2017, Software Engineering and Formal Methods (SEFM))

   Exploration algorithms for explicit-state transition systems are a core back-end technology in program verification. They can be applied to programs by generating the transition system on the fly, avoiding an expensive up-front translation. An on-the-fly strategy requires significant modifications to the implementation, into a form that stores states directly as valuations of program variables. Performed manually on a per-algorithm basis, such modifications are laborious and error-prone. In this paper we present the Ijit Application Programming Interface (API), which allows users to automatically transform a given transition system exploration algorithm to one that operates on Boolean programs. The API converts system states temporarily to program states just in time for expansion via image computations, forward or backward. Using our API, we have effortlessly extended various non-trivial (e.g. infinite-state) model checking algorithms to operate on multi-threaded Boolean programs. We demonstrate the ease of use of the API, and present a case study on the impact of the just-in-time translation on these algorithms. 

   more » « less
5. Unbounded-Time Safety Verification of Stochastic Differential Dynamics.

   https://doi.org/10.1007/978-3-030-53291-8_18  

   Feng, Shenghua; Chen, Mingshuai; Bai, Xue; Sankaranarayanan, Sriram; Zhan, Naijun (July 2020, Computer-Aided Verification (CAV))

   null (Ed.)

   In this paper, we propose a method for bounding the probability that a stochastic differential equation (SDE) system violates a safety specification over the infinite time horizon. SDEs are mathematical models of stochastic processes that capture how states evolve continuously in time. They are widely used in numerous applications such as engineered systems (e.g., modeling how pedestrians move in an intersection), computational finance (e.g., modeling stock option prices), and ecological processes (e.g., population change over time). Previously the safety verification problem has been tackled over finite and infinite time horizons using a diverse set of approaches. The approach in this paper attempts to connect the two views by first identifying a finite time bound, beyond which the probability of a safety violation can be bounded by a negligibly small number. This is achieved by discovering an exponential barrier certificate that proves exponentially converging bounds on the probability of safety violations over time. Once the finite time interval is found, a finite-time verification approach is used to bound the probability of violation over this interval. We demonstrate our approach over a collection of interesting examples from the literature, wherein our approach can be used to find tight bounds on the violation probability of safety properties over the infinite time horizon. 

   more » « less