出版物

书籍

Automatic Generation of Combinatorial Test Data

作者：Jian Zhang, Zhiqiang Zhang, Feifei Ma

Logic in Computer Science

作者：Hantao Zhang, Jian Zhang

已发表论文

2020-现在

2026

[TKDE] A Closer Look at the Application of Causal Inference in Graph Representation Learning - H Gao, K Li, H Hong, B Cui, F Wu
[ASE] Efficient Code Analysis via Graph-Guided Large Language Models - H Gao, T Peng, B Cui, H Huang, F Wu, J Zhao, J Zhang
[ICSE] OSmartPro : a large language model-assisted option fuzzing approach - K Wang, M Chen, L He, Y Wang, P Su, JY Chen, Y Cai, B Zhang, C Feng, ...
[SPE] Runtime Monitoring Abnormalities in Object Detection With Spatial and Temporal Abstractions - R Yan, C Li, R Zheng, CH Cheng
[ICRA] Validating Generalist Robots with Situation Calculus and STL Falsification - C Li, R Yan, CH Cheng, J Zhang

2025

[TSE] A comprehensive evaluation of four end-to-end ai autopilots using cctest and the carla leaderboard - C Li, J Sifakis, R Yan, J Zhang
[APSEC] A Packing-Insensitive Detection Method for Android Malware Based on Image Representation - S Ma, S Zhu, L Zhang, Y Cai
[TSE] Boosting Generalizable Fairness With Mahalanobis Distances Guided Boltzmann Exploratory Testing - K Dong, P Wu, Y Chen
[AAAI] Bootstrapping heterogeneous graph representation learning via large language models: A generalized approach - H Gao, C Zhang, F Wu, C Zheng, J Zhao, H Liu
[AAAI] Bootstrapping Heterophily Graph Representation Learning via a Large Language Model-Based Approach - W Huang, F Wu, H Gao, J Zhao
[ICSE] CCTest: Critical Configuration Testing for Autonomous Driving Systems - C Li, J Sifakis, R Yan, J Zhang
[IEEE] Checking Linearizability of Multi-core Task Management and Scheduling System - Q Jia, L Lv, Y Yang, B Zhan, P Wu, J Hao, H Ye, C Wang, Y Lv
[IEEE] Def-VAE: Identifying Adversarial Inputs with Robust Latent Representations - C Li, C Wu, R Yan
[TSE] Intrathread method orders based adaptive testing of concurrent objects - Y Dai, L Xie, P Wu, S Cui, L Ma
[IJCAI] Learn to Think: Bootstrapping LLM Logic Through Graph Representation Learning - H Gao, C Zhang, T Wang, J Zhao, F Wu, C Zheng, H Liu
[IJCAI] Learn to Think: Bootstrapping LLM Reasoning Capability Through Graph Learning - H Gao, C Zhang, T Wang, J Zhao, F Wu, C Zheng, H Liu
[IJCAI] Learn to Think: Bootstrapping LLM Reasoning Capability Through Graph Representation Learning - H Gao, C Zhang, T Wang, J Zhao, F Wu, C Zheng, H Liu
[KDD] LLM Enhancers for GNNs: An Analysis from the Perspective of Causal Mechanism Identification - H Gao, W Huang, F Wu, J Zhao, C Zheng, H Liu
[WWW] LNAHGN: LLM-Guided Neighbor Aggregation for Heterogeneous Graph Neural Network - C Zhang, F Wu, H Gao
[ICSE] Reduce Dependence for Sound Concurrency Bug Prediction - S Zhu, Y Guo, Y Cai, B Liang, L Zhang, R Chen, T Yu
[APSEC] Seed-Adapted Cross-State Protocol Fuzzing - D Li, S Zhu, Y Cai, L Zhang
[ICRA] Simulation-Based Testing of Autonomous Robotic Systems for Surgical Applications - J Lin, T Sun, R Song, D Zhu, L Liu, J Leng, K Huang, R Yan
[IEEE] Testing Autonomous Driving Systems with Irregular Junctions Extracted from OpenStreetMap - T Sun, C Li, R Yan, Y Cai
[TSE] Testing Autonomous Driving Systems--What Really Matters and What Doesn't - C Li, J Sifakis, R Yan, J Zhang
[AAAI] Training deep neural networks with virtual smoothing classes - Z Zhou, S Wei, X Zhang, W Dou, M Qu, Y Cai

