title: Can Coq be used (easily) as a model checker?
body: <p>As the title says, can Coq be used as a model checker? Can I mix model checking with Coq proving? Is this usual? Google talks about a "µ-calculus", does anyone have experience with this or something similar? Is it advised to use Coq in this way, or should I look for another tool?</p>