Formal Methods, Tools, Verification, Security

New Systems, New Tools, New Math, Richard Shoup, 2008 [slides-PDF]
Abstract: The appalling state of most software produced today is largely the result of the continual free lunch that has been provided by semiconductor technology (Moore's law) for nearly four decades. The current "parallelism panic" (the multicore revolution) can only worsen this situation. The advent of more parallel, highly complex, highly interconnected systems suggests that new and better tools are not only desirable but essential for dependable and secure computing in distributed, multicore, and reconfigurable systems.
    We argue that not only better tools, but new mathematical foundations are needed that permit grounded formal representations, unified and common to both hardware and software design, from the earliest specification of a computation through to implementation and later upgrades. The talk attempts to show 1) why the computing field is a mess today, 2) what it will require to take full advantage of reconfigurable and multicore hardware, and 3) how new deeper mathematical foundations can suggest ways of building formal hardware and software engineering tools that enable the production of verifiable, secure complex systems.