Before learning about Alloy*, you might want to learn about Alloy itself: <a href="http://alloy.lcs.mit.edu/alloy/index.html" rel="nofollow">http://alloy.lcs.mit.edu/alloy/index.html</a><p>Hillel Wayne has a great series of blog posts on using Alloy to solve software design problems: <a href="https://www.hillelwayne.com/tags/alloy/" rel="nofollow">https://www.hillelwayne.com/tags/alloy/</a>
Sometimes it would be great for such posts to somehow explain to the uninitiated why you want to be initiated.<p>"Relational Constraint Solver" sounds sort of interesting, but I haven't the faintest clue what I could use it for, and that's not that common for me.
I still find cbmc easier to find exhaustive counterexamples or test cases, because I can do it in straight C.<p>With ATS or spark/Ada I can also do the same, but much more. I can actually solve the problem, not only prove that it is solvable or incorrect.