The website [1] is worth reading too. I like the idea of an automated prover and an SMT solver running concurrently, one looking for a proof and the other for

The website [1] is worth reading too. I like the idea of an automated prover and an SMT solver running concurrently, one looking for a proof and the other for a counter example. [1] http://cosette.cs.washington.edu/ http://cosette.cs.washington.edu/