More Like this

1. Differentiated Monitor Generation for Real-Time Systems

   https://doi.org/10.5220/0012080600003538  

   Rezvani, Behnaz; Patterson, Cameron (July 2023, Proceedings of the 18th International Conference on Software Technologies (ICSOFT 2023))

   Fill, Hans-Georg; Mayo, Francisco; van Sinderen, Marten; Maciaszek, Leszek (Ed.)

   Safety-critical real-time systems require correctness to be validated beyond the design phase. In these systems, response time is as critical as correct functionality. Runtime verification is a promising approach for validating the correctness of system behaviors during runtime using monitors derived from formal system specifications. However, practitioners often lack formal method backgrounds, and no standard notation exists to capture system properties that serve their needs. To encourage the adoption of formal methods in industry, we present GROOT, a runtime monitoring tool for real-time systems that automatically generates efficient monitors from structured English statements. GROOT is designed with two branches, one for functional requirements and one for specifications with metric time constraints, which use appropriate formalisms to synthesize monitors. This paper introduces TIMESPEC, a structured English dialect for specifying timing requirements. Our tool also automates formal analysis to certify the C monitors’ construction. We apply GROOT to timing specifications from an industrial component and a simulated autonomous system in Simulink. 

   more » « less
2. Tighter Abstract Queries in Neural Network Verification

   Cohen, Elazar; Elboher, Yizhak Yisrael; Barrett, Clark; Katz, Guy (June 2023, Proceedings of the 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2023))

   Piskac, Ruzica; Voronkov, Andrei (Ed.)

   Neural networks have become critical components of reactive systems in various do- mains within computer science. Despite their excellent performance, using neural networks entails numerous risks that stem from our lack of ability to understand and reason about their behavior. Due to these risks, various formal methods have been proposed for verify- ing neural networks; but unfortunately, these typically struggle with scalability barriers. Recent attempts have demonstrated that abstraction-refinement approaches could play a significant role in mitigating these limitations; but these approaches can often produce net- works that are so abstract, that they become unsuitable for verification. To deal with this issue, we present CEGARETTE, a novel verification mechanism where both the system and the property are abstracted and refined simultaneously. We observe that this approach allows us to produce abstract networks which are both small and sufficiently accurate, allowing for quick verification times while avoiding a large number of refinement steps. For evaluation purposes, we implemented CEGARETTE as an extension to the recently proposed CEGAR-NN framework. Our results are highly promising, and demonstrate a significant improvement in performance over multiple benchmarks. 

   more » « less
3. Visualizing Virtual Vector Fields

   Alrawi, Othman; Day, Brian; Matsumoto, Elisabetta A. (August 2022, Proceedings of Bridges 2022: Mathematics, Art, Music, Architecture, Culture)

   We present our current progress on a virtual reality sandbox experience equipped with a toolset to create interactive vector fields and vector calculus operations. The aim of the project is to empower the student’s understanding of vector field and assist in the development of their intuition. The source code for this project is open-source and available at https://github.com/OthmanAlrawi/Visualizing-Vector-Fields. 

   more » « less
4. Probabilistic Refinement Session Types

   https://doi.org/10.1145/3729317  

   Fu, Qiancheng; Das, Ankush; Gaboardi, Marco (June 2025, Proceedings of the ACM on Programming Languages)

   Session types provide a formal type system to define and verify communication protocols between message-passing processes. In order to analyze randomized systems, recent works have extended session types with probabilistic type constructors. Unfortunately, all the proposed extensions only support constant probabilities which limits their applicability to real-world systems. Our work addresses this limitation by introducing probabilistic refinement session types which enable symbolic reasoning for concurrent probabilistic systems in a core calculus we call PReST. The type system is carefully designed to be a conservative extension of refinement session types and supports both probabilistic and regular choice type operators. We also implement PReST in a prototype which we use for validating probabilistic concurrent programs. The added expressive power leads to significant challenges, both in the meta theory and implementation of PReST, particularly with type checking: it requires reconstructing intermediate types for channels when type checking probabilistic branching expressions. The theory handles this by semantically quantifying refinement variables in probabilistic typing rules, a deviation from standard refinement type systems. The implementation relies on a bi-directional type checker that uses an SMT solver to reconstruct the intermediate types minimizing annotation overhead and increasing usability. To guarantee that probabilistic processes are almost-surely terminating, we integrate cost analysis into our type system to obtain expected upper bounds on recursion depth. We evaluate PReST on a wide variety of benchmarks from 4 categories: (i) randomized distributed protocols such as Itai and Rodeh's leader election, bounded retransmission, etc., (ii) parametric Markov chains such as random walks, (iii) probabilistic analysis of concurrent data structures such as queues, and (iv) distributions obtained by composing uniform distributions using operators like max, and sum. Our experiments show that the PReST type checker scales to large programs with sophisticated probabilistic distributions. 

   more » « less
5. Refinement-Based Game Semantics and Certified Abstraction Layers

   Koenig, Jeremie; Shao, Zhong (July 2020, Proc. 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'20))

   Formal methods have advanced to the point where the functional correctness of various large system components has been mechanically verified. However, the diversity of semantic models used across projects makes it difficult to connect these component to build larger certified systems. Given this, we seek to embed these models and proofs into a general-purpose framework where they could interact. We believe that a synthesis of game semantics, the refinement calculus, and algebraic effects can provide such a framework. To combine game semantics and refinement, we replace the downset completion typically used to construct strategies from posets of plays. Using the free completely distributive completion, we construct strategy specifications equipped with arbitrary angelic and demonic choices and ordered by a generalization of alternating refinement. This provides a novel approach to nondeterminism in game semantics. Connecting algebraic effects and game semantics, we interpret effect signatures as games and define two categories of effect signatures and strategy specifications. The resulting models are sufficient to represent the behaviors of a variety of low-level components, including the certified abstraction layers used to verify the operating system kernel CertiKOS. 

   more » « less