wiki_page.2006-04-02.4483798772
last edited 3 years ago by rjoshi
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
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?)