Most of the papers available from this document appear in print, and the corresponding copyright is held by the publisher. While the papers can be used for personal use, redistribution or reprinting for commercial purposes is prohibited.
Hongyu Fan, and Fei He, Leveraging Datapath Propagation in IC3 for Hardware Model Checking, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, accepted, 2024. pdf
Fengmin Zhu, Xingyu Xie, Dongyu Feng, Na Meng and Fei He, On the Methodology of Three-Way Structured Merge in Version Control Systems: Top-Down, Bottom-Up, or Both, Journal of Systems Architecture, Vol. 145, December 2023, 103011. DOI pdf artifact
Hongyu Fan, Zhihang Sun and Fei He, Satisfiability Modulo Ordering Consistency Theory for SC, TSO, and PSO Memory Models, ACM Transactions on Programming Languages and Systems (TOPLAS), 2023, 45 (1), Article 6, 37 pages. DOI pdf
Bowen Shen, Muhammad Ali Gulzar, Fei He and Na Meng. A Characterization Study of Merge Conflicts in Java Projects. ACM Transactions on Software Engineering and Methodology (TOSEM), March 2023, 32 (2), Article 40, 28 pages. DOI
Fei He, Qianshan Yu and Liming Cai, Efficient Summary Reuse for Software Regression Verification, IEEE Transactions on Software Engineering, April 2022, 48(4): 1417-1431. DOI pdf 中文介绍 artifact
Jianhui Chen, Fei He, Leveraging Control Flow Knowledge in SMT Solving of Program Verification, ACM Transactions on Software Engineering and Methodology (TOSEM), May 2021, 30 (4), Article 41, 26 pages. DOI pdf
Chen Luo, Fei He, Fei Peng, Dong Yan, Dan Zhang and Xin Zhou, PSpec-SQL: Enabling Fine-Grained Control for Distributed Data Analytics, IEEE Transactions on Dependable and Secure Computing, 2021, 18 (2): 810-824. DOI pdf
Chen Luo, Fei He, SMT-Based Query Tracking for Differentially Private Data Analytics Systems, Frontier of Computer Science, 2018, 12 (6): 1192-1207. pdf
Fei He, Yuan Gao and Liangze Yin, Efficient Software Product-Line Model Checking using Induction and a SAT-Solver, Frontier of Computer Science, 2018, 12 (2): 264-279. pdf
Liangze Yin, Wei Dong, Fei He and Ji Wang, A True-Concurrency Encoding for BMC of Compositional Systems, The Computer Journal, 2017 July: 1-14.
Chen Luo, Fei He and Carlo Ghezzi, Inferring Software Behavioral Models with MapReduce (extended version), Science of Computer Programming, vol. 145, pp. 13-36, Oct. 2017. pdf
Fei He, Xiaowei Gao, Miaofei Wang, Bow-Yaw Wang and Lijun Zhang, Learning Weighted Assumptions for Compositional Verification of Markov Decision Processes (journal version of the POPL’15 paper), ACM Transactions on Software Engineering and Methodology (TOSEM), 25 (3), Article 21 (June 2016), 39 pages. pdf
Dexi Wang, Fei He, Yangdong Deng, Chao Su, Ming Gu, and Jiaguang Sun, Deadlock detection in FPGA design: a practical way, Tsinghua Science & Technology, 20(2), pp. 212-218, January 2015. pdf
Fei He, Xiaoyu Song, Ming Gu and Jiaguang Sun, Generalized Interface Automata with Multicast Synchronization, Frontier of Computer Sciences, 9(1), pp. 1-14, Feb. 2015. pdf
Min Zhou, Fei He, Xiaoyu Song, Shi He, Gangyi Chen, Ming Gu. Estimating the Volume of Solution Space for Satisfiability Modulo Linear Real Arithmetic. Theory of Computing Systems, 56(2), pp. 347-371, Feb. 2015. pdf
Hui Kong, Fei He, Xiaoyu Song, Ming Gu, Hongyan Tan and Jiaguang Sun, Safety Verification of Semi-Algebraic Dynamical Systems via Inductive Invariant, Tsinghua Science and Technology, 19(2), pp. 211-222, April, 2014. pdf
Min Zhou, Fei He, Bow-Yaw Wang, Ming Gu and Jiaguang Sun, Array Theory of Bounded Elements and its Applications, Journal of Automated Reasoning, 52(4), pp. 379-405, April, 2014. pdf
Min Zhou, Fei He, Bow-Yaw Wang, Wenrui Meng, Ming Gu and Jiaguang Sun, A unified framework for DPLL(T) + certificates, Journal of Applied Mathematics, vol. 2013, Article ID 964682, 13 pages, 2013. pdf
Liangze Yin, Fei He, William N. N. Hung, Xiaoyu Song and Ming Gu, Maxterm Covering for Satisfiability, IEEE Transactions on Computers, 61(3), pp. 420-426, March, 2012. pdf
Fei He, Xiaoyu Song, William N. N. Hung, Ming Gu and Jiaguang Sun, Integrating Evolutionary Computation with Abstraction Refinement for Model Checking, IEEE Transactions on Computers, vol. 59, no. 1, pp. 116-126, Jan. 2010. pdf
Fei He, Xiaoyu Song, Ming Gu and Jiaguang Sun, Heuristic-Guided Abstraction Refinement, Computer Journal, 52(3), pp. 280-287, May, 2009. pdf
Delong Zhang, Chong Ye and Fei He, P4Inv: Inferring Packet Invariants for Verification of Stateful P4 Programs, INFOCOM 2024, Accepted. pdf artifact
Jiangyi Liu, Fengmin Zhu and Fei He, Automated Ambiguity Detection in Layout-Sensitive Grammars, OOPSLA 2023. DOI pdf artifact
Chong Ye and Fei He, P4b: A Translator from P4 Programs to Boogie, ESEC/FSE 2023 (Tool), December 3-9, 2023. DOI pdf artifact
Zhilei Han and Fei He, Data-driven Recurrent Set Learning For Non-termination Analysis, ICSE 2023, May 14-20, 2023. DOI pdf artifact
Fei He, On SMT Solving for Multi-threaded Program Verification, Keynote, SETTA 2022.
Fengmin Zhu, Xingyu Xie, Dongyu Feng, Na Meng and Fei He, Mastery: Shifted-Code-Aware Structured Merging, SETTA 2022, LNCS 13649, Oct. 27-29, 2022 (Best Paper Award). DOI pdf artifact
Fengmin Zhu and Fei He, EqFix: Fixing LaTeX Equation Errors by Examples, SETTA 2022, LNCS 13649, Oct. 27-29, 2022. DOI pdf artifact
Zhihang Sun, Hongyu Fan and Fei He. Consistency-Preserving Propagation for SMT Solving of Concurrent Program Verification, OOPSLA 2022, October 2022, Article 158, 28 pages. DOI pdf artifact
Fei He, Zhihang Sun and Hongyu Fan, Deagle: An SMT-based Verifier for Multi-threaded Programs (Competition Contribution), TACAS 2022. DOI pdf artifact
Rongchen Xu, Jianhui Chen and Fei He, Data-Driven Loop Bound Learning for Termination Analysis, ICSE 2022, May 2022. DOI pdf artifact
Hongyu Fan, Weiting Liu and Fei He, Interference Relation-Guided SMT Solving for Multi-Threaded Program Verification, PPoPP 2022, April 2022 (Best Paper Award). DOI pdf artifact
Fei He, Zhihang Sun and Hongyu Fan, Satisfiability Modulo Ordering Consistency Theory for Multi-threaded Program Verification, PLDI 2021, June 20-26, 2021. DOI pdf artifact
Fei He and Jitao Han, Termination Analysis for Evolving Programs, OOPSLA 2020, November 2020. DOI pdf artifact
Qianshan Yu, Fei He and Bow-yaw Wang, Incremental Predicate Analysis for Regression Verification, OOPSLA 2020, November 2020. DOI pdf artifact
Rongchen Xu, Fei He and Bow-Yaw Wang, Interval Counterexamples for Loop Invariant Learning, ESEC/FSE 2020, November 2020. DOI pdf artifact
Jianhui Chen and Fei He, Proving Termination by k-Induction, ASE 2020 (NIER), Septermber 2020. pdf
Jianhui Chen and Fei He, Proving Almost-Sure Termination by Omega-Regular Decomposition, PLDI 2020, June 2020. DOI pdf
Fengmin Zhu, Fei He and Qianshan Yu, Proper Tree Matching for Enhancing Precision of Structured Merge, in Proceedings of ICSE 2019 (Companion), Canada, 2019. (Poster) pdf
Jianhui Chen and Fei He, Control Flow-Guided SMT Solving for Program Verification, 33rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2018), Montpellier, France, September 3–7, 2018. (ACM SIGSOFT Distinguished Paper) pdf
Fengmin Zhu and Fei He, Conflict Resolution for Structured Merge via Version Space Algebra, Proceedings of the ACM on Programming Languages, Vol. 2, No. OOPSLA, Article 166 (October 2018), 25 pages. DOI pdf project
Chen Luo, Fei He, Dong Yan, Dan Zhang, Xin Zhou and Bow-Yaw Wang, PSpec: A Formal Specification Language for Fine-Grained Control on Distributed Data Analytics, in Proceedings of ICSE 2017 (Companion), Buenos Aires, Argentina, May 20-28, pp. 300-302, 2017. (Poster) pdf
Fei He, Shu Mao and Bow-Yaw Wang, Learning-based Assume-Guarantee Regression Verification, 28th International Conference on Computer Aided Verification (CAV 2016), Toronto, ON, Canada, July 17-23, pp. 310-328, 2016. pdf
Chen Luo, Fei He and Carlo Ghezzi, Inferring Software Behavioral Models with MapReduce, Symposium on Dependable Software Engineering: Theories, Tools and Applications (SETTA 2015), Nanjing, China, Nov. 4-6, pp. 135-149. Springer, 2015. pdf
Shuo Zhang, Fei He and Ming Gu, VeRV: A Temporal and Data-Concerned Verification Framework for the Vehicle Bus Systems, IEEE INFOCOM 2015, Hong Kong, April 16 – May 1, pp. 1167-1175. IEEE, 2015. pdf
Fei He, Xiaowei Gao, Bow-Yaw Wang and Lijun Zhang, Leveraging Weighted Automata in Composition Reasoning about Concurrent Probabilistic Systems, In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2015), Mumbai, India, January 12-18, pp. 503-514. ACM, 2015. pdf
Fei He, Bow-Yaw Wang, Liangze Yin, and Lei Zhu, Symbolic Assume-Guarantee Reasoning through BDD Learning, 36th International Conference on Software Engineering (ICSE 2014), Hyderabad, India, May 31 – June 7, pp. 1071-1082, 2014. pdf
Liangze Yin, Fei He, Ming Gu and Jiaguang Sun, Clause Replication and Reuse in Incremental Temporal Induction, ICECCS 2014, Tianjin, China, 4-7 Aug, pp. 108-115, 2014. pdf
Hui Kong, Fei He, Xiaoyu Song, William N. N. Hung and Ming Gu, Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid Systems, 25th International Conference on Computer Aided Verification (CAV 2013), Saint Petersburg, Russia, July 13-19, pp. 242–257, 2013. pdf
Liangze Yin, Fei He and Ming Gu, Reusing Search Tree for Incremental SAT Solving of Bounded Model Checking, International Conference on Engineering of Complex Computer Systems (ICECCS 2013), 2013, pp. 85-92. pdf
Fei He, Liangze Yin, Bow-Yaw Wang, Lianyi Zhang, Guanyu Mu and Wenrui Meng, VCS: A Verifier for Component-Based Systems, 11th International Symposium on Automated Technology for Verification and Analysis (ATVA 2013), Hanoi, Vietnam, Oct. 15-18, pp. 478-481, 2013. tool paper pdf
Liangze Yin, Fei He and Ming Gu, Optimizing the SAT Decision Ordering of Bounded Model Checking by Structural Information, 7th International Symposium on Theoretical Aspects of Software Engineering (TASE 2013), 2013, pp. 23-26. pdf
Min Zhou, Hai Wan, Chen Su, Liangze Yin, Lianyi Zhang, Fei He, Ming Gu, Jiaguang Sun. Component-based Modeling and Code Synthesis for Cyclic Programs, the 37th International Conference on Computer, Software and Applications (COMPAC 2013). Kyoto, Japan, July 22-26, pp. 569-578, 2013. best paper award
Wenrui Meng , Fei He, Bow-Yaw Wang, and Qiang Liu, Thread-Modular Model Checking with Iterative Refinement, 4th International Conference on NASA Formal Methods (NFM 2012), Norfolk, Virginia, USA, April 3 – 5, 2012, pp. 237-251. pdf
Min Zhou, Fei He and Ming Gu, An Efficient Resolution Based Algorithm for Satisfiability Problem. 5th IEEE International Conference on Theoretical Aspects of Software Engineering (TASE 2011), Xi’an, China, August 29 - 31, 2011, pp. 60–67. pdf
Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Fei He, Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang, and Lei Zhu, Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning, 4th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA 2010), Heraklion, Crete, Greece, October 18-21, 2010, pp. 643–657. pdf
Fei He, He Zhu, William N. N. Hung, Xiaoyu Song and Ming Gu, Compositional Abstraction Refinement for Timed Systems, 2010 4th IEEE International Symposium on Theoretical Aspects of Software Engineering, August 25- 27, 2010, pp. 168-176. pdf
Min Zhou, Fei He, Bow-Yaw Wang, Ming Gu, On Array Theory of Bounded Elements, 22nd International Conference on Computer Aided Verification (CAV 2010), Edinburgh, UK, July 15-19, pp. 570-584, 2010. pdf
He Zhu, Fei He, William N. N. Hung, Xiaoyu Song and Ming Gu, Data Mining Based Decomposition for Assume-Guarantee Reasoning, 9th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2009), Austin, TX, USA, Nov. 15-18, pp. 116-119, 2009. pdf
Min Zhou, Fei He, Ming Gu and Xiaoyu Song, Translation-based model checking for PLC programs, 33rd Annual IEEE International Computer Software and Applications Conference (COMPSAC 2009), Seattle, Washington, USA, July 20-24, pp. 553-562, 2009.
Fei He, Luciano Baresi, Carlo Ghezzi and Paola Spoletini, Formal Analysis of Publish-Subscribe Systems by Probabilistic Timed Automata, 27th IFIP WG 6.1 International Conference on Formal Methods for Networked and Distributed Systems (FORTE 2007), Tallinn, Estonia, June 27-29, pp. 247-262, 2007. pdf
Fei He, Xiaoyu Song, Ming Gu and Jiaguang Sun, A Probabilistic Learning Approach for Counterexample Guided Abstraction Refinement, Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis (ATVA 2006), LNCS 4218, Beijing, China, October 23-26, pp. 39-50, 2006. pdf
Anduo Wang, Fei He, Ming Gu and XiaoYu Song, Verifying Java Programs by Theorem Prover HOL, 30th Annual International Computer Software and Applications Conference (COMPSAC 2006), Chicago, US, September 17-21, pp. 139-142, 2006.
Back to the homepage of Fei He.