On Thu, Jul 31, 2008 at 02:52:11PM -0700, Andrew Lentvorski wrote: > The keyword for what you are talking about is called "formal > verification." It's not easy.
Sounds like an interesting and important field. I think that Djikstra (sic?) guy was a big fan of formally verifying all software IIRC. > Even verifying that something without state is correct is hard. Take, > for example, a 64bit x 64-bit multiplier. Simple energy considerations > automatically rule out combinatoric testing. Bummer. > I recommend the book "Algorithms and Data Structures in VLSI Design" by > Meinel and Theobald. It's focus is on how to use Binary Decision > Diagrams (BDD's) to do logic verification in the presence of the > combinatoric explosion presented by most VLSI systems. Use a little intelligence to avoid the entire search space. Now that would be a fun field to work in. Sounds very mathematical. > And, as an aside, just so you know, one of the few programming languages > to be formally verified is the Scheme48 system. One more reason to like Scheme. :) I don't know who likes Scheme more, mathematicians or programmers. Chris -- [email protected] http://www.kernel-panic.org/cgi-bin/mailman/listinfo/kplug-list
