He Jifeng, computer software expert£¬was born in Shanghai in August, 1943, and graduated from the math department of Fudan University in the year 1965. He is the president of Hangzhou International Outsourcing College. Since 1965, he has been working in Huadong Normal University (HDNU) as a teacher, and then a professor since the year 1986. During 1980-1982, He studied in Stanford University and University of San Francisco as a visiting scholar, and then as a visiting professor and senior researcher in Oxford University during 1984-1998. He has been a tutor of Ph.D. students in HDNU since 1995, and a part-time professor and tutor of Ph.D. students of Shanghai Jiaotong University since 1996. Since 1998, he has been a senior researcher of United Nations University International Institute for International Software Technology (UNU-IIST). He is also a part-time professor and tutor of Ph.D. students of Nanjing University. In the year 2001, he became the president of Software School of Huadong Normal University. In the year 2002, he was selected as a professor for life in Huadong Normal University. Since 2003, he has become a part-time professor and tutor of Ph.D. students of Zhejiang University. At present, he is the president of Software School of Huadong Normal University and director of Shanghai Institute of imbedded Systems. In December, 2005, he was elected as an academician of Chinese Academy of Sciences.

He has started to engage in the research of programming theory and application since 1980. And in 1986, he and C.A.R.Hoare co-proposed ¡°the program decomposition operator ", and regarded the standard language and the program language as the identical kind of mathematical object. Then he proposed to take ¡°the relational algebra" as the unified mathematical model to standardize the procedure and software so as to ensure the use relational algebra to describe the process of program decomposition and combination, which enables to support the development of software directly. In the data refinement aspect, he has worked out the complete method to process the indefinite program language data refinement.

In 1995, upon summering a series of program language semantic theories and methods, he and C.A.R. Hoare co-proposed the programming unification theory and a mathematic principle in connecting each kind of programming theory. He also proposed to communicate several program languages with the formalized surface theory, as well as the mathematical model and algebra law for indefinite data flow. In recent years, his research on co-design system of the software and hardware provides a beneficial way to reduce time and cost in the systematic chip design.

In 1985, he won the First Prize for software design awarded by the Ministry of Electronics Industry; in 1986, the First Prize for advancement of science and technology in Shanghai; in 1988, selected as Outstanding Middle-aged Expert with Prominent Contribution to the country; Queen¡¯s Award for Advanced Technology in 1989 and 1993 respectively; in 2000, the First Prize for advancement of science and technology in Shanghai; in 2002, the Second Prize for National Natural Science

Experiences

May, 1960 ~ Feb., 1965 Study in math department of Fudan University

July, 1980 ~ July, 1981 visiting scholar in Stanford University and University of San Francisco

Mar., 1965 ~ July, 1985 teacher in Huadong Normal University

Dec., 1984 ~ July, 1998 visiting professor and senior researcher in Oxford University

Aug., 1986 up to present working as a professor in Huadong Normal University

1988 up to present State Outstanding Expert

Aug., 1995 up to present tutor of Ph.D. students in Huadong Normal University

July, 1998 up to present senior researcher of United Nations University International Institute for International Software Technology (UNU-IIST)

Aug., 1996 up to present part-time professor and tutor of Ph.D. students of Shanghai Jiaotong University

Aug., 1998 up to present part-time professor and tutor of Ph.D. students of Nanjing University

Nov., 2001 up to present president of Software School of Huadong Normal University

Dec., 2002 up to present professor for life in Huadong Normal University

May, 2003 up to present part-time professor and tutor of Ph.D. students of Zhejiang University

Since December, 2005, academician of Chinese Academy of Sciences

Awards

First Prize for software design awarded by the Ministry of Electronics Industry in 1985

First Prize for advancement of science and technology in Shanghai in 1986

Queen¡¯s Award for Advanced Technology in 1989

Queen¡¯s Award for Advanced Technology in 1993

First Prize for advancement of science and technology in Shanghai in 2000

Second Prize for National Natural Science in 2002

Major Academic Research Papers and Achievements

Since 1985, his academic research achievement in the ¡°Design of Strict Security Software Complete Mathematic Calculation System¡± has mainly provided two sorts of technology, inclusive of (1) establishing standardized programming and software calculation system, which is able to use mathematic calculation to support the set-up of technical files and verification task related to software design in each important stage in the process of software development, and (2) design of complete calculation principles to guide the development tasks including the standardized description of all software system parts educed based on the users¡¯ requirement, and the function description of the low layer software module process calculated from the standardized description of all parts. His related academic research papers were respectively published in the well-known international journals like ¡°Comm of the ACM¡±¡¢¡°Formal Aspect of Computing¡±¡¢¡°Science of Computer Programming¡±¡¢¡°Acta Information¡± or read in some important academic meetings. By the year 2002, his academic viewpoints have been cited by SCI index for 169 times.

