Counterexamples for Coq Conjectures
The goals of this presentation are to motivate the need for automatic counterexample search in Coq, to evaluate existing tools which are currently available for Coq users, but also tools from other ecosystems performing better than those available for Coq, to conclude that the current state of the art for counterexample search in Coq is unsatisfactory and should be improved, hopefully initiating a discussion in the Coq community on how this problem should be tackled.
Sat 19 Jan
|09:00 - 09:05|
|09:05 - 10:05|
|10:05 - 10:30|
Sam GruetterMassachusetts Institute of TechnologyFile Attached