Research
Logic and Algorithms for Software Verification.
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).
Modeling and Verification of Autonomous Cyber-Physical Agents.
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.
Automated Analysis of Safety-Critical AI Software.
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.
Ongoing research
SMT-Based Model Checking for Signal Temporal Logic
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.
Semantics and Analysis of PLC System
This research focuses on defining the behavior of the whole PLC behavior including the PLC ST, multitask, external environment, and communication features.
MH-SynchAADL
We define the MH-SynchAADL modeling language and verification tool for hierarchical multirate CPSs with advanced control programs, continuous behaviors, and imprecise local clocks.
Formal Specification of Trusted Execution Environment APIs
This research focuses on presenting a formal specifcation of TEE APIs by leveraging Maude, to support formal analysis and verification of TEE applications.
Model Checking of Infinite-State Systems using Narrowing
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.
Utilization of Activation Property for Efficient Incremental Neural Network 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.
TLS Model-based Testing using Maude
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.