More Like this

1. Verification of Cyberphysical Systems

   https://doi.org/10.3390/math8071068  

   Sirjani, Marjan; Lee, Edward A.; Khamespanah, Ehsan (July 2020, Mathematics)

   The value of verification of cyberphysical systems depends on the relationship between the state of the software and the state of the physical system. This relationship can be complex because of the real-time nature and different timelines of the physical plant, the sensors and actuators, and the software that is almost always concurrent and distributed. In this paper, we study different ways to construct a transition system model for the distributed and concurrent software components of a CPS. The purpose of the transition system model is to enable model checking, an established and widely used verification technique. We describe a logical-time-based transition system model, which is commonly used for verifying programs written in synchronous languages, and derive the conditions under which such a model faithfully reflects physical states. When these conditions are not met (a common situation), a finer-grained event-based transition system model may be required. We propose an approach for formal verification of cyberphysical systems using Lingua Franca, a language designed for programming cyberphysical systems, and Rebeca, an actor-based language designed for model checking distributed event-driven systems. We focus on the cyber part and model a faithful interface to the physical part. Our method relies on the assumption that the alignment of different timelines during the execution of the system is the responsibility of the underlying platforms. We make those assumptions explicit and clear. 

   more » « less
2. Verification Complexity: An Initial Look at Verification Artifacts

   Jung, Raphael; Salado, A. (January 2023, Conference on Systems Engineering Research (CSER))
3. Verification of Hierarchical Artifact Systems

   https://doi.org/10.1145/3321487  

   Deutsch, Alin; Li, Yuliang; Vianu, Victor (June 2019, ACM Transactions on Database Systems)
4. Incremental Verification of Neural Networks

   https://doi.org/10.1145/3591299  

   Ugare, Shubham; Banerjee, Debangshu; Misailovic, Sasa; Singh, Gagandeep (June 2023, Proceedings of the ACM on Programming Languages)

   Complete verification of deep neural networks (DNNs) can exactly determine whether the DNN satisfies a desired trustworthy property (e.g., robustness, fairness) on an infinite set of inputs or not. Despite the tremendous progress to improve the scalability of complete verifiers over the years on individual DNNs, they are inherently inefficient when a deployed DNN is updated to improve its inference speed or accuracy. The inefficiency is because the expensive verifier needs to be run from scratch on the updated DNN. To improve efficiency, we propose a new, general framework for incremental and complete DNN verification based on the design of novel theory, data structure, and algorithms. Our contributions implemented in a tool named IVAN yield an overall geometric mean speedup of 2.4x for verifying challenging MNIST and CIFAR10 classifiers and a geometric mean speedup of 3.8x for the ACAS-XU classifiers over the state-of-the-art baselines. 

   more » « less
5. Scalable verification of probabilistic networks

   https://doi.org/10.1145/3314221.3314639  

   Smolka, Steffen; Kumar, Praveen; Kahn, David M.; Foster, Nate; Hsu, Justin; Kozen, Dexter; Silva, Alexandra (June 2019, Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation)

   This paper presents McNetKAT, a scalable tool for verifying probabilistic network programs. McNetKAT is based on a new semantics for the guarded and history-free fragment of Probabilistic NetKAT in terms of finite-state, absorbing Markov chains. This view allows the semantics of all programs to be computed exactly, enabling construction of an automatic verification tool. Domain-specific optimizations and a parallelizing backend enable McNetKAT to analyze networks with thousands of nodes, automatically reasoning about general properties such as probabilistic program equivalence and refinement, as well as networking properties such as resilience to failures. We evaluate McNetKAT's scalability using real-world topologies, compare its performance against state-of-the-art tools, and develop an extended case study on a recently proposed data center network design. 

   more » « less