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?

Fagot

I'm not sure what you mean about side effects. – Yolk

See this: en.wikipedia.org/wiki/Side_effect_%28computer_science%29 – Fagot

See https://mcmap.net/q/321533/-why-can-39-t-programs-be-proven which has some good answers. – Spiker

A very practical program which does verification (w/ other tools) is frama-c, watch the video demonstration screentoaster.com/watch/stUk9UQEZPTFxZSFtZWVNZ/frama_c_demo – Mommy

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.

Corrientes

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.

Nissa

And if you like Z, be confident that you will find tools to incorporate it in the process of writing a formally correct algorithm: bmethod.com/php/methode-b-en.php – Horsey

Answer 3

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.

Batho

Answer 4

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.

Yolk

Algorithm reduction (especially described as in the link you offer) is a theoretical tool to demonstrate that a problem is at least as hard as another. These proofs, often done in the Turing machine computation model, are hand-wavy affairs and nothing like formal (machine-checkable) proofs. They are often done for problems to hard to be useful in practice (the example in your link is for the Halting problem; showing a problem is NP-hard by reducing a known NP-hard problem to it is also popular). In short, I'm not sure problem reduction, as linked, has anything to do with formal correctness. – Horsey

Hmm maybe reduction is not the correct term I should be using here. When I say reduction I meant something along the lines of the following example. Suppose that you have an algorithm that computes the intersection of N rectangles, which you know is correct. Suppose you have another problem for which there exists a non-trivial translation of that problem to the problem of computing the intersection of N rectangles. Then you use the first algorithm to compute the solution to the latter problem. All that remains is showing that the translation is correct. – Yolk

But I can see that this is confusing, its a trick that relies on the fact that you make use of a well known algorithm that is known to be correct (in this case the one to compute the intersection of N rectangels.) I can see where the confusion comes as to whether this is a method of proving or providing a correct algorithm. – Yolk

Answer 5

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

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

Convalescent

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".

Kymry

"Formal methods" encompass all the objectives you cited. I'm in the sub-field of "proving programs correct" and I have to admit that until now the big industrial successes have come from the other sub-fields (just wait till next year!). A conference such as FMWEEK is somewhat puzzling because it gathers people with all these different approaches and objectives, but we do have a lot in common and a lot to exchange. – Horsey

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.

Horsey

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

Kenishakenison

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.

Pasco

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.

Hifi

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.

Lialiabilities