Home » forums » LtU Forum

The Halting Problem and Program Proving Algorithms

Is there any literature that investigates the abilities and limitations of Program Proving software in relationship to the halting problem? It seems like there is a relationship there that would warrant investigation, but I wasn't aware of where to find literature on the subject.

Thanks!

By johnnyb at 2010-06-27 03:36 | LtU Forum | previous forum topic | next forum topic | other blogs | 3966 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

What are you looking for?

Clearly automatic verification of full functional correctness for Turing-complete languages is undecidable, and you can show that with a standard reduction from the halting problem. At the same time, programs in Turing-complete languages that are annotated (by people) with clever loop invariants can often be checked quite effectively.

I'm not sure what more you're looking for. Even decidable verification problems are too expensive to solve in practice, more often than not. In practice, the key is either to find a really clever domain-specific abstraction or to get a human prover involved.

By Adam Chlipala at Mon, 2010-06-28 11:26 | login or register to post comments

I'm Looking for the Boundary

I'm looking for:

1) An introduction to writing such clever loop invariants
2) A look at how far that approach (and other approaches) can go, and what sorts of programs are the most problematic

Basically, I'm looking for the boundary. Obviously, the halting problem implies that there is a boundary, but I'm wondering who has done the research on where that boundary is - both in who has pushed it further out, and who has pushed it further in.

By johnnyb at Mon, 2010-06-28 15:45 | login or register to post comments

Your Guy

Then Adam, who wrote the reply you're replying to, is your guy. :-)

By Paul Snively at Mon, 2010-06-28 16:03 | login or register to post comments

Byron Cook's Work on Terminator

You will also find Byron Cook's work on Terminator educational.

C
By Charles Torre at Tue, 2010-06-29 23:30 | login or register to post comments