My research interests include software engineering and automated verification, mainly
focusing on design methodologies, analysis techniques and verification tools for building
highly quality software.
Collaboration with Industry
We have a very close collaboration with industry. We developed useful techniques of
modeling and testing for our industry partners. Our industry partners include:
I jointed the Formal Methods Group led By Prof. Jifeng He in East China Normal
University in 2005, and Since 2012, I became a Professor in School of Computer Science
and Software Engineering. I completed my Ph.D. in Mathematics at Peking University in
July 2005 , and I received a B.S. in Mathematics from Wuhan University.
On Reachability Analysis of Pushdown Systems with Transductions: Application to Boolean Programs with Call-by-Reference.
Fu Song, Weikai Miao, Geguang Pu, Min Zhang.
CONCUR2015, PP 383-397, 2015
SAT-Based Explicit LTL Reasoning.
Jianwen Li, Shufang Zhu, Geguang Pu, Moshe Y. Vardi.
Haifa Verification Conference 2015, pp209-224, 2015
Ke Wu, Shiping Tang, Geguang Pu, Min Wu, Ting Su.
Fm-QCA: A Novel Approach to Multi-value Qualitative Comparative Analysis.
KSEM 2015, pp115-127, 2015
Combining Symbolic Execution and Model Checking for Data Flow Testing.
Ting Su, Zhoulai Fu, Geguang Pu, Jifeng He, Zhendong Su.
ICSE2015, pp654-665, 2015
Formal Development of a Real-Time Operating System Memory Manager.
Wen Su, Jean-Raymond Abrial, Geguang Pu, Bin Fang:
ICECCS 2015, pp130-139, 2015
Modeling and Verifying Google File System.
Bo Li, Mengdi Wang, Yongxin Zhao, Geguang Pu, Huibiao Zhu, Fu Song.
HASE 2015, pp207-214, 2015.
The semantics and verification of timed service choreography.
Yongxin Zhao, Hao Xiao, Zheng Wang, Geguang Pu, Ting Su.
Int. J. Comput. Math., 91(3), pp384-402, 2014
LTLf Satisfiability Checking.
Jianwen Li, Lijun Zhang, Geguang Pu, Moshe Y. Vardi, Jifeng He.
ECAI 2014, pp513-518, 2014
Aalta: an LTL satisfiability checker over Infinite/Finite traces.
Jianwen Li, Yinbo Yao, Geguang Pu, Lijun Zhang, Jifeng He:
SIGSOFT FSE 2014, pp731-734, 2014
Automated Coverage-Driven Test Data Generation Using Dynamic Symbolic Execution.
Ting Su, Geguang Pu, Bin Fang, Jifeng He, Jun Yan, Siyuan Jiang, Jianjun Zhao.
SERE 2014, pp98-107, 2014
Combining Syntactic and Semantic Encoding for LTL Bounded Model Checking.
Wanwei Liu Xiaoguang Mao, Geguang Pu, Rui Wang.
TASE 2014, pp82-89, 2014
Runtime Verification by Convergent Formula Progression.
Yan Shen, Jianwen Li, Zheng Wang, Ting Su, Bin Fang, Geguang Pu, Wanwei Liu, Mingsong Chen.
APSEC (1) 2014, pp255-262, 2014
Efficient Two-Phase Approaches for Branch-and-Bound Style Resource Constrained Scheduling.
Mingsong Chen, Fan Gu, Lei Zhou, Geguang Pu, Xiao Liu.
VLSI Design 2014, pp162-167, 2015
A novel requirement analysis approach for periodic control systems.
Zheng Wang, Geguang Pu, Jianwen Li, Yuxiang Chen, Yongxin Zhao, Mingsong Chen, Bin Gu, Mengfei Yang, Jifeng He.
Frontiers of Computer Science 7(2), pp214-235, 2013
On the Relationship between LTL Normal Forms and Büchi Automata.
Jianwen Li, Geguang Pu, Lijun Zhang, Zheng Wang, Jifeng He, Kim Guldstrand Larsen.
Theories of Programming and Formal Methods 2013, pp256-270, 2013
LTL Satisfiability Checking Revisited.
Jianwen Li, Lijun Zhang, Geguang Pu, Moshe Y. Vardi, Jifeng He.
TIME 2013, pp91-98, 2013
Bound-oriented parallel pruning approaches for efficient resource constrained scheduling of high-level synthesis.
Mingsong Chen, Lei Zhou, Geguang Pu, Jifeng He.
CODES+ISSS 2013, pp1-10, 2013
Branch-and-bound style resource constrained scheduling using efficient structure-aware pruning.
Mingsong Chen, Saijie Huang, Geguang Pu, Prabhat Mishra.
ISVLSI 2013, pp224-229, 2013
The stochastic semantics and verification for periodic control systems.
Mengfei Yang, Zheng Wang, Geguang Pu, Shengchao Qin, Bin Gu, Jifeng He.
SCIENCE CHINA Information Sciences 55(12), pp2675-2693, 2012
A Type System for SPARDL.
Zheng Wang, Jiangwen Li, Geugang Pu, Gu Bin
TASE 2012, pp 209-216, 2012
MDM: A Mode Diagram Modeling Framework.
Zheng Wang, G. Pu, Jianwen Li, Jifeng He, Shengchao Qin, Kim G. Larsen, Jan Madsen, Bin Gu.
FTSCS2012, pp135-149, 2012.
Xiao Yu, Shuai Sun, Geguang Pu, Siyuan Jiang, Zheng Wang.
A Parallel Approach to Concolic Testing with Low-cost Synchronization.
Electr. Notes Theor. Comput. Sci. 274: 83-96, 2011, Slides In 2009
A Unifying Approach to Validating Specification-Oriented XML Constraints.
Yongxin Zhao, Zheng Wang, Hao Xiao, Jing Ping, Geguang Pu, Jifeng He, Huibiao Zhu.
HASE 2011, pp33-40, 2011
An Event-B Interpretation for SPARDL Model
Jianwen Li, Zheng Wang, Yongxin Zhao, Geguang Pu, Yanxia Qi, Bin Gu:
HASE 2011, pp41-48, 2011
Linking denotational semantics with operational semantics for web services.
Huibiao Zhu, Jifeng He, Jing Li, Geguang Pu, Jonathan P. Bowen.
ISSE 6(4), pp 283-298, 2010
Web services choreography validation.
Zheng Wang, Lei Zhou, Yongxin Zhao, Jing Ping, Hao Xiao, Geguang Pu, Huibiao Zhu.
Service Oriented Computing and Applications 4(4), pp291-305, 2010
Model-Based Methods for Linking Web Service Choreography and Orchestration.
Jun Sun, Yang Liu, Jin Song Dong, Geguang Pu, Tian Huat Tan.
APSEC 2010, pp166-175, 2010
Automatically Testing Web Services Choreography with Assertions.
Lei Zhou, Jing Ping, Hao Xiao, Zheng Wang, Geguang Pu, Zuohua Ding.
ICFEM 2010, pp138-154, 2010
SPARDL: A Requirement Modeling Language for Periodic Control System.
Zheng Wang, Jianwen Li, Yongxin Zhao, Yanxia Qi, Geguang Pu, Jifeng He, Bin Gu.
ISoLA (1) 2010, pp594-608, 2010
Constraint Checking for XML-Based Language Specification by SAT Solver.
Hao Xiao, Zheng Wang, Geguang Pu, Bin Gu.
SSIRI (Companion) 2010, pp26-27, 2010
A Formal Model for Service Choreography with Exception Handling and Finalization.
Yongxin Zhao, Zheng Wang, Geguang Pu, Huibiao Zhu.
TASE 2010, pp15-24, 2010
Selected Papers Before 2010
Static Check of WS-CDL Documents.
Lei Zhou, Hanyi Zhang, Tao Wang, Chuchao Yang, Zheng Wang, Meng Sun, Geguang Pu.
SOSE 2008, pp142-147, 2009
A Bigraphical Model of WSBPEL.
Min Zhang, Ling Shi, Longfei Zhu, Yifei Wang, Libo Feng, Geguang Pu.
TASE 2008, pp117-120, 2008
Conformance Validation between Choreography and Orchestration.
Jing Li, Huibiao Zhu, Geguang Pu.
TASE 2007, pp473-482, 2008
Towards the Semantics and Verification of BPEL4WS.
Geguang Pu, Xiangpeng Zhao, Shuling Wang, Zongyan Qiu.
Electr. Notes Theor. Comput. Sci. 151(2), pp33-52, 2006
Theoretical Foundations of Scope-Based Compensable Flow Language for Web Service.
Geguang Pu, Huibiao Zhu, Zongyan Qiu, Shuling Wang, Xiangpeng Zhao, Jifeng He.
FMOODS 2006, pp251-266, 2006
A Formal Model forWeb Service Choreography Description Language (WS-CDL).
Hongli Yang, Xiangpeng Zhao, Zongyan Qiu, Geguang Pu, Shuling Wang.
ICWS 2006, pp893-894, 2006
Exploring optimal solution to hardware/software partitioning for synchronous model.
Jifeng He, Dang Van Hung, Geguang Pu, Zongyan Qiu, Wang Yi.
Formal Asp. Comput. 17(4), pp443-460, 2005
Semantics of BPEL4WS-Like Fault and Compensation Handling.
Zongyan Qiu, Shuling Wang, Geguang Pu, Xiangpeng Zhao.
FM 2005 ,pp350-365, 2005.
Building a web thesaurus from web link structure.
Zheng Chen, Shengping Liu, Liu Wenyin, Geguang Pu, Wei-Ying Ma.
SIGIR 2003, pp48-55, 2003