About
EducationWorkExperienceResumeOther AppointmentsResearch FieldsResearch 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:
Brief Bio: 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. Publications: 2015 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. 2014 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 2013 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 2012 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. 2011 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 2010 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 Enrollment and TrainingCourseScientific ResearchAcademic AchievementsPeking University‚ 2000.9-2005. 7‚ Ph. D Whuhan University‚ 1996.9-2000.7‚ BA Honor |