The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Steve,

 

I support Adam Chlipala’s statement that SMT might not be what you really want when working with Coq. Of cause the promise that it does things automatically is nice, but SMT is much less expressive than what Coq can handle in general. So you might spend a substantial amount of work formulating something such that you can automatically solve it with an SMT solver, which you can easily write down and solve automatically in Coq.

 

I would recommend to look at the Shorr Waite algorithm proofs in Dafny (SMT based proof language) and the same thing done in Coq. The things you have to write down to formulate this such that the SMT solver can solve it is really hard to understand, while the formulation of the proof goals in Coq is fairly straightforward. Also interesting is, that the Coq paper is 10 years older.

 

Another bad thing about SMT solvers is less abstraction. In Coq things can be abstracted a lot and proofs be done in small steps. SMT proof goals tend to be much less abstract and grow more with the complexity of your project. So it might be easy to start with SMT, but get increasingly unpleasant the further you go. Towards the end of a project, you might spend most of your time thinking about how you can reformulate your goal so that the SMT solver can solve it automatically – something which can be just time consuming and tedious trial and error. Coq work is much more pleasant ;-)

 

Best regards,

 

Michael

 

References:

Dafny: An Automatic Program Verifier for Functional Correctness K. Rustan M. Leino Microsoft Research

A case study of C source code verification: the Schorr-Waite algorithm. Thierry Hubert, Claude Marché

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of stvienna wiener
Sent: Friday, May 15, 2015 8:58 AM
To: coq-club AT inria.fr
Subject: [Coq-Club] Pointers regarding the state of the art of automation in Coq

 

Hi all,

 

Where can I start looking about the state of the art of automation in Coq? I have read that there is ongoing work on SMT/SAT integration, as well as automation support for resolution and rewriting proofs.

 

Are there any current papers I should look at?

 

By “Coq automation”, I mean automation regarding resolution, rewriting and SAT/SMT solver integration. I am less interested in the basic automation tools (auto, trivial or omega).

 

So far I have looked at the Coq workshop, ITP and the issues Journal of Automated reasoning for the last six years. I am aware that my question is rather broad and I still have some literature research to do. However, I would be glad if I get pointers into the right direction.

 

Best regards from Vienna,

Steve

 

PS: these are the papers I found so far:

 

[1] Armand, Michaël, et al. "A modular integration of SAT/SMT solvers to Coq through proof witnesses." Certified Programs and Proofs. Springer Berlin Heidelberg, 2011. 135-150.

 

[2] Blanqui, Frédéric, and Adam Koprowski. "CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates." Mathematical Structures in Computer Science 21.04 (2011): 827-859.

 

[3] Strub, Pierre-Yves. "Coq modulo theory." Computer Science Logic. Springer Berlin Heidelberg, 2010.

 

[4] Boldo, Sylvie, Jean-Christophe Filliâtre, and Guillaume Melquiond. "Combining Coq and Gappa for certifying floating-point programs." Intelligent Computer Mathematics. Springer Berlin Heidelberg, 2009. 59-74.

 

[5] Bezem, Marc, Dimitri Hendriks, and Hans De Nivelle. "Automated proof construction in type theory using resolution." Journal of Automated Reasoning 29.3 (2002): 253-275.