activity
20162026
most citedHigh-Assurance Separation Kernels: A Survey on Formal Methods

4 citations · 7 across the 7 of their papers we have counts for

collaborators

14 papers

cs.CR2026

Towards Real-World Industrial-Scale Verification: LLM-Driven Theorem Proving on seL4

Jianyu Zhang, Fuyuan Zhang, Jiayi Lu +5

Formal methods (FM) are reliable but costly to apply, often requiring years of expert effort in industrial-scale projects such as seL4, especially for theorem proving. Recent advan…

cs.SE2023

Event-based Compositional Reasoning of Information-Flow Security for Concurrent Systems

Yongwang Zhao, David Sanan, Fuyuan Zhang +1

High assurance of information-flow security (IFS) for concurrent systems is challenging. A promising way for formal verification of concurrent systems is the rely-guarantee method.…

cs.SE2023★ 3 cited

Mosaic: Model-based Safety Analysis Framework for AI-enabled Cyber-Physical Systems

Xuan Xie, Jiayang Song, Zhehua Zhou +2

Cyber-physical systems (CPSs) are now widely deployed in many industrial domains, e.g., manufacturing systems and autonomous vehicles. To further enhance the capability and applica…

cs.SE2022

Towards Benchmarking GUI Compatibility Testing on Mobile Applications

Jiaming Ye, Mulong Xie, Siyuan Chen +4

GUI is a bridge connecting user and application. Existing GUI testing tasks can be categorized into two groups: functionality testing and compatibility testing. While the functiona…

cs.SE2022

DeepGalaxy: Testing Neural Network Verifiers via Two-Dimensional Input Space Exploration

Xuan Xie, Fuyuan Zhang

Deep neural networks (DNNs) are widely developed and applied in many areas, and the quality assurance of DNNs is critical. Neural network verification (NNV) aims to provide formal…

cs.SE2020

Detecting Critical Bugs in SMT Solvers Using Blackbox Mutational Fuzzing

Muhammad Numair Mansur, Maria Christakis, Valentin Wüstholz +1

Formal methods use SMT solvers extensively for deciding formula satisfiability, for instance, in software verification, systematic test generation, and program synthesis. However,…