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


Datasheets.com Parts Search

185 million searchable parts
(please enter a part number or hit search to begin)
Like Us on Facebook
Special Video Section
5G LTE is on the way. These systems will require more ...
Protecting sensitive electronic circuitry from voltage ...
09:45
Watch as a web server authenticates or rejects a water ...
Protecting sensitive electronic circuitry from voltage ...
Watch as a web server authenticates or rejects a water ...
Protecting sensitive electronic circuitry from voltage ...
Power can be a gating factor in success or failure of ...
Get to market faster and connect your next product to the ...
00:44
See how microQSFP is setting a new standard for tomorrow’s ...
The LTC3649 step-down regulator combines key features of a ...
Once the base layer of a design has been taped out, making ...
In this short video we show an LED light demo to ...
The LTC2380-24 is a versatile 24-bit SAR ADC that combines ...
In this short video we show an LED light demo to ...
02:46
Wireless Power enables applications where it is difficult ...
07:41
LEDs are being used in current luxury model automotive ...
With design sizes expected to increase by 5X through 2020, ...
01:48
Linear Technology’s LT8330 and LT8331, two Low Quiescent ...
The quality and reliability of Mill-Max's two-piece ...