2024

[TSE] Adaptive Testing of Concurrent Objects - Y Dai¹, P Wu, S Cui¹, L Ma
[ICRA] Automatic construction of HD maps for simulation-based testing of autonomous driving systems - S Wang, C Li, T Sun, F Jia, R Yan, J Yan
[PPoPP] but Not Strongly Linearizable Concurrent Objects - C Wang, P Wu, G Petri, Q Jia¹, Y He¹
[ICML] Extending test-time augmentation with metamorphic relations for combinatorial problems - S Wei, X Zhang, Z Zhou, Y Cai
[AAAI] Graph Partial Label Learning with Potential Cause Discovering - H Gao, J Yuan, J Li, P Qiao, F Wu, C Zheng, H Liu
[AAAI] Hierarchical topology isomorphism expertise embedded graph contrastive learning - J Li, Y Jin, H Gao, W Qiang, C Zheng, F Sun
[KBS] Introducing diminutive causal structure into graph representation learning - H Gao, P Qiao, Y Jin, F Wu, J Li, C Zheng
[NN] Learning node representations under partial label learning - J Yuan, H Gao, F Wu, J Zhao
[TKED] Molecular graph representation learning via structural similarity information - C Yao, H Huang, H Gao, F Wu, H Chen, J Zhao
[TSE] Multi-level Critical Transformation Robustness Evaluation of Object Detection Models - Z Zhang, C Li, Z Liang, C Yao, J Zhang, R Yan, P Wu
[SIGSAC] OSmart: Whitebox Program Option Fuzzing - K Wang, M Chen, L He, P Su, Y Cai, J Chen, B Zhang, C Feng, C Tang
[TSE] Out-of-bounding-box triggers: A stealthy approach to cheat object detectors - T Lin, L Yu, G Jin, R Li, P Wu, L Zhang
[ICSE] Reorder pointer flow in sound concurrency bug prediction - Y Guo, S Zhu, Y Cai, L He, J Zhang
[AAAI] Rethinking causal relationships learning in graph neural networks - H Gao, C Yao, J Li, L Si, Y Jin, F Wu, C Zheng, H Liu
[TSE] Rigorous Simulation-based Testing for Autonomous Driving Systems--Targeting the Achilles' Heel of Four Open Autopilots - C Li, J Sifakis, R Yan, J Zhang
[ICSE] Slicing Assisted Program Verification: An Empirical Study - W Chai, R Yan, W Zhang, J Zhang
[CONCUR] Strong Linearizability Checking and Determination for Concurrent Objects. - C Wang, Q Jia, Y Lyu, P Wu
[KDD] The Double-Edged Sword of Input Perturbations to Robust Accurate Fairness - X Li, P Wu, Y Chen, X Ma, Z Zhang, K Dong
[PPoPP] Universal construction for linearizable but not strongly linearizable concurrent objects - C Wang, P Wu, G Petri, Q Jia, Y He, Y Lv, Z Liu
[KBS] Unsupervised social event detection via hybrid graph contrastive learning and reinforced incremental clustering - Y Guo, Z Zang, H Gao, X Xu, R Wang, L Liu, J Li

2023

