Tue 19 Jun 2018 16:50 - 16:55 at Columbus Ballroom B - Lightning Talks

Suppose I am despairing on a Coq proof goal about integers, but omega, lia, nia etc don’t work, and I don’t even know if my goal is true at all. Before continuing my proof, I’d like a quick diagnosis, by a bleeding edge tool, on whether the goal actually is true, but I don’t feel like installing any plugins or additional tools. In this talk, I will demo a quick way to achieve this: I will go to https://github.com/samuelgruetter/coq-smt-notations, copy-paste a few lines of Ltac and Coq notations right into my proof buffer (no need to compile anything or to reprocess anything in the IDE), and I get the negation of my goal printed in smtlib format. I don’t even need to install an SMT solver, but I can just copy-paste this into the online Z3 solver available at https://rise4fun.com/z3, and immediately get “unsat”, which means I should continue my proof, or a counterexample, which helps me figure out what’s wrong.

Tue 19 Jun

deepspec-2018-papers
16:10 - 17:35: DeepSpec 2018 - Lightning Talks at Columbus Ballroom B
deepspec-2018-papers16:10 - 16:15
Talk
deepspec-2018-papers16:15 - 16:20
Talk
deepspec-2018-papers16:20 - 16:25
Talk
Gordon StewartOhio University
deepspec-2018-papers16:25 - 16:30
Talk
deepspec-2018-papers16:30 - 16:35
Talk
deepspec-2018-papers16:35 - 16:40
Talk
deepspec-2018-papers16:40 - 16:45
Talk
Christine RizkallahUniversity of New South Wales
deepspec-2018-papers16:45 - 16:50
Talk
Joonwon ChoiMassachusetts Institute of Technology, USA
deepspec-2018-papers16:50 - 16:55
Talk
Sam GruetterMassachusetts Institute of Technology