Breaking News
Comments
Newest First | Oldest First | Threaded View
<<   <   Page 3 / 3
pmetzger
User Rank
Rookie
Proving a program is error free
pmetzger   1/9/2014 7:15:07 PM
NO RATINGS
Our author asks: "but how can you actually prove that your design is error-free?"

The answer is it is difficult but possible. It requires the use of technologies people are generally not familiarized with, such as proof assistants -- prominent examples are Coq, Isabelle/HOL, and ACL2.

There exist, at this point, actual formally verified software artifacts of quite substantial complexity -- the seL4 microkernel, the CompCert C compiler, the Quark browser, and a number of others.

Sadly, very few people outside of academia are familiar with the existence of formal verification tools for software, and the documentation for such systems is (to say the least) non-transparent. The best tool at the moment, Coq, practically requires that its users learn quite a bit about Martin-Löf type theory in order to work effectively in it.

That said, such tools are clearly the way to deal with such things going forward.

<<   <   Page 3 / 3


Flash Poll
EE Life
Frankenstein's Fix, Teardowns, Sideshows, Design Contests, Reader Content & More
Max Maxfield

MSGEQ7-Based DIY Audio Spectrum Analyzer: Testing
Max Maxfield
13 comments
In my previous column on this topic, we discussed the step-by-step construction of the first pass at a MSGEQ7-based DIY audio spectrum analyzer for use in my BADASS Display project. Of ...

Karen Field

June 2014 Cartoon Caption Winner
Karen Field
13 comments
Congratulations to "Wnderer" for submitting the winning caption for our June cartoon, after much heated conversation by our judges, given the plethora of great entries.

Jeremy Cook

Inspection Rejection: Why More Is Less in a Vision System
Jeremy Cook
3 comments
Albert Einstein has been quoted as saying, "Everything should be as simple as possible, but not simpler." I would never claim to have his level of insight -- or such an awesome head of ...

Jeremy Cook

Machine Fixes That Made Me Go 'DUH!'
Jeremy Cook
21 comments
As you can see in my bio at the end of this article, I work as a manufacturing engineer. One of my favorite things that happens on a Friday late in the afternoon is to hear my phone ring ...

Top Comments of the Week
Like Us on Facebook
EE Times on Twitter
EE Times Twitter Feed

Datasheets.com Parts Search

185 million searchable parts
(please enter a part number or hit search to begin)