[TGRS] A unified gan framework regarding manifold alignment for remote sensing images generation - X Su, W Qiang, Z Song, H Gao, F Wu, C Zheng
[AAAI] Accurate fairness: Improving individual fairness without trading accuracy - X Li, P Wu, J Su
[TSE] An interleaving guided metamorphic testing approach for concurrent programs - CA Sun, H Dai, N Geng, H Liu, TY Chen, P Wu, Y Cai, J Wang
[SIGSOFT] Building critical testing scenarios for autonomous driving from real accidents - X Zhang, Y Cai
[ASPLOS] Discovering parallelisms in python programs - S Wei, G Song, S Zhu, R Ruan, S Zhu, Y Cai
[NN] Information theory-guided heuristic progressive multi-view coding - J Li, H Gao, W Qiang, C Zheng
[KDD] Introducing Expertise Logic into Graph Representation Learning from A Causal Perspective - H Gao, J Li, W Qiang, L Si, X Su, F Wu, C Zheng, F Sun
[NN] Introducing semantic-based receptive field into semantic segmentation via graph neural networks - D Jia, H Gao, X Su, F Wu, J Zhao
[KDD] Manifold-guided sampling in diffusion models for unbiased image generation - X Su, W Qiang, Z Song, H Gao, F Wu, C Zheng
[ASPLOS] One simple api can cause hundreds of bugs an analysis of refcounting bugs in all modern linux kernels - L He, P Su, C Zhang, Y Cai, J Ma
[AAAI] Robust causal graph representation learning against confounding effects - H Gao, J Li, W Qiang, L Si, B Xu, C Zheng, F Sun
[ICSE] RobustFair: Adversarial Evaluation through Fairness Confusion Directed Gradient Search - X Li, P Wu, K Dong, Z Zhang, Y Chen
[RV] Runtime Monitoring DNN-Based - CH Cheng, M Luttenberger¹, R Yan
[SETTA] Runtime Monitoring DNN-Based Perception: (via the Lens of Formal Methods) - CH Cheng, M Luttenberger, R Yan
[SIGSOFT] Simulation-based validation for autonomous driving systems - C Li, J Sifakis, Q Wang, R Yan, J Zhang
[ISSTA] VeriLin: A linearizability checker for large-scale concurrentSound Predictive Fuzzing for Multi-threaded Programs - Y Guo, Z Liang, S Zhu, J Wang, Z Yang, W Shen, J Zhang, Y Cai
[ICSE] Tolerate control-flow changes for sound data race prediction - S Zhu, Y Guo, L Zhang, Y Cai
[ISSTA] VeriLin: A linearizability checker for large-scale concurrent objects - Q Jia, Y Lv, P Wu, B Zhan, J Hao, H Ye, C Wang

2022

[ISSRE] Adversarial input detection based on critical transformation robustness - J Su, Z Zhang, P Wu, X Li, J Zhang
[IJCAI] Bootstrapping informative graph augmentation via a meta learning approach - H Gao, J Li, W Qiang, L Si, F Sun, C Zheng
[ICRA] ComOpT: Combination and optimization for testing autonomous driving systems - C Li, CH Cheng, T Sun, Y Chen, R Yan
[TR] Concspectre: Be aware of forthcoming malware hidden in concurrent programs - Y Liu, Z Xu, M Fan, Y Hao, K Chen, H Chen, Y Cai, Z Yang, T Liu
[SANER] Excepy: A python benchmark for bugs with python built-in types - X Zhang, R Yan, J Yan, B Cui, J Yan, J Zhang
[NN] Layer-specific repair of neural network classifiers - S Sun, J Yan, R Yan
[WWW] Self-supervised Graph Learning with Segmented Graph Channels - H Gao, J Li, C Zheng
[ISSRE] Test case prioritization with neuron valuation based pattern - R Yan, Y Chen, H Gao, J Yan
[NN] Weight-aware graph contrastive learning - H Gao, J Li, P Qiao, C Zheng
[USENIX Security] {FreeWill}: Automatically Diagnosing Use-after-free Bugs via Reference Miscounting Detection on Binaries - L He, H Hu, P Su, Y Cai, Z Liang

2021

[CONCUR] Bounded Linearizability on TSO Memory Model is Decidable - C Wang, Y Lv, P Wu, Q Jia
[DATE] Continuous safety verification of neural networks - CH Cheng, R Yan
[ISSRE] Detecting concurrency vulnerabilities based on partial orders of memory and thread events - K Yu, C Wang, Y Cai, X Luo, Z Yang
[TSE] Efficient testing of GUI applications by event sequence reduction - J Yan, H Zhou, X Deng, P Wang, R Yan, J Yan, J Zhang
[SIGSOFT] Empirical evaluation of smart contract testing: What is the best choice? - M Ren, Z Yin, F Ma, Z Xu, Y Jiang, C Sun, H Li, Y Cai
[RSJ] Monitoring object detection abnormalities via data-label and post-algorithm abstractions - Y Chen, CH Cheng, J Yan, R Yan
[AAAI] Out-of-distribution detection through relative activation-deactivation abstractions - Z Zhang, P Wu, Y Chen, J Su
[SIGSOFT] RAProducer: efficiently diagnose and reproduce data race bugs for binaries via trace analysis - M Yuan, Y Lee, C Zhang, Y Li, Y Cai, B Zhao
[ASPLOS] Sound and efficient concurrency bug prediction - Y Cai, H Yun, J Wang, L Qiao, J Palsberg
[JSS] Stability evaluation for text localization systems via metamorphic testing - R Yan, S Wang, Y Yan, H Gao, J Yan
[ASE] Testing autonomous systems with believed equivalence refinement - CH Cheng, R Yan
[TSE] Xdebloat: Towards automated feature-oriented app debloating - Y Tang, H Zhou, X Luo, T Chen, H Wang, Z Xu, Y Cai

