Breaking News
Blog

How Can One Speed Up Validation?

NO RATINGS
View 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
Radio
LATEST ARCHIVED BROADCAST
EE Times editor Junko Yoshida grills two executives --Rick Walker, senior product marketing manager for IoT and home automation for CSR, and Jim Reich, CTO and co-founder at Palatehome.
Like Us on Facebook

Datasheets.com Parts Search

185 million searchable parts
(please enter a part number or hit search to begin)
EE Times on Twitter
EE Times Twitter Feed