Festschrift Symposium in Honor of He Jifeng
01-03 September 2013, Shanghai, China

Festschrift Symposium in Honor of He Jifeng

Invited Papers


Authors Paper Title
Jean-Raymond Abrial Set-theoretic Models of Computations
Bernhard K. Aichernig Model-Based Mutation Testing of Reactive Systems: from Semantics to Automated Test-Case Generation
Richard Banach Pliant Modalities in Hybrid Event-B
Jonathan P. Bowen A Relational Approach to an Algebraic Community: From Paul Erdos to He Jifeng
Michael Butler and Issam Maamria Practical Theory Extension in Event-B
Ana Cavalcanti, Alexandre Mota and Jim Woodcock Simulink Timed Models for Program Verification
Chao Chen, Huaikou Miao and Yihai Chen Concept analysis based approach to statistical web testing
Yifeng Chen Algebraic Program Semantics in Supercomputing
Hung Dang Van and Hoang Truong Modeling and Specification of Real-time Interfaces with UTP
Zhenhua Duan, Qian Ma, Cong Tian and Nan Zhang Some Fixed-Point Issues in PPTL
Yuxi Fu The Value-Passing Calculus
Martin Hilscher, Sven Linker and Ernst-Ruediger Olderog Proving Safety of Traffic Manoeuvres on Country Roads
Tony Hoare Generic Models of the Laws of Programming
Cliff Jones, Leo Freitas and Velykis Andrius Ours is to reason why
Line Juhl, Kim Guldstrand Larsen and Jean-Francois Raskin Optimal Bounds for Multiweighted and Parametrised Energy Games
Jianwen Li, Geguang Pu, Lijun Zhang, Zheng Wang, Jifeng He and Kim Larsen On the Relationship between LTL Normal Forms and Büchi Automata
Jian Lu, Yu Huang, Chang Xu and Xiaoxing Ma Managing Environment and Adaptation Risks for the Internetware Paradigm
Hanne Riis Nielson and Flemming Nielson Safety versus Security in the Quality Calculus
Shengchao Qin, Guanhua He, Wei-Ngan Chin and Hongli Yang Invariants Synthesis over a Combined Domain for Automated Program Verification
Bill Roscoe and Philippa Hopcroft Slow abstraction via priority
Jian Zhang Performance Estimation Using Symbolic Data
Hengjun Zhao, Naijun Zhan and Deepak Kapur Synthesizing Switching Controllers for Hybrid Systems by Generating Invariants
Liang Zhao, Shuling Wang and Zhiming Liu Graph-Based Object-Oriented Hoare Logic
Longfei Zhu, Yongxin Zhao, Huibiao Zhu and Qiwen Xu Towards a Modeling Language for Cyber-Physical Systems
     

Advanced Program for Festschrift Symposium in Honor of He Jifeng

Sep 01 - 03, 2013, Shanghai, China

(Download Program File: Word, PDF)



Symposium Venue:
Huashen Academic Exchange Center Hotel (Yi Fu Building, In the ECNU Campus)
East China Normal University, 3663 Zhongshan Road (North), Shanghai 200062, China

Note: The hotel address can be found here.

Day 1: 01 Sep 2013
8:45-9:30: Opening

9:30-10:30: UTP-1 (Chair: Cliff Jones)
A Relational Approach to an Algebraic Community: From Paul Erdos to He Jifeng
Jonathan P. Bowen

Set-theoretic Models of Computations
Jean-Raymond Abrial

10:30-11:00: Coffee Break

11:00-12:00: UTP-2 (Chair: Shengchao Qin)
Algebraic Program Semantics in Supercomputing
Yifeng Chen

Modeling and Specification of Real-time Interfaces with UTP
Hung Dang Van and Hoang Truong

12:00-14:00: Lunch Break

14:00-15:30: CPS (Chair: Richard Banach)
Optimal Bounds for Multiweighted and Parametrised Energy Games
Line Juhl, Kim Guldstrand Larsen and Jean-Francois Raskin

Towards a Modeling Language for Cyber-Physical Systems
Longfei Zhu, Yongxin Zhao, Huibiao Zhu and Qiwen Xu

Synthesizing Switching Controllers for Hybrid Systems by Generating Invariants
Hengjun Zhao, Naijun Zhan and Deepak Kapur

15:30-16:00: Coffee Break

16:00-17:00: Logics & Applications-1 (Chair: Jonathan Bowen)
Proving Safety of Traffic Manoeuvres on Country Roads
Martin Hilscher, Sven Linker and Ernst-Ruediger Olderog

On the Relationship between LTL Normal Forms and Büchi Automata
Jianwen Li, Geguang Pu, Lijun Zhang, Zheng Wang, Jifeng He and Kim Larsen


Day 2: 02 Sep 2013
9:00-10:30:Process Algebra (Chair: Hanne Riis Nielson)
Slow abstraction via priority
Bill Roscoe and Philippa Hopcroft

Simulink Timed Models for Program Verification
Ana Cavalcanti, Alexandre Mota and Jim Woodcock

The Value-Passing Calculus
Yuxi Fu

10:30-11:00: Coffee Break

11:00-12:00: Safety and Security (Chair: Kim Larsen)
Safety versus Security in the Quality Calculus
Hanne Riis Nielson and Flemming Nielson

Managing Environment and Adaptation Risks for the Internetware Paradigm
Jian Lü, Yu Huang, Chang Xu and Xiaoxing Ma

12:00-14:00: Lunch Break

14:00-15:30: Program Analysis and Verification (Chair: Yuxi Fu)
Invariants Synthesis over a Combined Domain for Automated Program Verification
Shengchao Qin, Guanhua He, Wei-Ngan Chin and Hongli Yang

Performance Estimation Using Symbolic Data
Jian Zhang

Ours is to reason why
Cliff Jones, Leo Freitas and Velykis Andrius

15:30-16:00: Coffee Break

16:00-17:00: Testing (Chair: Jian Zhang)
Model-Based Mutation Testing of Reactive Systems: from Semantics to Automated Test-Case Generation
Bernhard K. Aichernig

Concept analysis based approach to statistical web testing
Chao Chen, Huaikou Miao and Yihai Chen


Day 3: 03 Sep 2013
9:00-10:00: Event-B (Chair: Jean-Raymond Abrial )
Practical Theory Extension in Event-B
Michael Butler and Issam Maamria

Pliant Modalities in Hybrid Event-B
Richard Banach

10:00-10:30: Coffee Break

10:30-11:30: Logics & Applications-2 (Chair: Ernst-Ruediger Olderog)
Some Fixed-Point Issues in PPTL
Zhenhua Duan, Qian Ma, Cong Tian and Nan Zhang

Graph-Based Object-Oriented Hoare Logic
Liang Zhao, Shuling Wang and Zhiming Liu

11:30-12:00: Close

12:00-14:00: Lunch Break
  • Download Program File: (Word, PDF)