Formally verifying the correctness of an algorithm

Question

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?

Answer 1

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.

Answer 2

1. It's generally a lot easier to verify/prove correctness when no side effects are involved, but it's not an absolute requirement.
2. You might want to look at some of the documentation for a formal specification language like Z. A formal specification isn't a proof itself, but is often the basis for one.

Answer 3

Usually proofs of correctness are very specific to the algorithm at hand.

However, there are several well known tricks that are used and re-used again. For example, with recursive algorithms you can use loop invariants.

Another common trick is reducing the original problem to a problem for which your algorithm's proof of correctness is easier to show, then either generalizing the easier problem or showing that the easier problem can be translated to a solution to the original problem. Here is a description.

If you have a particular algorithm in mind, you may do better in asking how to construct a proof for that algorithm rather than a general answer.

Answer 4

Buy these books: http://www.amazon.com/Science-Programming-Monographs-Computer/dp/0387964800

The Gries book, Scientific Programming is great stuff. Patient, thorough, complete.

Answer 5

I think that verifying the correctness of an algorithm would be validating its conformance with a specification. There is a branch of theoretical Computer Science called Formal Methods which may be what you are looking for if you need to get as close to proof as you can. From wikipedia,

Formal Methods are a particular kind of mathematically-based techniques for the specification, development and verification of software and hardware systems

You will be able to find many learning resources and tools from the multitude of links on the linked Wikipedia page and from the Formal Methods wiki.

Answer 6

Logic in Computer Science, by Huth and Ryan, gives a reasonably readable overview of modern systems for verifying systems. Once upon a time people talked about proving programs correct - with programming languages which may or may not have side effects. The impression I get from this book and elsewhere is that real applications are different - for instance proving that a protocol is correct, or that a chip's floating point unit can divide correctly, or that a lock-free routine for manipulating linked lists is correct.

ACM Computing Surveys Vol 41 Issue 4 (October 2009) is a special issue on software verification. It looks like you can get to at least one of the papers without an ACM account by searching for "Formal Methods: Practice and Experience".

Answer 7

The tool Frama-C, for which Elazar suggests a demo video in the comments, gives you a specification language, ACSL, for writing function contracts and various analyzers for verifying that a C function satisfies its contract and safety properties such as the absence of run-time errors.

An extended tutorial, ACSL by example, shows examples of actual C algorithms being specified and verified, and separates the side-effect-free functions from the effectful ones (the side-effect-free ones are considered easier and come first in the tutorial). This document is also interesting in that it was not written by the designers of the tools it describe, so it gives a fresher and more didactic look at these techniques.

Answer 8

If you are familiar with LISP then you should definitely check out ACL2: http://www.cs.utexas.edu/~moore/acl2/acl2-doc.html

Answer 9

Dijkstra's Discipline of Programming and his EWDs lay the foundation for formal verification as a science in programming. A simpler work is Wirth's Systematic Programming, which begins with the simple approach to using verification. Wirth uses pre-ISO Pascal for the language; Dijkstra uses an Algol-68-like formalism called Guarded (GCL). Formal verification has matured since Dijkstra and Hoare, but these older texts may still be a good starting point.

Answer 10

PVS tool developed by Stanford guys is a specification and verification system. I worked on it and found it very useful for Theoram Proving.

Answer 11

WRT (1), you will probably have to create a model of the algorithm in a way that "captures" the side-effects of the algorithm in a program variable intended to model such state-based side-effects.