591 citations · 697 across the 15 of their papers we have counts for
15 papers
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…
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.…
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…
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…
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…
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,…
Perfectly Parallel Fairness Certification of Neural Networks
Caterina Urban, Maria Christakis, Valentin Wüstholz +1
Recently, there is growing concern that machine-learning models, which currently assist or even automate decision making, reproduce, and in the worst case reinforce, bias of the tr…
DeepSearch: A Simple and Effective Blackbox Attack for Deep Neural Networks
Fuyuan Zhang, Sankalan Pal Chowdhury, Maria Christakis
Although deep neural networks have been very successful in image-classification tasks, they are prone to adversarial attacks. To generate adversarial inputs, there has emerged a wi…
An Event-based Compositional Reasoning Approach for Concurrent Reactive Systems
Yongwang Zhao, David Sanan, Fuyuan Zhang +1
Reactive systems are composed of a well defined set of input events that the system reacts with by executing an associated handler to each event. In concurrent environments, event…
Combinatorial Testing for Deep Learning Systems
Lei Ma, Fuyuan Zhang, Minhui Xue +4
Deep learning (DL) has achieved remarkable progress over the past decade and been widely applied to many safety-critical applications. However, the robustness of DL systems recentl…
DeepMutation: Mutation Testing of Deep Learning Systems
Lei Ma, Fuyuan Zhang, Jiyuan Sun +8
Deep learning (DL) defines a new data-driven programming paradigm where the internal system logic is largely shaped by the training data. The standard way of evaluating DL models i…
DeepGauge: Multi-Granularity Testing Criteria for Deep Learning Systems
Lei Ma, Felix Juefei-Xu, Fuyuan Zhang +9
Deep learning (DL) defines a new data-driven programming paradigm that constructs the internal system logic of a crafted neuron network through a set of training data. We have seen…
High-Assurance Separation Kernels: A Survey on Formal Methods
Yongwang Zhao, David Sanan, Fuyuan Zhang +1
Separation kernels provide temporal/spatial separation and controlled information flow to their hosted applications. They are introduced to decouple the analysis of applications in…
Compositional Reasoning for Shared-variable Concurrent Programs
Fuyuan Zhang, Yongwang Zhao, David Sanan +4
Scalable and automatic formal verification for concurrent systems is always demanding. In this paper, we propose a verification framework to support automated compositional reasoni…
Reasoning About Information Flow Security of Separation Kernels with Channel-based Communication
Yongwang Zhao, David Sann, Fuyuan Zhang +1
Assurance of information flow security by formal methods is mandated in security certification of separation kernels. As an industrial standard for separation kernels, ARINC 653 ha…