Software is everywhere, but it can be buggy, unpredictable, and vulnerable to attacks. The goal of software verification is to ensure the reliability, security, and safety of software. In this research, we study automated algorithms for software verification, based model checking, computational logic, and satisfiability modulo theories (SMT).
Autonomous cyber-physical agent systems, such as self-driving cars and drones, must meet strong safety requirements. The goal of this study is to develop techniques to model and verify these systems before actual implementation, which can avoid possible accidents during prototype testing.
AI-based technologies such as deep neural networks are being applied to safety-critical applications, e.g., self-driving cars and air traffic control systems. The subject of this research is to develop new techniques to prove the safety requirements of AI-based systems, to prevent accidents or security problems caused by software errors.
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.
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.
This research focuses on presenting a formal specifcation of TEE APIs by leveraging Maude, to support formal analysis and verification of TEE applications.
This project leverages reinforcement learning to automatically learn search heuristics that improve the efficiency of model checking by guiding the exploration toward error states.
In this research, we aim to develop a framework that leverages "UNSAT" information from previous BaB-based verification processes to improve the integration of the Branch-and-Bound technique with incremental verification, which allows for SOTA BaB-based verifiers to support incremental verification with minimal modifications
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.