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.

Research Projects

Layered Abstraction Technique for Effective Formal Verification of Deep Neural Networks

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.

SMT-Based Model Checking for Signal Temporal Logic

This research focuses on modeling cyber-physical systems (CPS) that rely on virtual synchrony for coordination and timing accuracy. The goal is to improve the reliability of CPS in critical applications such as aerospace or automotive systems, where precision and safety are paramount.

Reusable Model Checking

Model checking usually takes very long time until a result is obtained. Even worse, model checking typically is quite a repetitive process, much like software development. Our main goal is to devise a learning based technique that exploits frequent logical patterns within a group of similar model checking instances to accelerate the search.

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.