Design Con 2015
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
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)
EE Life
Frankenstein's Fix, Teardowns, Sideshows, Design Contests, Reader Content & More
Max Maxfield

DIY Practical Joke Project Idea
Max Maxfield
12 comments
I just received a rather interesting email from a member of the EETimes community who prefers to remain anonymous. This message was as follows:

Jolt Judges and Andrew Binstock

Jolt Awards: The Best Books
Jolt Judges and Andrew Binstock
1 Comment
As we do every year, Dr. Dobb's recognizes the best books of the last 12 months via the Jolt Awards -- our cycle of product awards given out every two months in each of six categories. No ...

Engineering Investigations

Air Conditioner Falls From Window, Still Works
Engineering Investigations
2 comments
It's autumn in New England. The leaves are turning to red, orange, and gold, my roses are in their second bloom, and it's time to remove the air conditioner from the window. On September ...

David Blaza

The Other Tesla
David Blaza
5 comments
I find myself going to Kickstarter and Indiegogo on a regular basis these days because they have become real innovation marketplaces. As far as I'm concerned, this is where a lot of cool ...