Peng WU

Peng WU	Associate Research Professor Ph.D. in Computer Software and Theory, 2005
`Contact Address:`	`Lab of Computer Science, P.O.Box 8718, Beijing 100190, China`
`Office:`	`Room 325, Building 5#, Institute of Software, Chinese Academy of Sciences 4 South Fourth Street, ZHONGGUANCUN, Beijing 100190, China`
`Telephone:`	`+86 (10) 6266 1622 Fax: +86 (10) 6266 1627`
`Email:`	`wp (at) ios (dot) ac (dot) cn`

I am looking for 2 master students in software analysis, verification and testing, and machine learning. If interested, please contact me.

Research Interests: Concurrency, Model Checking, Software Testing, Machine Learning

Publications (DBLP Journals Proceedings Reports Theses) - Software - Links

Journals

Zhen Zhang, Peng Wu, Yuting Yang, Xuran Li. Interpreting Deep Neural Networks via Relative Activation-Deactivation Abstractions. ACM Transactions on Software Engineering and Methodology, 2025
Yibo Dai, Li Xie, Peng Wu, Shecheng Cui, Linhai Ma. Intrathread Method Orders Based Adaptive Testing of Concurrent Objects. Science of Computer Programming, 248: Article 103362, 2026
Kaixiang Dong, Peng Wu, Yanting Chen. Boosting Generalizable Fairness with Mahalanobis Distances Guided Boltzmann Exploratory Testing. IEEE Transactions on Software Engineering, 51(8): 2213 - 2231, 2025
Chang-Ai Sun, Hepeng Dai, Ning Geng, Huai Liu, Tsong Yueh Chen, Peng Wu, Yan Cai, and Jinqiu Wang. An Interleaving Guided Metamorphic Testing Approach for Concurrent Programs. ACM Transactions on Software Engineering and Methodology 33(1), Article 8, 21 pages, 2024
王超, 吕毅, 吴鹏, 贾巧雯. TSO内存模型下限界可线性化的可判定性研究. 软件学报 33(8): 2896–2917, 2022
Chang-ai Sun, An Fu, Yiqiang Liu, Qing Wen, Zuoyi Wang, Peng Wu, Tsong Yueh Chen. An Iterative Metamorphic Testing Technique for Web Services and Case Studies. International Journal of Web and Grid Services, 16(4), online, 2020
Linhai Ma, Peng Wu, Tsong Yueh Chen. Diversity driven adaptive test generation for concurrent data structures. Information & Software Technology, 2018, 103: 162-173
Chao Wang, Yi Lv, Peng Wu. TSO-to-TSO linearizability is undecidable. Acta Informatica, 2018, 55(8): 649-668
Chao Wang, Yi Lv, Peng Wu. Decidability of linearizabilities for relaxed data structures. SCIENCE CHINA Information Sciences, 2018, 61(1): 012103:1-012103:10
Zhenya Zhang, Peng Wu, Yu Zhang. Localization of Linearizability Faults on the Coarse-Grained Level. International Journal of Software Engineering and Knowledge Engineering, 2017, 27(9&10): 1483-1505
Alessio Lomuscio, Ben Strulo, Nigel G. Walker, Peng Wu. Assume-Guarantee Reasoning with Local Specifications. International Journal of Foundations of Computer Science, 2013, 24(4): 419-444 [abstract+full-text]
Alessio Lomuscio, Ben Strulo, Nigel G. Walker, Peng Wu. Model Checking Optimisation-Based Congestion Control Algorithms. Fundamenta Informaticae, 2010, 102(1): 77 - 96 [abstract+full-text]
Gethin Norman, Catuscia Palamidessi, David Parker and Peng Wu. Model Checking Probabilistic and Stochastic Extensions of the Pi-calculus. IEEE Transactions on Software Engineering, 2009, 35(2): 209 - 223 [full-text][MMCsp]
Peng Wu, Huimin Lin, Model-Based Testing of Concurrent Programs with Predicate Sequencing Constraints. International Journal of Software Engineering and Knowledge Engineering, 2006, 16(5): 727 - 746 [abstract+full-text/WorldScientific][PSCL]
Peng Wu. Analyzing Interoperability of Protocols Using Model Checking. The Chinese Journal of Electronics, 2005, 14(3): 453 - 457 (A preliminary version was accepted by the 1st International Workshop on Automated Technology for Verification and Analysis (ATVA 2003), National Taiwan University, Dec. 10 - 13, 2003)
Peng Wu, Xiaochun Shi, Jiangjun Tang, Huimin Lin, T. Y. Chen. Metamorphic Testing and Special Case Testing: A Case Study. Journal of Software, 2005, 16(7): 1210 - 1220 [abstract + full-text][MTest]
Peng Wu. Interpreting pi-Calculus with Spin/Promela. Computer Science, 2003, 8: 7 - 9, Supplement(the Proceedings of National Conference on Theoretical Computer Science, Qingdao, China, Aug. 3 - 7, 2003 [An English version][pi2promela]
Peng Wu, Qiang Gao, Implementation of Home Networking: Technical Research, Accepted by Computer Engineering and Application, 2001

Conferences & Workshop Proceedings

Yibo Dai, Peng Wu, Shecheng Cui and Linhai Ma. Intrathread Method Orders based Adaptive Testing of Concurrent Objects. 18th Theoretical Aspects of Software Engineering Conference (TASE 2024), to appear
Qiaowen Jia, Yi Lv, Peng Wu, Bohua Zhan, Jifeng Hao, Hong Ye, Chao Wang. VeriLin: A Linearizability Checker for Large-Scale Concurrent Objects. 17th International Symposium on Theoretical Aspects of Software Engineering (TASE 2023), 202-220
Xuran Li, Peng Wu, Jing Su. Accurate Fairness: Improving Individual Fairness without Trading Accuracy. 37th AAAI Conference on Artificial Intelligence (AAAI-23), 14312-14320
Jing Su, Zhen Zhang, Peng Wu, Xuran Li and Jian Zhang. Adversarial Input Detection Based on Critical Transformation Robustness, 33rd International Symposium on Software Reliability Engineering (ISSRE 2022), 390-401
Zhen Zhang, Peng Wu, Yuhang Chen, Jing Su. Out-of-Distribution Detection through Relative Activation-Deactivation Abstractions, 32nd International Symposium on Software Reliability Engineering (ISSRE 2021), 150-161
Wentao Xie and Peng Wu. Fairness Testing of Machine Learning Models Using Deep Reinforcement Learning. 19th IEEE International Conference on Trust, Security and Privacy in Computing and Communications (TrustCom 2020), 121-128
Yang Chen, Zhenya Zhang, Peng Wu, Yu Zhang. Interleaving-Tree Based Fine-Grained Linearizability Fault Localization. 4th International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2018), LNCS 10998, 108-126
Zhenya Zhang, Peng Wu and Yu Zhang. Localization of Linearizability Faults on the Coarse-grained Level. 29th International Conferences of Software Engineering and Knowledge Engineering (SEKE 2017), 272–277
Chao Wang, Yi Lv, Peng Wu. Decomposable Relaxation for Concurrent Data Structures. 43rd International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2017), 188-202
Chao Wang, Yi Lv and Peng Wu. Bounded TSO-to-SC Linearizability is Decidable. 42nd International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2016), 404-417
Wei Ji, Farn Wang, Peng Wu and Yi Lv. An Experiment on Decision Diagrams for Model Checking Probabilistic Timed Automata. 21st International Conference on Engineering of Complex Computer Systems (ICECCS 2016), 111-121
Qian Zhang, Ying Jiang and Peng Wu. Modelling and Analysis of Network Security - an Algebraic Approach. 15th IEEE International Conference on Trust, Security and Privacy in Computing and Communications (IEEE TrustCom-16), 308-315
Han Yue, Peng Wu, Tsong-Yueh Chen and Yi Lv. Input-driven Active Testing of Multi-threaded Programs. Asia-Pacific Software Engineering Conference (APSEC 2015), pp. 246-253 [Maple-IDAT]
Chao Wang, Yi Lv, Gaoang Liu and Peng Wu. Quasi-Linearizability is Undecidable. 13rd Asian Symposium on Programming Languages and Systems (APLAS 2015), LNCS 9458, pp.369-386
Chao Wang, Yi Lv and Peng Wu. TSO-to-TSO Linearizability is Undecidable. 13rd International Symposium on Automated Technology for Verification and Analysis (ATVA 2015), LNCS 9364, pp. 309–325
Yi Lv, Luming Sun, Xiaochun Ye, Dongrui Fan and Peng Wu. Efficiently and Completely Verifying Synchronized Consistency Models. 12nd International Symposium on Automated Technology for Verification and Analysis (ATVA 2014), LNCS 8837, pp 264-280
Alessio Lomuscio, Ben Strulo, Nigel G. Walker, Peng Wu. Assume-Guarantee Reasoning with Local Specifications. In Proc. 12th International Conference on Formal Engineering Methods (ICFEM 2010), LNCS 6447, pp. 204 - 219, Shanghai, China, Nov. 17 - 19, 2010 [abstract + full-text/SpringerLink]
Alessio Lomuscio, Ben Strulo, Nigel G. Walker, Peng Wu. Model Checking Optimisation-Based Congestion Control Models. In the Proceedings of the 12th International Workshop on Concurrency, Specification and Programming (CS&P 2009), pp. 386 - 397, Krakow, Poland, Sep. 28 - 30, 2009 [full-text]
Peng Wu, Catuscia Palamidessi and Huimin Lin. Symbolic Bisimulations for Probabilistic Systems. In the proceedings of the 4th International Conference on the Quantitative Evaluation of SysTems (QEST 2007), pp. 179 - 188, Edinburgh, Scotland, Sep. 16 - 19, 2007 [report version]
Gethin Norman, Catuscia Palamidessi, David Parker and Peng Wu. Model Checking the Probabilistic pi-Calculus. In the proceedings of the 4th International Conference on the Quantitative Evaluation of SysTems (QEST 2007), pp. 169 - 178, Edinburgh, Scotland, Sep. 16 - 19, 2007 [full-text][MMCsp]
Peng Wu, Daguang Liu and Huimin Lin. Symbolic Test Generation Using a Temporal Logic with Constrained Events. Position Paper. In the Proceedings of the 19th IFIP International Conference on Testing of Communicating Systems and the 7th International Workshop on Formal Approaches to Testing of Software (TESTCOM/FATES 2007), Tallinn, Estonia, Jun. 26-29, 2007 [PSCL]
Yuxin Deng, Jun Pang, Peng Wu. Measuring Anonymity with Relative Entropy. In the Proceedings of the 4th International Workshop on Formal Aspects in Security and Trust (FAST 2006), LNCS pp. 65 - 79, Ontario, Canada, Aug. 26 - 27, 2006
Peng Wu, Dongmei Zhang. Compositional Modelling and Verification of IPv6 Mobility. In the Proceedings of the 25th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE 2005), LNCS 3731, pp. 553 - 556, National Taiwan University, Oct. 2 - 5, 2005 [abstract + full-text/SpringerLink]
Peng Wu, Huimin Lin. Model-Based Testing of Concurrent Programs with Predicate Sequencing Constraints. In the Proceedings of the 5th International Conference On Quality Software (QSIC 2005), pp. 3 - 10, Melbourne, Australia, Sep. 19 - 20, 2005 [abstract + full-text/IEEE][PSCL]
Peng Wu. Iterative Metamorphic Testing. In the Proceedings of 29th Annual International Computer Software and Applications Conference(COMPSAC 2005), pp. 19 - 24, Edinburgh, UK, Jul. 26 - 28, 2005 [abstract + full-text/IEEE][MTest]
Peng Wu, Dongmei Zhang. Compositional Analysis of Mobile Network Protocols. Accepted by International Workshop on Software Verification and Validation (SVV 2004), Seattle, USA, Nov. 8, 2004
Peng Wu, Dongmei Zhang. Compositional Analysis of Mobile IP with Symbolic Transition Graph. In the Proceedings of 16th International Conference on Computer Communication (ICCC 2004), pp.1481 - 1488, Beijing, China, Sep. 15 - 17, 2004 [full-text]
Peng Wu, Jiangjun Tang, Xiaochun Shi. Software Reliability Model and Engineering. In the Proceedings of National Conference on Reliability Technologies in National Defense Industry, pp.134 - 141, Beijing, China, Nov. 4 - 7, 2003
Peng Wu, Qiang Gao. Incompleteness of Bluetooth Protocol Conformance Test Cases. In the Proceedings of SPIE, Conference on Asia-Pacific Optical and Wireless Communications: Wireless and Mobile Communications (APOC 2001), Vol.4586, pp.266 - 273, Beijing, China, Nov. 12 - 15 [abstract + full-text/SPIE]

