Abstract
In previous lectures and seminars, we have explored the diversity of proofers, each with its own degree of automation, expressiveness and safety. In this talk, I will present various approaches to combining these tools in order to benefit from the advantages of each, paying particular attention to two families of provers:
- on the one hand, SMT provers, which are highly automated and general-purpose, but have lower expressiveness and safety ;
- on the other hand, proof assistants, highly expressive and secure tools for verifying complex properties, but with little automation.
I will discuss several recent implementations of these various approaches, ranging from the interaction between SMT and Coq provers thanks to Ergo, SMTCoq or Why3, toIsabelle's automatic sledgehammertactic, via the semi-automated program proof tool F*.
