VERDS

Princples and Techniques

Wenhui Zhang.
QBF Encoding of Temporal Properties and QBF-Based Verification.
IJCAR 2014 (LNAI 8562):224-239. Springer International Publishing Switzerland (2014).

Wenhui Zhang,
Bounded Semantics.
Theor. Comput. Sci. 564(2015):1-29.

Zhaowei Xu, Wenhui Zhang.
Linear Templates of ACTL Formulas with an Application to SAT-based Verification.
Information Processing Letters 127(2017):6-16.

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.

Applications and Extensions

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, 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) August 25-27, 2021, Shanghai, China.

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).

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.

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.
Formal Verification of SystemC Designs Using VERDS.
Proceedings of the 20th Asia-Pacific Software Engineering Conference (APSEC 2013): 371-379.

Lanlan Zhang.
Model checking method on subset of C language based on VERDS.
Comput Syst Appl 22(11):19-25,18.