Wenhui Zhang.
First order Büchi automata and their application to verification of
LTL specifications.
J. Log. Algebraic Methods Program. 142 (2025) 101021, 1-31.
DOI: 10.1016/j.jlamp.2024.101021
Freely accessible before December 07, 2024
Zhaowei Xu, Wenhui Zhang.
Linear Templates of ACTL Formulas with an Application to SAT-based Verification.
Information Processing Letters 127(2017)6-16.
Long Teng, Wenhui Zhang.
Termination analysis with recursive calling graphs.
Journal of Network and Computer Applications 59:109–116. 2016.
Zhaowei Xu, Yuefei Sui, Wenhui Zhang.
Completeness of Hoare Logic with inputs over the Standard Model.
Theor. Comput. Sci. 612:23–28. 2016.
麻婧、张文辉.
AKC攻击研究：攻击方式、转换算法和实例分析.
计算机系统应用 25(10):18-26. 2016.
Wenhui Zhang.
Bounded Semantics.
Theor. Comput. Sci. 564:1-29. 2015.
Yanyan Xu, Wei Chen, Kaile Su, Wenhui Zhang.
Greedy Clique Decomposition for Symbolic Satisfiability Solving.
International Journal of Advancements in Computing Technology 4(10):174-184. 2012.
Liang Xu, Wei Chen, Yanyan Xu, Wenhui Zhang.
Improved Bounded Model Checking for Universal Fragment of CTL.
Journal of Computer Science and Technology 24(1):96-109. 2009.
Syed Asad Raza Kazmi, Wenhui Zhang.
Compositional Reasoning in Intuitionistic Linear-Time μ-Calculus.
Journal of Software (软件学报). 20(8):2026-2036 , 2009.
Wei Chen, Wenhui Zhang.
A Direct Construction of Polynomial-size OBDD Proof of Pigeon Hole Problem.
Information Processing Letters 109(10):472-477. 2009.
Syed Asad Raza Kazmi, Wenhui Zhang.
Intuitionistic Linear-time mu-Calculus. Journal of Software (软件学报) 19(12):3122-3133, 2008.
Jian Zhang, Wenhui Zhang, Naijun Zhan, Yi-Dong Shen, Haiming Chen, Yunquan Zhang, Yongji Wang,
Enhua Wu, Hongan Wang, Xueyang Zhu:
Basic research in computer science and software engineering at SKLCS.
Frontiers of Computer Science in China 2(1): 1-11 (2008)
Xiang-Yun Wang, Wenhui Zhang, Yong-Chao Li and Kai-Yuan Cai.
A polynomial dynamic system approach to software design for attractivity requirement.
Information Sciences 177(13):2712-2725. Elsevier, 2007.
Fei Pu and Wenhui Zhang.
Combining search space partition and abstraction for LTL model checking.
Science in China, Series F, vol. 50(6):793-810. 2007.
王向云、张文辉、王鹏、李永超、蔡开元。
一种基于监控理论的软件设计方法：状态性质变换方法。
控制理论与应用24（2）：187-192.2007。
Zhilin Wu, Wenhui Zhang.
The Complexity of Dual Models Problem of Propositional Linear Temporal Logic.
Journal of Software (软件学报) 18(7):1573-1582. 2007.
Wenhui Zhang.
Structure of Proofs and the Complexity of Cut Elimination.
Theoretical Computer Science 353(1-3):63-70. Elsevier, 2006.
易锦，张文辉.
基于迁移的扩展Buchi自动机到Buchi自动机的有效转换.
软件学报17(4)720-728. 2006.
张文辉.
模态逻辑与模型检测.
中国计算机学会通讯 1(2):22-26. 2005.
Wenhui Zhang.
Combining static analysis and case-based search space partitioning for reducing peak memory in model checking.
Journal of Computer Science and Technology 18(6):762-770, 2003.
林惠民，张文辉。
模型检测：理论、方法与应用.
电子学报 30(12A):1907-1912. 2002.
Analysis trees as a mechanical proof method.
Chinese Journal of Advanced Software Research 4(2):171-179, 1997.
Wenhui Zhang.
Number of models and satisfiability of sets of clauses.
Theoretical Computer Science 155(1):277-288, 1996.
Wenhui Zhang.
Verification of XYZ/SE programs.
Chinese Journal of Advanced Software Research 2(4):364-373, 1995.
Wenhui Zhang.
Depth of proofs, depth of cut-formulas and complexity of cut formulas.
Theoretical Computer Science 129(1):193-206, 1994.
Wenhui Zhang.
Cut formulas in propositional logic.
Theoretical Computer Science 120(1):157-168, 1993.
Renwei Li, Pei He and Wenhui Zhang.
An introduction to INCAPS system.
Journal of Computer Science and Technology 8(1):26-37, 1993.
Wenhui Zhang.
Cut elimination and automatic proof procedures.
Theoretical Computer Science 91(2):265-284, 1991.
Wenjian Chai, Rongjie Yan, Wenhui Zhang and Jian Zhang.
Slicing Assisted Program Verification: An Empirical Study.
Proceedings of the 18th IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2024, LNCS 14777): 38-57.
July 29 - August 1, 2024, Guiyang, China.
Xufeng Zhao, Qiuyang Wei, Xue-Yang Zhu, Wenhui Zhang.
Template-Based Smart Contract
Verification: A Case Study on Maritime
Transportation Domain.
Proceedings of the
28th International Conference on Engineering of Complex Computer Systems (ICECCS 2024, LNCS 14784), pp. 179-198.
June 19–21, 2024, Limassol, Cyprus.
Qiuyang Wei, Xufeng Zhao, Xue-Yang Zhu, Wenhui Zhang.
Formal Analysis of IBC Protocol.
Proceedings of the
31st IEEE International Conference on Network Protocols
(ICNP 2023): 1-11.
October 10-13, 2023, Reykjavik, Iceland.
Xufeng Zhao, Qiuyang Wei, Xue-Yang Zhu, Wenhui Zhang.
A Smart Contract Development Framework for Maritime Transportation Systems.
IEEE 23rd International Conference on Software Quality, Reliability, and Security, QRS 2023 Companion: 310-319.
October 22-26, 2023, Chiang Mai, Thailand.
Yulong Bao, Xue-Yang Zhu, Wenhui Zhang, Wuwei Shen, Pengfei Sun and Yingqi Zhao.
On Verification of Smart Contracts via Model Checking.
Proceedings of the 16th IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2022，LNCS 13299): 92-112.
July 8-10, 2022, Cluj-Napoca, Romania.
Wenhui Zhang, Ya Gao.
A Bounded Semantics for Improving the Efficiency of
Bounded Model Checking.
Proceedings of the
26th International Conference on Engineering of Complex Computer Systems (ICECCS 2022), pp. 97-106.
March 26-30, 2022, Hiroshima, Japan.
Ya Gao, Wenhui Zhang, Xue-Yang Zhu.
Multi-Agent Automata and Its Application to
LDLK Satisfiability Checking.
Proceedings of the 21th IEEE International Conference on Quality, Reliability and Security (QRS 2021), pp. 1024-1035.
December 6-10, 2021, Hainan, China.
Wenhui Zhang, Xueyang Zhu, Yulong Bao.
VERDS: Modeling and Verification of Finite State Systems with Discrete Time Models by Symbolic Techniques.
The 15th International Symposium on Theoretical Aspects of Software Engineering (TASE 2021): 135-142.
August 25-27, 2021, Shanghai, China.
Wenhui Zhang.
Correctness and Bounded Correctness.
18th IEEE/ACIS International Conference on Computer and Information Science
(ICIS 2019): 2-2.
June 17-19, 2019, Beijing, China
Ran Chen, Wenhui Zhang.
Verification of CTL_BDI Properties by Symbolic Model Checking.
Proceedings of the 26th Asia-Pacific Software Engineering Conference
(APSEC 2019): 102-109.
December 2-5, 2019, Putrajaya, Malaysia.
Ran Chen, Wenhui Zhang.
Checking Multi-Agent Systems against Temporal-Epistemic Specifications.
Proceedings of the 24th International Conference on Engineering of Complex Computer Systems
(ICECCS 2019): 21-30.
November 10-13, 2019, Guangzhou, China.
Pei Huang, Minghao Liu, Ping Wang, Wenhui Zhang, Feifei Ma, Jian Zhang.
Solving the Satisfiability Problem of Modal Logic S5 Guided by Graph Coloring.
Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence (IJCAI 2019): 1093-1100.
August 10-16, 2019, Macao, China.
Xinxin Liu, Tingting Yu, Wenhui Zhang.
Logics for Bisimulation and Divergence.
The 21st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2018, LNCS 10803): 221–237.
14-20 April 2018, Thessaloniki, Greece.
Xinxin Liu, Wenhui Zhang.
Characterization and Verification of Stuttering Equivalence.
LNCS 11180 (Symposium on Real-Time and Hybrid Systems 2017): 116-132. September 2018, Springer.
Changsha, China. October 2017.
Xinxin Liu, Tingting Yu, Wenhui Zhang.
Analyzing divergence in bisimulation semantics.
The 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017),
Jan 18 - 20, 2017, Paris, France. pp. 735-747. 2017.
Zhaowei Xu, Wenhui Zhang, Yuefei Sui.
Completeness of Hoare Logic Relative to the Standard Model.
The 43rd International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2017),
Jan 16–20, 2017, Lero–Limerick, Ireland. LNCS 10139:119-131. 2017.
Xue-Yang Zhu, Rongjie Yan, Yu-Lei Gu, Jiang Zhang, Wenhui Zhang and Guangquan Zhang.
Static Optimal Scheduling for Synchronous Data
Flow Graphs with Model Checking.
FM 2015. June 24-26, 2015, Oslo, Norway.
Wenhui Zhang.
QBF Encoding of Temporal Properties and QBF-Based Verification.
IJCAR 2014 (LNAI 8562):224-239. Springer International Publishing Switzerland (2014).
Naiju Zeng, Wenhui Zhang.
A Symbolic Partial Order Method for Verifying SystemC.
Proceedings of the 21th Asia-Pacific Software Engineering Conference (APSEC 2014):271-278.
Teng Long, Wenhui Zhang.
Termination Analysis with Recursive Calling Graphs.
Proceedings of Computing, Communications & IT Applications Conference (ComComAp 2014):276-282.
Naiju Zeng, Wenhui Zhang.
An Executable Semantics of SystemC Transaction Level Models and Its Applications with VERDS.
Proceedings of the 19th International Conference on Engineering of
Complex Computer Systems (ICECCS 2014):198-201.
Naiju Zeng, Wenhui Zhang.
A SystemC Semantics in Guarded Assignment Systems
and Its Applications with VERDS.
Proceedings of the 20th Asia-Pacific Software Engineering Conference (APSEC 2013):371-379.
Teng Long, Wenhui Zhang.
Proving Liveness Property under Strengthened Compassion Requirements.
Lecture Notes in Computer Science 7287 (TAMC 2012):498-508.
Teng Long, Wenhui Zhang.
Proving Liveness Property under Fairness Requirements.
APSEC 2012: 674-682.
Xanyan Xu, Wei Chen, Kaile Su, Wenhui Zhang.
Solving Difficult SAT Problems by Using OBDDs and Greedy Clique Decomposition.
Lecture Notes in Computer Science 7285 (FAW-AAIM 2012):259-268.
Teng Long, Wenhui Zhang.
Auxiliary Constructs for Proving Liveness in Compassion Discrete Systems.
Lecture Notes in Computer Science 6252 (ATVA 2010):276-290. Springer-Verlag. 2010.
Bowen Chen, Haihua Shen, Wenhui Zhang.
Formula-Oriented Compositional Minimization in Model Checking.
Proceedings of the 19th IEEE Asian Test Symposium (ATS 2010):81-84. IEEE Computer Society. 2010.
Wenhui Zhang.
Bounded Semantics of CTL and SAT-based Verification.
Lecture Notes in Computer Science 5885 (ICFEM 2009):286-305. Springer-Verlag. 2009.
Wei Chen, Wenhui Zhang.
Bounded Model Checking of ACTL formulae .
Proceedings of the 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2009):90-99. 2009.
Wenhui Zhang.
Model Checking with SAT-Based Characterization of ACTL Formulas.
Lecture Notes in Computer Science 4789 (ICFEM’07):191-211. Springer-Verlag. 2007.
Jin Yi, Wenhui Zhang.
Enhancing Simulation for Checking Language Containment.
Lecture Notes in Computer Science 4484 (TAMC’07):374-385. Springer-Verlag. 2007.
Jin Yi, Wenhui Zhang. Efficient State Space Reduction for Automata by Fair Simulation.
Lecture Notes in Computer Science 4767 (FSEN’07):380-387. Springer-Verlag. 2007.
Yanyan Xu, Wei Chen, Liang Xu, Wenhui Zhang.
Evaluation of SAT-based Bounded Model Checking of ACTL Properties.
Proceedings of the 1st Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE'07):339-348. IEEE Computer Society Press. 2007.
Wenhui Zhang.
Verification of ACTL Properties by Bounded Model Checking.
Lecture Notes in Computer Science 4739 (EUROCAST’07):556-563. Springer-Verlag. 2007.
Wenhui Zhang.
SAT-Based Verification of LTL Formulas.
Lecture Notes in Computer Science 4346 (FMICS/PDMC’06):277-292. Springer-Verlag. 2007.
Fei Pu, Wenhui Zhang.
Partition Refinement in Abstract Model Checking.
Proceedings of the 1st Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE'07):209-218. IEEE Computer Society Press. 2007.
Fei Pu, Wenhui Zhang.
LTL Model Checking via Search Space Partition.
Proceedings of the 6th International Conference on Quality Software (QSIC'06):418-428. IEEE Computer Society Press. 2006.
Fei Pu, Wenhui Zhang, Shaochun Wang.
An Improved Case-Based Approach to LTL Model Checking.
Lecture Notes in Computer Science 3943 (RISE’05):190-202. Springer-Verlag. 2006.
Bai Su, Wenhui Zhang.
Search Space Partition and Case Basis Exploration for Reducing Model Checking Complexity.
Lecture Notes in Computer Science 3299 (ATVA’04):34-48. Springer-Verlag. 2004.
Wenhui Zhang, Zhuo Huang and Jian Zhang.
Parallel execution of stochastic search procedures on reduced SAT instances.
Lecture Notes in Computer Science 2417 (PRICAI’02):108-117. Springer-Verlag. 2002.
Einar B. Johnsen, Wenhui Zhang, Olaf Owe and Demissie B. Aredo.
Combining graphical and formal development of open distributed systems.
Lecture Notes in Computer Science 2335 (ICFEM’02):319-338. Springer-Verlag. 2002.
Weiwen Xu, Wenhui Zhang and Xinda Lu.
Formal analysis and verification of distributed grid directory service.
Proceedings of the 5th International Conference on Algorithms and Architecture for Parallel Processing (ICA3PP'02 Vol II):505-509. IEEE Computer Society Press. 2002.
Wenhui Zhang.
A strategy for improving the efficiency of procedure verification.
Lecture Notes in Computer Science 2434 (SAFECOMP’02):113-126. Springer-Verlag. 2002.
Einar B. Johnsen, Wenhui Zhang, Olaf Owe and Demissie B. Aredo.
Specification of Distributed Systems with a Combination of Graphical and Formal Languages.
Proceedings of the 8th Asia-Pacific Software Engineering Conference(APSEC’01):105-108. IEEE Computer Society Press. 2001.
Wenhui Zhang.
Applying SDL specifications and tools to the verification of procedures.
Lecture Notes in Computer Science 2078 (SDL 2001: Meeting UML):421-437. Springer-Verlag. 2001.
Wenhui Zhang, Einar B. Johnsen, Olaf Owe and Demissie B. Aredo.
Integrating UML and OUN for Specification of Open Distributed Systems.
Proceedings of the 2001 IEEE Symposia on Human-Centric Computing Languages and Environments (HCC'01):122-123. IEEE Computer Society Press. 2001.
Wenhui Zhang.
Validation of control system specifications with abstract plant models.
Lecture Notes in Computer Science 1943 (SAFECOMP’00):53-62. Springer-Verlag. 2000.
Wenhui Zhang.
Principles of Applying Model Checking to Verification of Operator Procedures.
Proceedings of the Norwegian Computer Science Conference (NIK'99):339-350. Tapir Forlag, 1999.
Wenhui Zhang.
Model checking operator procedures. (Promela Codes)
Lecture Notes in Computer Science 1680 (SPIN’99):200-215. Springer-Verlag. 1999.
Pei He, Renwei Li, Wenhui Zhang.
Theory and Practice for XYZ/VERI System.
IFIP Transactions A-19 (Automated Reasoning):239-248, North-Holland, 1992.