Review on Imandra by Aaron Carney

The ease with which we can manage our own model in order to prove properties, or disprove them as well! It's fast and easy too boot. We have used it mainly for proving/disproving loop invariants (LIs). There are no other tools that I know about like this one; so far its pretty much what you need if you're looking at implementing LISP into your code base. Nothing specific comes up when using this tool but maybe some familiarity will help? Do not make assumptions regarding how familiar others would be with their use. Try before buying - there really isn't any way around that unless they offer free trial periods. Proving Loop Invariant was an important part of my graduate work.