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.