Formal Methods, Tools, Verification, Security

Highly-Parallel Systems, New Math, and New Tools, Richard Shoup, 2011 [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 over four decades. The current "parallelism panic" (aka the multicore revolution) is sure to 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.     This talk attempts to show 1) how the computing field is getting in trouble by building increasingly complex systems that no one understands, 2) what it will require to take full advantage of reconfigurable and multicore highly-parallel hardware, and 3) some new and deeper mathematical formalisms for building formal hardware and software engineering tools to enable the production of verifiable, secure complex systems.

Kids running down a hill, out of control.