=========================================================================


TITLE
-----

Does Formal Methods need a relaunch?



POSITION STATEMENT
------------------

Many consider formal methods to be boring, hard to understand and of
dubious value (or even a waste of time).

Do we need to "relaunch" formal methods to show that it is a crucial
scientific foundation for "computational thinking" and may be the
basis for future breakthroughs?

Here are some thoughts on how a relaunch might proceed.

 1. Promulgate the concept of "Formal Thinking" as a special case of
    Wing's influential manifesto for Computational Thinking
    [http://www.cs.cmu.edu/afs/cs/usr/wing/www/publications/Wing06.pdf].

    Material for this is in Wing's paper "Weaving Formal Methods into
    the Undergraduate Computer Science Curriculum" (2000)
    [http://www.springerlink.com/content/1taf7cbm5qxb4vn3/fulltext.pdf].
    The goal would be to go beyond reforming undergraduate teaching
    and to make the case that formal thinking is a crucial scientific
    foundation for all computational thinking.

 2. Create a Web 2.0 style buzz around formal methods. Here are some
    suggestions.

     - Run a competition like the one the Computer Lab and Google have
       just launched [http://www.2minutechallenge.org/site/].  A
       formal methods competition could aim to generate a repository
       of accessible material to:

         * explain what formal methods are;
         * show where they can be applied;
         * exhibit unusual and "cool" applications.

       Prizes could consist of the winning video(s) being shown at a
       prestige conference, to which the winner(s) gets expenses paid.
       Competitions do seem to work in creating excitement (the CADE
       theorem proving competitions and the CAV SAT and SMT
       competitions certainly generate a buzz). Our competition would
       be oriented to explaining and publicising formal methods,
       rather than comparing competing tools.

     - Create a web page of masters level projects to help steer
       start-of-career people into formal methods and then provide
       them with credentials and motivation to proceed to industry or
       a PhD.  For example, here are some projects from a list I
       maintain for our final year undergraduate students:

         http://research.microsoft.com/~bycook/suggestions.htm
         http://research.microsoft.com/~jfisher/projects.html
         http://www.cl.cam.ac.uk/~jem74/project_suggestions_2007-2008.html
         http://www.cl.cam.ac.uk/~pes20/projects-f.html

        I'm not suggesting these for the list, but perhaps they give
        an idea of the sort of thing one could have.

     - Create a web page listing challenge projects for research:
       these would be PhD sized and thought provoking.  The projects
       could be contributed by academics and industry.

         * A non-traditional formal methods PhD area might be the
           synthesis and/or verification of financial tools
           (http://www.scicomp.com/derivativesmodeling/compilers).

         * Biology is an emerging area for formal methods applications
           as shown by the workshop "Formal Methods in Systems
           Biology" (http://research.microsoft.com/ero/FMSB/).

         * There are, of course, very challenging verification
           problems in the systems programming area.  I've had
           discussions with members of the Xen hypervisor group at
           Cambridge: low level hypervisor code might be an area ripe
           for mining for PhD projects.


Mike Gordon
01 June 2008

=========================================================================