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
Engineer's Bookshelf
Caleb Kraft

The Martian: A Delightful Exploration of Math, Mars & Feces
Caleb Kraft
6 comments
To say that Andy Weir's The Martian is an exploration of math, Mars, and feces is a slight simplification. I doubt that the author would have any complaints, though.

The Engineering Life - Around the Web
Caleb Kraft

Surprise TOQ Teardown at EELive!
Caleb Kraft
Post a comment
This year, for EELive! I had a little surprise that I was quite eager to share. Qualcomm had given us a TOQ smart watch in order to award someone a prize. We were given complete freedom to ...

Design Contests & Competitions
Caleb Kraft

Join The Balancing Act With April's Caption Contest
Caleb Kraft
57 comments
Sometimes it can feel like you're really performing in the big tent when presenting your hardware. This month's caption contest exemplifies this wonderfully.

Engineering Investigations
Caleb Kraft

Frankenstein's Fix: The Winners Announced!
Caleb Kraft
8 comments
The Frankenstein's Fix contest for the Tektronix Scope has finally officially come to an end. We had an incredibly amusing live chat earlier today to announce the winners. However, we ...

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)