1. J. He, J. He, C.A.R. Hoare, J.W. Sanders£¬Data Refinement Refined - Resume£¬Lecture Notes in Computer Science£¬1986£¬213: 187-196

2. C.A.R. Hoare, He Jifeng, J.W. Sanders£¬Prespecification in Data Refinement£¬Information processing Letters£¬1987£¬25: 71-76

3. He Jifeng£¬Process Simulation and Refinement£¬Formal Aspects of Computing£¬1989£¬1: 229-241

4. He Jifeng, C.A.R. Hoare£¬From Algebra to Operational Semantics£¬Information processing letters£¬1993£¬45: 75-80

5. He Jifeng£¬From CSP to Hybrid Systems£¬A Classical Mind£¬1994£¬171-191

6. He Jifeng, C.A.R. Hoare£¬Provably Correct Systems£¬Lecture Notes of Computer Science£¬1994£¬863: 288-335

7. He Jifeng£¬Provably Correct Systems: Modelling of Communication Languages and Design of Optimized Compilers£¬McGraw-Hill Publisher£¬1994.

8. He Jifeng, K. Seidel, A. McIver£¬Probabilistic Models for The Guarded Command Language£¬Science of Computer Programming£¬1997£¬28: 171-192

9. C.A.R. Hoare, He Jifeng£¬Unifying Theories of Programming£¬Prentice Hall International£¬1998.

10. He Jifeng£¬A Common Framework for Mixed Hardware/Software Systems£¬Proceedings of IFM'99£¬1999£¬1-24.

Major achievements

1. In allusion to the imperfection of data refinement method and its limitations on process of only definite programming language, He Jifeng and his collaborator co-proposed a complete data refinement theory and put forward a data refinement method for processing the indefinite program language in their research papers ¡°Data Refinement Refined¡± and ¡°Prespecification in Data Refinement¡±, by using ¡°up-down simulation image set¡± to obtain function declaration of each process from every programming module for a mature calculation principle. In the year 1986, He and his collaborator co-proposed the direct connection between data refinement theory and algebraic programming law, so that the corresponding data refinement methods can be chosen according to different languages. The well-known European specification B language has adopted such method (see ¡°The B Book¡± written by J-R Abrial, page 501 and 550, Cambridge University Press). Theoretical Computer Science Series published by Cambridge University Press once pointed out that this data refinement theory is a milestone of model-oriented software development.

2. In 1986, he and his collaborator co-proposed process dissociation operator, and took specification language and programming language together as the same mathematical object. One year later, in 1987, he proposed in his academic research paper ¡°The Weakest Prespecification¡± the idea of using relational algebra as the unified mathematical model of programming and software specification, and discovering that the algorithm analysis equations (X£»Q£¾S and P£»X£¾S) in the mathematical frame can finally be solved. In this case, relational algebra can be used to describe courses of the decomposition and composition of the process. Therefore, mathematical methods can be taken directly to develop software. Based on the above work, he proposed the theory of algebra law in programming, and a set of algebra laws were then concluded regarding programming language so that program transformation can be accomplished directly by the application of basic laws.

3. In 1998, he and C.A.R.Hoare, in their monograph ¡°Unifying Theories of Programming¡±, co-proposed a unifying mathematic model which is able to describe Serial Language, Parallel language, Communication Language, Logic language, Functional programming language and proved the Consistency of three Semantics, i.e. Denotation semantics, algebraic semantics and operational semantics, and also brings in the model of The probability programming language by using "linking theory".

4. He used formalized interface theory to communicate in several programming languages, and proposed the mathematical models and the algebra law of indefinite data flow. In 1989, in the European research program Eureka PROCOS, whose major task is to take the formalized interface theory to communicate in several programming languages and design a provable compiler and programming transformation system. He Jifeng, in this program, did an important contribution. He has summarized the related work in his monograph "Provable Correct Systems: Modelling of Communication Languages and Design of Optimized Compilers". In 1990, he raised a mathematical model of indefinite data flow and algebra law in his academic research paper "A theory of Synchrony and Asynchrony", which was used to support Jackson development methods and the design of asynchronous communication process.

5. Since 1992, he has gone in for software-hardware coordinated design frame of the industry-based programming language VERILOG to discuss the consistency of language simulator semantics and synthetic semantics, and designed the mathematical model for an optimized software-hardware decomposer and synthesizer. So far, the development of software-hardware co-design platform named Poseidon has been completed and put into use.

Projects/programs completed in recent years

2001 - 2003, VERILOG simulator and synthesizer design, sponsored by Shanghai Information Commission (CX20010005)

2002 - 2004, formalized theory of UML software development process, key project sponsored by the Ministry of Education (02104)

2003 - 2005, theory of software security and hardware and software co-design, "211" project

2002 - 2007, formalized theory and method of study of software network configuration, ¡°973¡± project (study of intermediate software theory and method which is based on Internet environment, project code: 2002CB31200001)