Regular properties are widely used in software analysis and verification. It is challenging to effectively check a regular property of a program. RGSE is a regular property guided dynamic symbolic execution (DSE) engine, for finding a Java program path satisfying a regular property as soon as possible. The key idea is to evaluate the candidate branches based on the history and future information, and explore the branches along which the paths are more likely to satisfy the property in priority.

RGSE is presented in [1]. The technique implemented by RGSE was presented in [2].


Demonstration Video


Please feel free to contact us if you have any problem.

[1]. Hengbiao Yu, Zhenbang Chen, Yufeng Zhang, Ji Wang, Wei Dong. RGSE: A Regular Property Guided Symbolic Executor for Java, in 11th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2017), Tool Demo, ACM Press, pp: 954-958. (PDF)
[2]. Yufeng Zhang, Zhenbang Chen, Ji Wang, Wei Dong, Zhiming Liu. Regular Property Guided Dynamic Symbolic Execution, in 37th IEEE/ACM International Conference on Software Engineering (ICSE 2015), IEEE Press, pp: 643-653. (PDF)