REGISTER | LOGIN
Breaking News
Comments
Newest First | Oldest First | Threaded View
<<   <   Page 3 / 3
pmetzger
User Rank
Author
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


Like Us on Facebook
EE Life
Frankenstein's Fix, Teardowns, Sideshows, Design Contests, Reader Content & More
Martin Rowe

Test Tool Finds Ethernet Wiring Errors
Martin Rowe
Post a comment
When my house was renovated several years ago, I had the electrician install network outlets in numerous places, then run the LAN cables to a wiring closet. But he didn't document the ends ...

Martin Rowe

Local Electronics Store Supplies Engineers and Hobbyists
Martin Rowe
5 comments
Rochester, N.Y. — Tucked away in this western New York city known for its optics is Goldcrest Electronics, a local store that's supplied businesses and individuals with electronic ...

Martin Rowe

How to Transform a Technology University (Book Review)
Martin Rowe
1 Comment
The Presiding Genius of the Place by Alison Chisolm. WPI, Worcester, Mass., 234 pp., 2016. Engineers love to discuss, and often criticize, engineering education. They often claim ...

Max Maxfield

Aloha from EEWeb
Max Maxfield
Post a comment
Just a few minutes ago as I pen these words, I posted this blog about this month's Cartoon Punchline Competition over on EEWeb.com.