2020

[QRS] A study on testing autonomous driving systems - X Zhang, Y Cai, Z Yang
[TR] An iterative metamorphic testing technique for web services and case studies - C Sun, A Fu, Y Liu, Q Wen, Z Wang, P Wu, TY Chen
[JSA] Contention-aware mapping and scheduling optimization for NoC-based MPSoCs - R Yan, Y Zhou, A Cai, C Li, Y Yan, M Yin
[AAAI] Contention-Aware Mapping and Scheduling Optimization for NoC-Based MPSoCs (Student Abstract) - Y Zhou, R Yan, A Cai, Y Yan, M Yin
[TSE] Corrections to “Detecting Bugs by Discovering Expectations and Their Violations” - P Bian, B Liang, Y Zhang, C Yang, W Shi, Y Cai
[ASE] Fairness testing of machine learning models using deep reinforcement learning - W Xie, P Wu
[APSEC] Feature Location Benchmark for Decomposing and Reusing Android Apps - Y Tang, H Zhou, Z Xu, X Luo, Y Cai, T Zhang
[ICSE] Low-overhead deadlock prediction - Y Cai, R Meng, J Palsberg
[ISSRE] Neuron activation frequency based test case prioritization - K Zhang, Y Zhang, L Zhang, H Gao, R Yan, J Yan
[ASPLOS] Resource race attacks on android - Y Cai, Y Tang, H Li, L Yu, H Zhou, X Luo, L He, P Su
[SQJ] Special section on testing and repair for software engineering technologies and applications - I Bayley, Y Cai, P Machado

2010-2019

2019

[CSUR] Architecting dependable learning-enabled autonomous systems: A survey - CH Cheng, D Gulati, R Yan
[ICSE] Convul: an effective tool for detecting concurrency vulnerabilities - R Meng, B Zhu, H Yun, H Li, Y Cai, Z Yang
[FSE] Detecting concurrency memory corruption vulnerabilities - Y Cai, B Zhu, R Meng, H Yun, L He, P Su, B Liang
[JSA] Fine-grained communication-aware task scheduling approach for acyclic and cyclic applications on MPSoCs - K Huang, X Jiang, H Jiang, X Zhang, M Yu, R Yan, X Yan
[ICSE] sCompile: Critical path identification and analysis for smart contracts - J Chang, B Gao, H Xiao, J Sun, Y Cai, Z Yang
[JSA] Smt-based multi-objective optimization for scheduling of mpsoc applications - R Yan, A Cai, H Gao, F Ma, J Yan

2018

[ICST] A weight-based approach to combinatorial test generation - J Zhao, GR Ning, HL Lu, YB Wang, Y Cai, J Zhang
[CONCUR] Decidability of linearizabilities for relaxed data structures - C Wang, Y Lv, P Wu
[JSA] Design verification and validation for reliable safety-critical autonomous control systems - R Yan, J Yang, D Zhu, K Huang
[TSE] Detecting bugs by discovering expectations and their violations - P Bian, B Liang, Y Zhang, C Yang, W Shi, Y Cai
[IST] Diversity driven adaptive test generation for concurrent data structures - L Ma, P Wu, TY Chen
[TCAD] Energy-efficient fault-tolerant mapping and scheduling on heterogeneous multiprocessor real-time systems - K Huang, X Jiang, X Zhang, R Yan, K Wang, D Xiong, X Yan
[JSA] Energy-efficient scheduling of periodic applications on safety-critical time-triggered multiprocessor systems - X Jiang, K Huang, X Zhang, R Yan, K Wang, D Xiong, X Yan
[JSA] Expected energy optimization for real-time multiprocessor SoCs running periodic tasks with uncertain execution time - K Huang, K Wang, D Zheng, X Jiang, X Zhang, R Yan, X Yan
[ISSTA] Interleaving-tree based fine-grained linearizability fault localization - Y Chen, Z Zhang, P Wu, Y Zhang
[FSE] Nar-miner: discovering negative association rules from code for bug detection - P Bian, B Liang, W Shi, J Huang, Y Cai
[ICSE] Poster: A Weight-Based Approach to Combinatorial Test Generation - J Zhao, G Ning, H Lu, Y Wang, C Yan, J Zhang
[JSA] Resource-aware design for reliable autonomous applications with multiple periods - R Yan, D Zhu, F Zhang, Y Lv, J Yang, K Huang

