SMTCoq: the power of SMT solving in Coq

Chantal Keller
Follow

Abstract

SMTCoq is a tool to make the Coq proof assistant and SMT solvers cooperate, with the same degree of confidence as Coq. In this talk, I will give an overview of its potential:

  • checking SMT answers, both in Coq and externally using the Coq extraction mechanism
  • importing SMT problems as Coq theorems
  • calling SMT solvers to ease Coq proof building, in a ongoing project called Sniper.

An API to build first-order SMTCoq terms and formulas is also under progress, in order to have an easy access to SMTCoq internal functionalities.

Date
Friday, November 12, 2021 10:00 Europe/Paris
Event
GReTA-ExACT working group
Zoom registration: click here! Please consider joining the meeting already within the 15min prior to the start of the seminar to ensure your setup is functioning properly. You may connect with either the Zoom web or Zoom desktop clients.

Please note that the meeting will be recorded and live-streamed to YouTube:

.GReTA-ExACT
Chantal Keller
Chantal Keller
Maître de Conférences

I am a member of the Laboratory of Formal Methods, teaching at the Computer Science Department at IUT d’Orsay. I am interested in programming languages and formal methods, notably through Type Theory, the combination of automated and interactive provers, and proof and test of programs. I apply these methods to many domains from programming languages themselves to security.