头像

Pugeguang

      

About

  • Department:
  • Graduate School:
  • Degree:
  • Academic Credentials:
  • PostCode:
  • Tel: 021 62235710
  • Fax: 86 21 62235255
  • Email: ggpu@sei.ecnu.edu.cn
  • Office: Math Building 212
  • Address: Zhongshan Road 3663

Education

WorkExperience

Resume

Other Appointments

Research Fields

Research

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 LiJifeng HeShengchao QinKim G. LarsenJan MadsenBin 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 Training

Course

Scientific Research

Academic Achievements

Peking University‚ 2000.9-2005. 7‚  Ph. D

Whuhan University‚ 1996.9-2000.7‚ BA 

Honor

10 Visits

Related to the teacher