2017

[JSA] A Hybrid Multi-objective Evolutionary Algorithm for Energy-Aware Allocation and Scheduling Optimization of MPSoCs - R Yan, Y Zhou, Y Yan, M Yin, M Yu, F Ma, K Huang
[ICSE] Adaptively generating high quality fixes for atomicity violations - Y Cai, L Cao, J Zhao
[TSE] Atexrace: Across thread and execution sampling for in-house race detection - Y Guo, Y Cai, Z Yang
[ASE] Automatically assessing crashes from heap overflows - L He, Y Cai, H Hu, P Su, Z Liang, Y Yang, H Huang, J Yan, X Jia, D Feng
[COMPSAC] Comprehensive Static Analysis for Configurable Software via Combinatorial Instantiation - D Yan, L Pan, R Yan, J Yan, J Zhang
[PPoPP] Decomposable relaxation for concurrent data structures - C Wang, Y Lv, P Wu
[JSA] Formal collision avoidance analysis for rigorous building of autonomous marine vehicles - R Yan, X Yao, J Yang, K Huang
[ISSRE] Localization of linearizability faults on the coarse-grained level - Z Zhang, P Wu, Y Zhang
[SETTA] Synthesizing coalitions for multi-agent games - W Ji, F Wang, P Wu
[ASPLOS] Undead: Detecting and preventing deadlocks in production software - J Zhou, S Silvestro, H Liu, Y Cai, T Liu

2016

[JSS] 5W+ 1H pattern: A perspective of systematic mapping studies and a case study on cloud software testing - C Jia, Y Cai, YT Yu, TH Tse
[SIGSOFT] A deployable sampling strategy for data race detection - Y Cai, J Zhang, L Cao, J Liu
[SETTA] An experiment on decision diagrams for model checking probabilistic timed automata - W Ji, F Wang, P Wu, Y Lv
[ICSE] AntMiner - B Liang, P Bian, Y Zhang, W Shi, W You, Y Cai
[ICSE] AntMiner: mining more bugs by reducing noise interference - B Liang, P Bian, Y Zhang, W Shi, W You, Y Cai
[CONCUR] Bounded TSO-to-SC linearizability is decidable - C Wang, Y Lv, P Wu
[FM] Component-based verification using incremental design and invariants - S Bensalem, M Bozga, A Legay, TH Nguyen, J Sifakis, R Yan
[TSE] Dynamic testing for deadlocks via constraints - Y Cai, Q Lu
[ICSE] Fixing deadlocks via lock pre-acquisitions - Y Cai, L Cao
[ISPA] Modelling and Analysis of Network Security-an Algebraic Approach - Q Zhang, Y Jiang, P Wu
[ASE] Radius aware probabilistic testing of deadlocks with guarantees - Y Cai, Z Yang

2015

[HRI] A Verifiable and Correct-by-Construction Controller for Robots in Human Environments - SB Lavindra de Silva, Rongjie Yan, Félix Ingrand, Rachid Alami
[TECS] Communication optimizations for multithreaded code generation from Simulink models - K Huang, M Yu, R Yan, X Zhang, X Yan, L Brisolara, AA Jerraya, J Feng
[ICSE] Effective and precise dynamic detection of hidden races for java programs - Y Cai, L Cao
[DATE] Formal consistency checking over specifications in natural languages - R Yan, CH Cheng, Y Chai
[DATE] Formal consistency checking over specifications in natural languages. In 2015 Design, Automation & Test in Europe Conference & Exhibition (DATE) - R Yan, CH Cheng, Y Chai
[VLSI] Functional testbench qualification by mutation analysis - K Huang, P Zhu, R Yan, X Yan
[APSEC] Input-driven active testing of multi-threaded programs - H Yue, P Wu, TY Chen, Y Lv
[CONCUR] Quasi-linearizability is undecidable - C Wang, Y Lv, G Liu, P Wu
[ETRI] Software Partitioning Method Trading off Load Balance and Communication Optimization. - K Huang, S Xiu, M Yu, X Zhang, R Yan, X Yan, Z Liu
[TASE] Static optimal scheduling for synchronous data flow graphs with model checking - XY Zhu, R Yan, YL Gu, J Zhang, W Zhang, G Zhang
[ATVA] TSO-to-TSO Linearizability Is Undecidable - C Wang, Y Lv, P Wu

