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


EE Life
Frankenstein's Fix, Teardowns, Sideshows, Design Contests, Reader Content & More
Glen Chenier

Engineers Solve Analog/Digital Problem, Invent Creative Expletives
Glen Chenier
1 Comment
An analog engineer and a digital engineer join forces, use their respective skills, and pull a few bunnies out of a hat to troubleshoot a system with which they are completely unfamiliar. ...

Max Maxfield

What's the Best Traveling Toolkit?
Max Maxfield
13 comments
A few years ago at a family Christmas party, I won a pocket knife as part of a "Dirty Santa" game. This little scamp was a Buck 730 X-Tract. In addition to an incredibly strong and sharp ...

Rishabh N. Mahajani, High School Senior and Future Engineer

Future Engineers: Don’t 'Trip Up' on Your College Road Trip
Rishabh N. Mahajani, High School Senior and Future Engineer
10 comments
A future engineer shares his impressions of a recent tour of top schools and offers advice on making the most of the time-honored tradition of the college road trip.

Larry Desjardin

Engineers Should Study Finance: 5 Reasons Why
Larry Desjardin
41 comments
I'm a big proponent of engineers learning financial basics. Why? Because engineers are making decisions all the time, in multiple ways. Having a good financial understanding guides these ...

Top Comments of the Week
Flash Poll
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)