The goal of the Verifying Compiler Grand Challenge [7, 6] is to build a verifying compiler that “uses mathematical and logical reasoning to check the programs that it compiles”. This implies that “a program should be allowed to run only if it is both syntactically
and semantically correct”. To achieve this goal, the whole computing community have to deal with a wide range of issues, among which are...

Contents (11 pages)

1 Formal Software Engineering and the Grand Challenge
    1.1 The state of the art in software engineering
    1.2 The state of the art of formal methods
    1.3 Aims and Objective
2 Formal Modelling of Complex Systems
    2.1 Requirements modelling
    2.2 Design
3 Research Problems
4 Summary

As part of a history of the development of the computer industry from 1950 to 1970 focusing on the origins of t he "software crisis", I am currently trying to determine what people had in mind when they first began to talk about "software engineering". Although one writer has suggested that the term originated in 1965, it first came into common currency in 1967 when the Study Group on Computer Science of the NATO Science Committee called for an international conference on the subject. As Brian Randell and Peter Naur point out in the introduction to their edition of the proceedings, "The phrase 'software engineering' was deliberately chosen as being provocative, in implying the need for software manufacture to be [based] on the types of theoretical foundations and practical disciplines that are traditional in the established branchesof engineering."... (10 pages)