2014

[TSE] A subsumption hierarchy of test case prioritization for composite services - L Mei, Y Cai, C Jia, B Jiang, WK Chan, Z Zhang, TH Tse
[ASP] Annotation and Analysis Combined Cache Modeling for Native Simulation - R Yan, D Ma, K Huang, X Zhang, S Xiu
[TSE] ASN: a dynamic barrier-based approach to confirmation of deadlocks from warnings for large-scale multithreaded programs - Y Cai, C Jia, S Wu, K Zhai, WK Chan
[JSA] Communication-oriented performance optimisation during code generation from Simulink models - R Yan, M Yu, K Huang, X Zhang
[ICSE] ConLock: A constraint-based approach to dynamic checking on deadlocks in multithreaded programs - Y Cai, S Wu, WK Chan
[ISSTA] Efficiently and completely verifying synchronized consistency models - Y Lv, L Sun, X Ye, D Fan, P Wu
[TASE] Formal throughput and response time analysis of MARTE models - G Yan, XY Zhu, R Yan, G Li
[IEICE] ILP based multithreaded code generation for Simulink model - K Huang, M Yu, X Zhang, D Zheng, S Xiu, R Yan, Z LIU, X YAN
[ICSE] Magiclock: Scalable detection of potential deadlocks in large-scale multithreaded programs - Y Cai, WK Chan
[ICESS] Modeling and Verifying of CPS Component Services Based on Hybrid Automata - J Zhang, G Zhang, R Yan, Y Zhu, X Qi
[ISOLA] Static Optimal Scheduling and Mapping of Synchronous Dataflow Graphs on a Heterogeneous Multiprocessor Platform with Model Checking - XY Zhu, R Yan, YL Gu, G Zhang

2013

[TASE] Assume-guarantee reasoning with local specifications - A Lomuscio, B Strulo, N Walker, P Wu
[JSA] Communication pipelining for code generation from Simulink models - R Yan, K Huang, M Yu, X Zhang
[SCIENCE] High throughput VLSI architecture for H. 264/AVC context-based adaptive binary arithmetic coding (CABAC) decoding - K Huang, D Ma, R Yan, H Ge, X Yan
[SPE] In quest of the science in statistical fault localization - WK Chan, Y Cai
[FSE] Lock trace reduction for multithreaded programs - Y Cai, WK Chan
[JSA] Performance estimation techniques with mpsoc transaction-accurate models - D Ma, R Yan, K Huang, M Yu, S Xiu, H Ge, X Yan, AA Jerraya
[TSE] Prioritizing structurally complex test pairs for validating WS-BPEL evolutions - L Mei, Y Cai, C Jia, B Jiang, WK Chan
[TSE] Taming deadlocks in multithreaded programs - Y Cai, WK Chan, YT Yu
[SIGPLAN] TeamWork: synchronizing threads globally to detect real deadlocks for multithreaded programs - Y Cai, K Zhai, S Wu, WK Chan
[IJWSR] Test pair selection for test case prioritization in regression testing for WS-BPEL programs - L Mei, Y Cai, C Jia, B Jiang, WK Chan

2012

[ASE] A dynamic deadlock prediction, confirmation and fixing frame-work for multithreaded programs - Y Cai
[ATVA] Distributed Priority Synthesis - CH Cheng, R Yan, S Bensalem, H Ruess
[ISOLA] Distributed priority synthesis using knowledge - CH Cheng, R Yan, H Ruess, S Bensalem
[ICSE] MagicFuzzer: Scalable deadlock detection for large-scale applications - Y Cai, WK Chan
[ICESS] Static and dynamic verifying method based on extended finite automata for service compositions - GQ Zhang, HJ Di, HJ Shi, RJ Yan, XY Zhu

