A5042013137- Formal Methods in Verification
- Logic, programming, and type systems
- Software Testing and Debugging Techniques
- Software Engineering Research
- Distributed systems and fault tolerance
- Security and Verification in Computing
- Advanced Software Engineering Methodologies
- Embedded Systems Design Techniques
- Parallel Computing and Optimization Techniques
- Advanced Malware Detection Techniques
- Real-Time Systems Scheduling
- Software Reliability and Analysis Research
- Model-Driven Software Engineering Techniques
- Service-Oriented Architecture and Web Services
- Adversarial Robustness in Machine Learning
- Software System Performance and Reliability
- Business Process Modeling and Analysis
- Petri Nets in System Modeling
- Software Engineering Techniques and Practices
- Machine Learning and Algorithms
- Anomaly Detection Techniques and Applications
- Scientific Computing and Data Management
- semigroups and automata theory
- Network Security and Intrusion Detection
- Natural Language Processing Techniques
Xidian University
2023-2024
Huawei Technologies (China)
2024
Teesside University
2013-2022
Shenzhen University
2013-2022
Durham University
2005-2018
Nanyang Technological University
2015
Shanghai Key Laboratory of Trustworthy Computing
2015
East China Normal University
2015
Public and Science
2013
Beijing University of Technology
2012-2013
Uncontrolled memory consumption is a kind of critical software security weaknesses. It can also become security-critical vulnerability when attackers take control the input to consume large amount and launch Denial-of-Service attack. However, detecting such challenging, as state-of-the-art fuzzing techniques focus on code coverage but not consumption. To this end, we propose usage guided technique, named MemLock, generate excessive inputs trigger uncontrolled bugs. The process with...
Existing coverage-based fuzzers usually use the individual control flow graph (CFG) edge coverage to guide fuzzing process, which has shown great potential in finding vulnerabilities. However, CFG is not effective discovering vulnerabilities such as use-after-free (UaF). This because, trigger UaF vulnerabilities, one needs only cover edges, but also traverse some (long) sequence of edges a particular order, challenging for existing fuzzers. To this end, we propose model typestate properties,...
Static analysis tools for capturing bugs and vulnerabilities in software programs are widely employed practice, as they have the unique advantages of high coverage independence from execution environment. However, existing analyzing large codebases often produce a great deal false warnings over genuine bug reports. As result, developers required to manually inspect confirm each warning, challenging, time-consuming, automation-essential task. This article advocates fast, general, easily...
Timed Automata have proven to be useful for specification and verification of real-time systems. System design using relies on explicit manipulation clock variables. A number automated analyzers been developed. However, lack composable patterns high-level system design. Logic-based languages like CSP TCOZ are well suited presenting compositional models complex In this work, we define a set based hierarchical constructs in timed enriched process algebras. The facilitate systems Automata. They...
Point-of-interest(POI) recommendation becomes a valuable service in location-based social networks. Based on the norm that similar users are likely to have preference of POIs, current techniques mainly focus users' provide accurate results. This tends generate list homogeneous POIs clustered into narrow band location categories(like food, museum, etc.) city. However, more interested taste wide range flavors exposed global set categories city.In this paper, we formulate new POI problem,...
Conventional specifications for object-oriented (OO) programs must adhere to behavioral subtyping in support of class inheritance and method overriding. However, this requirement inherently weakens the overridden methods superclasses, leading imprecision during program reasoning. To address this, we advocate a fresh approach OO verification that focuses on distinction relation between cater calls with static dispatching from those dynamic dispatching. We formulate novel specification...
Simulink is an industrial de-facto standard for building executable models of embedded systems and their environments, facilitating validation by simulation. Due to the inherent incompleteness this form system validation, complementing simulation formal verification would be desirable. A prerequisite such approach a semantics Simulink's graphical models. In paper, we show how encode diagrams into Hybrid CSP (HCSP), modelling language encoding hybrid dynamics means extension CSP. The...
Techniques for proving termination and non-termination of imperative programs are usually considered as orthogonal mechanisms. In this paper, we propose a novel mechanism that analyzes proves both program at the same time. We first introduce concept second-order constraints accumulate set relational assumptions on them via Hoare-style verification. then solve these with case analysis to determine (conditional) non- scenarios expressed in some specification logic form. contrast current...
Chest X-ray plays a key role in screening and diagnosis of many lung diseases including the COVID-19. Many works construct deep neural networks (DNNs) for chest images to realize automated efficient diseases. However, bias field caused by improper medical image acquisition process widely exists while robustness DNNs is rarely explored, posing threat X-ray-based system. In this paper, we study problem based on adversarial attack propose brand new attack, i.e., where instead additive noise as...
Rust libraries are ubiquitous in Rust-based software development. Guaranteeing their correctness and reliability requires thorough analysis testing. Fuzzing is a popular bug-finding solution, yet it writing fuzz targets for libraries. Recently, some automatic target generation methods have been proposed. However, two challenges remain: (1) how to generate diverse API sequences that prioritize unsafe code interactions reveal bugs libraries; (2) provide support the generic APIs verify both...
The research in AI-based formal mathematical reasoning has shown an unstoppable growth trend. These studies have excelled competitions like IMO, showing significant progress. However, these intertwined multiple skills simultaneously, i.e., problem-solving, reasoning, and writing specifications, making it hard to precisely identify the LLMs' strengths weaknesses each task. This paper focuses on verification, immediate application scenario of decomposes into six sub-tasks. We constructed 18k...
Controversial contents largely inundate the Internet, infringing various cultural norms and child protection standards. Traditional Image Content Moderation (ICM) models fall short in producing precise moderation decisions for diverse standards, while recent multimodal large language (MLLMs), when adopted to general rule-based ICM, often produce classification explanation results that are inconsistent with human moderators. Aiming at flexible, explainable, accurate we design a novel dataset...
Embedded systems are becoming more widely used but these often resource constrained. Programming models for should take into formal consideration resources such as stack and heap. In this paper, we show how memory bounds can be inferred assembly-level programs. Our inference process captures the needs of each method in terms symbolic values its parameters. For better precision, infer path-sensitive information through a novel guarded expression format. current proposal relies on Presburger...
Simulink is an industrial de-facto standard for building executable models of embedded systems and their environments, facilitating validation by simulation. Due to the inherent incompleteness this form system validation, complementing simulation formal verification would be desirable. A prerequisite such approach a semantics Simulink's graphical models. In paper, we show how encode diagrams into Hybrid CSP (HCSP), modelling language encoding hybrid dynamics means extension CSP. The...