History for wiki_page.2006-04-02.4483798772

changed:
-
Key characteristics for a pilot project

 * Complex enough e.g. multi-threaded, fault-tolerant, secure

 * Simple enough -- should take no more than 1-2 years

 * Verification should have an impact <br>
   esp. outside the formal methods community

 * Should be well-defined and the specification should be accessible

   * in the sense that code and models should be openly available

 * Should be amenable to different approaches

   * both a posteriori and a priori approaches

High-impact possibilities

 * Safety- and mission-critical systems

 * Financial systems?

 * Electronic Voting

  A serious problem with all of these is *accessibility*, since specifications for such applications are hard to come by (information is often classified or restricted e.g., ITAR)

Better possibilities

 * A verifying compiler

   * what to target? will this have an impact?

 * Small operating system (real-time?)

   * e.g., for embedded devices

 * Key component of an operating system

   * such as a filesystem or resource management (CPU? memory?)