Proving a Computer Program's Correctness

Re:Proving a Computer Program's Correctness by jgrahamc on Friday October 02, 2009 @09:14AM (#856929)

Yes, this stuff is hard. My doctoral thesis was about using formal methods to prove that a system met a security policy. Specifically, I developed an algebra for reasoning about a system and creating its code directly from a specification.

If that sort of stuff excites you it's here: http://www.jgc.org/blog/jgc-thesis.pdf

[ Parent | on HN ]

Re:Proving a Computer Program's Correctness by billswift on Friday October 02, 2009 @09:48AM (#856996)

Actually, Edsger W Dijkstra advocated this stuff for many years. Almost all of his writings are collected on his home page at the University of Texas, http://www.cs.utexas.edu/users/EWD/ . There have been some advances since, but as the Schneier article shows, not much that is very useful yet.

[ Parent | on HN ]