What is the future of Theorem Proving?

Organizer: Sandip Ray
Moderator: Panagiotis Manolios

Panelists: Arvind
           Matthias Felleisen
           David Hardin
           Wilfred Legato
           Paul Miner
           J Moore 

Theorem proving has a long and rich history of several decades, with
many successes in the formal verification of critical computing
systems.  Nevertheless, theorem proving has always been perceived of
as an extremely expensive and difficult technology and that perception
has not changed significantly over the decades.  Is theorem proving
really inherently complex?  Will it only be applicable in certain
critical areas of formal verification, requiring individual
super-human efforts? How can we make the use of theorem proving more
main-stream?  Is it a question of improving the technology itself, or
should more emphasis be given on training the work-force and
presenting the technology in more accessible terms to the outside
world?

The panelists will discuss the top challenges and opportunities they
see for pervasive use of theorem proving, both from academic and
industrial perspectives.  Audience members will respond with open
microphone, challenging or supporting the panelists and giving their
own views on the matter.