Search code examples
algorithmmathproofcorrectnessformal-verification

Formally verifying the correctness of an algorithm

First of all, is this only possible on algorithms which have no side effects?

Secondly, where could I learn about this process, any good books, articles, etc?

Solution

  • COQ is a proof assistant that produces correct ocaml output. It's pretty complicated though. I never got around to looking at it, but my coworker started and then stopped using it after two months. It was mostly because he wanted to get things done quicker, but if you need to verify an algorithm this might be a good idea.

    Here is a course that uses COQ and talks about proving algorithms.
    And here is a tutorial about writing academic papers in COQ.