2011

[TECS] A formal approach for incremental construction with an application to autonomous robotic systems - S Bensalem, L De Silva, A Griesmayer, F Ingrand, A Legay, R Yan
[HRI] A Verifiable and Correct-by-Construction Controller for Robot Functional Levels - RY Saddek Bensalem, Lavindra De Silva, Felix Ingrand
[CONCUR] Algorithms for synthesizing priorities in component-based systems - CH Cheng, S Bensalem, YF Chen, R Yan, B Jobstmann, H Ruess, ...
[CAV] D-finder 2: Towards efficient correctness of incremental design - S Bensalem, A Griesmayer, A Legay, TH Nguyen, J Sifakis, R Yan
[ICESS] Distributed Priority Synthesis and its Applications - CH Cheng, S Bensalem, R Yan, H Ruess, C Buckl, A Knoll
[ICSE] LOFT: redundant synchronization event removal for data race detection - Y Cai, WK Chan
[NASA] Model construction and priority synthesis for simple interaction systems - CH Cheng, S Bensalem, B Jobstmann, R Yan, A Knoll, H Ruess

2010

[JS] A refinement checking method of web services composition - G Zhang, M Rong, Y He, X Zhu, R Yan
[TASE] Incremental component-based construction and verification using invariants - S Bensalem, M Bozga, A Legay, TH Nguyen, J Sifakis, R Yan
[FTSCS] Incremental invariant generation for compositional design - S Bensalem, A Legay, TH Nguyen, J Sifakis, R Yan
[FAC] Model checking optimisation based congestion control algorithms - A Lomuscio, B Strulo, NG Walker, P Wu
[IARP] Verifiable and correct-by-construction controller for robots in human environments - S Bensalem, L da Silva, M Gallien, F Ingrand, R Yan

2010年以前

[SETTA] Verification, model checking, Markov processes, stochastic processes. - G Norman, C Palamidessi, D Parker, P Wu
[TSE] Model checking probabilistic and stochastic extensions of the π-calculus - G Norman, C Palamidessi, D Parker, P Wu
[SPIN] Truly bitstate-hashing for scc-based emptiness checking algorithms - RJ Yan, WL Zhang, ZS Tang
[QEST] Gethin Norman, Catuscia Palamidessi, David Parker, Peng Wu. Model checking the probabilistic pi-calculus. 4th International Conference on the Quantitative Evaluation of SysTems … - G Norman, C Palamidessi, D Parker, P Wu
[SETTA] Improvements for the Symbolic Verification of Timed Automata - R Yan, G Li, W Zhang, Y Peng
[CONCUR] Symbolic bisimulations for probabilistic systems - P Wu, C Palamidessi, H Lin
[ICSE] Symbolic test generation using a temporal logic with constrained events - D Liu, P Wu, H Lin
[ISOLA] Translating the Probabilistic p-calculus to PRISM, Technical Report CSR-07-2 - G Norman, C Palamidessi, D Parker, P Wu
[SCHOOL] Translating the probabilistic pi-calculus to PRISM - G Norman, C Palamidessi, D Parker, P Wu
[ISOLA] Measuring anonymity with relative entropy - Y Deng, J Pang, P Wu
[TASE] Model-based testing of concurrent programs with predicate sequencing oonstraints - W Peng, L Huimin
[SETTA] Reachability checking of finite precision timed automata - Y RJ, L GY, X YB, L CM, T ZS
[ICSE] Analyzing interoperability of protocols using model checking - P Wu
[ISCAS] Compositional analysis of mobile network protocols - P Wu, D Zhang
[FORTE] Compositional Modelling and Verification of IPv6 Mobility - P Wu, D Zhang
[JS] 关于蜕变测试和特殊用例测试的实例研究 - 吴鹏，施小纯，唐江峻，林惠民，陈宗岳
[ICCC] Compositional analysis of mobile IP with symbolic transition graphs - P Wu, D Zhang
[JOURNAL] Component-based software architecture refinement and its application - R Yan, G Zhang
[SPIN] Interpreting π-calculus with Spin/Promela - P Wu
[FORTE] Validation, implementation and conformance testing of Bluetooth SDP - P Wu