Current Status: Trying to learn a new thing.
I think they called it Coq because it's hard.. (Sorry 
)pic.twitter.com/3WQHw8ytIX
-
what kind of "property" coq will be able to prove on a digital hardware that a SMT solver like Z3 can't ?
Well, coq can't prove anything. It can just check if the proofs you give it are correct. :) There is a lot of stuff involving algebra that humans can solve pretty easily and bit-vector SMT solvers can't. For example, try this with N, M > 16: http://svn.clifford.at/handicraft/2017/vlcoqex/mulequiv.sv …pic.twitter.com/k9BKsKCikV
-
-
Also, QF SMT solvers by themselves don't know anything about complete proves of temporal properties. You can use techniques like k-induction with SMT solvers, but they are very limited. Stuff like IC3 is better but also has massive limitations.
-
With an SMT solver that excepts quantified SMT formulas you can express most temporal properties easily, but except for the most trivial problems the SMT solver will either not finish before the heat death of the universe, or it will return UNKNOWN.
- Show replies
New conversation -
-
-
I tried it by hand here: https://rise4fun.com/Z3/jlsl (I'm learning SMT so it is a great exercise). And yes it times out !
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.