This research focuses on developing a formal foundation and verification technique for signal temporal logic (STL), which specifies properties of continuous signals in hybrid systems. The goal is to enable robust bounded model checking of general STL properties, with correctness guarantees up to given bounds.

This research focuses on defining the behavior of the whole PLC behavior including the PLC ST, multitask, external environment, and communication features.

We define the MR-HybridSynchAADL modeling language and verification tool for hierarchical multirate CPSs with advanced control programs, continuous behaviors, and imprecise local clocks.

This project defines formal semantics of Promela using the K-Framework, with a support for deductive verification

In this research, we propose an "Activation Property", a form of information that can be extracted from previous verification processes, and develop a framework that leverages this for efficient incremental verification of neural networks. The proposed framework allows SOTA Branch-and-Bound(BaB)-based verifiers to support incremental verification with minimal modifications while improving verification performance.

This research focuses on presenting a formal specifcation of TEE APIs by leveraging Maude, to support formal analysis and verification of TEE applications.

WebAssembly (WASM) is a binary standard designed to execute high-performance programs on web browsers. Various verification techniques have been applied to WASM programs. In this study, we propose a model checking technique for WebAssembly programs using a rewriting logic-based Maude framework, aimed at verifying security properties related to concurrency and parallelism that have been challenging for existing methods.

This project leverages reinforcement learning to automatically learn search heuristics that improve the efficiency of model checking by guiding the exploration toward error states.

We use model-based testing approach to test TLS libraries using Maude. By using Maude, we can generate more various and complicated test scenario automatically. We build an automated tool to test several TLS libraries.

This research extends the Logical Model Checker (LMC) to verify a broader class of infinite-state systems by introducing a novel framework for constraint-based symbolic analysis and sound state-space reduction.

This research focuses on extending rewriting modulo SMT to support efficient and customizable symbolic analysis of infinite-state systems. The goal is to overcome the limitations of the existing Maude-SMT interface by enabling satisfying assignment generation, formula simplification, folding-based state-space reduction, and broader theory support including uninterpreted functions.

In this research, we propose a new technique, called layered abstraction, for non-linear activation functions, such as ReLU and Tanh, and the verification algorithm based on that. We have implemented our method by extending the existing SMT-based methods.