Grand Challenges for `Formal Methods'

Dines Bjørner
CSE: Computer Science and Engineering
IMM: Informatics and Mathematical Modelling
Building 322, Richard Petersens Plads
DTU: Technical University of Denmark
DK-2800 Kgs.Lyngby, Denmark
E-Mail: db@imm.dtu.dk, URL: www.imm.dtu.dk/~db

June 19, 2003

THIS PAGE IS PRESENTLY UNDER CONSTRUCTION

Purpose of this Web Page
On the Nature of Grand Challenges
Topics for Discussion
Modalities of Monitoring Submissions and E-Mail Discussion
Plans for a Mid-year 2004 European Workshop on ``Grand Challenges''
About this document ...

Abstract
- This is a document in The CSE/IMM/DTU series of CoLogNET Web Documents
- It is directly related to item [6.] A ``Grand Challenges'' Task Force on the just referenced web page.
- It also extends On a ``Grand Challenges'' Task Force
- In the present document we shall build up, over time, a list of `Grand Challenges' for the development of software,
  notably such using formal techniques.

Purpose of this Web Page

The purpose of this web site and those of its predecessor and successors:

is to entice (solicited) readers to rebut, to come with counter- or to additional grand challenges, or the help sharpen and rephrase previously expressed and here referenced grand challenges.

On the Nature of Grand Challenges

This section is an edited quote of 17 grand challenge criteria reported by Tony Hoare:

The Verifying Compiler: A Grand Challenge for Computing Research.
Journal of the ACM, Vol.50, No.1, January 2003, pp 63-69.

We edit, while in the process of seeking formal permission, our quote - where `it' normally refers to any proposed grand challenge -- into:

Fundamental: It relates strongly to foundations, and the nature and limits of a discipline.

Astonishing: It implies constructing something ambitious, heretofore not imagined.

Testable: It must be objectively decidable whether a grand challenge project endeavour is succeeding or failing.

Revolutionary: It must impy radical paradigm shifts.

Research-oriented: It can be achieved by methods of academic research -- and is not likely to be met sôlely by commercial interests.

Inspiring: Almost the entire research community must support it, enthusiastically -- even while not all may be engaged in the endeavour.

Understandable: Comprehensible by and captures the imagination of the general public.

Challenging: Goes beyond what is initially possible and requires insight, techniques and tools not available at the start of the project.

Useful: Results in scientific or other rewards - even if the project as a whole may fail.

International: It has international scope: Participation would increase the research profile of a nation.

Historical: It will eventually be said: It was formulated years ago, and will stand for yers to come.

Feasible: Reasons for previous failures are now understood and can noe be overcome.

Incremental: Decomposes into identified individual research goals.

Co-operative: Calls for loosely planned co-operation between research teams.

Competitive: Encourages and benefits from competition among individuals and teams - with clear criteria on who is winning, or who has won.

Effective: General awareness and spread of results changes attitudes and activities of scientists and engineers.

Risk-managed: Risks of failure are identified and means to meet will be applied.

Topics for Discussion

I venture to suggest the two ``challenges'' listed 1.-2. below. The second one really is'nt formulated as I would prefer it. So I am in the process of asking an English colleague of us to write ``his'' (I am sure, better) version.