Technical Reports

Alessio Lomuscio, Ben Strulo, Nigel G. Walker, Peng Wu. Assume-Guarantee Verification for Distributed Systems with Local Specifications. Research Note RN/10/01, Department of Computer Science, University College London. February 2010 [full-text]
Alessio Lomuscio, Ben Strulo, Nigel G. Walker, Peng Wu. Model Checking Optimisation-Based Congestion Control Models. Research Note RN/09/02, Department of Computer Science, University College London. March 2009 [full-text]
Gethin Norman, Catuscia Palamidessi, David Parker and Peng Wu. Translating the Probabilistic pi-Calculus to PRISM. Technical Report CSR-07-02, School of Computer Science, University of Birmingham. March 2007 [full-text]
Peng Wu, Dongmei Zhang. Compositional Analysis of Mobile Network Protocols. Technical Report ISCAS-LCS-05-02, Lab of Computer Science, Institute of Software, Chinese Academy of Sciences, March 2005 [full-text]

Theses

Peng Wu, Model Checking and Testing of Concurrent Systems, Ph.D. Thesis, Jun. 28, 2005 [abstract]
Peng Wu, Validation, Implementation and Conformance Testing of Bluetooth SDP, M.S. Thesis, Jun. 2001 [abstract]

Software

Pi2promela [download+manual][reference], a compiler from pi-calculus to Promela.
MTest [reference 1 2], an integrated metamorphic testing environment that supports special case tesing, random testing and n-iterative metamorphic testing.
PSCL-Based Symbolic Test Generator [download+manual][reference 1 2 3], a symbolic test case generator based on predicate sequencing constraint logic(PSCL).
MMCsp [download+manual][reference 1 2], an extension of MMC for a simple probabilistic pi-calculus.
Maple-IDAT Input-Driven Active Testing of Multithreaded Programs, based on Maple.

Links

Projects: Printemp (Information Theory, Anonymity), ProNoBis (Probabilistic pi-Calculus, Model Checking), Bedwyr (Case Study: Value-Passing CCS, pi-Calculus, Bisimulation, MUTE)
COMPSAC'05 ETAPS'06 POPL'07 TESTCOM/FATES'07 QEST'07 FCST'09 CS&P'09 Dagstuhl Seminar 10051 ICFEM'10