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

Book Review: Deadly Odds by Allen Wyler
Max Maxfield
10 comments
Generally speaking, when it comes to settling down with a good book, I tend to gravitate towards science fiction and science fantasy. Having said this, I do spend a lot of time reading ...

Martin Rowe

No 2014 Punkin Chunkin, What Will You Do?
Martin Rowe
Post a comment
American Thanksgiving is next week, and while some people watch (American) football all day, the real competition on TV has become Punkin Chunkin. But there will be no Punkin Chunkin on TV ...

Rich Quinnell

Making the Grade in Industrial Design
Rich Quinnell
13 comments
As every developer knows, there are the paper specifications for a product design, and then there are the real requirements. The paper specs are dry, bland, and rigidly numeric, making ...

Martin Rowe

Book Review: Controlling Radiated Emissions by Design
Martin Rowe
1 Comment
Controlling Radiated Emissions by Design, Third Edition, by Michel Mardiguian. Contributions by Donald L. Sweeney and Roger Swanberg. List price: $89.99 (e-book), $119 (hardcover).