Embedded Systems Conference
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


Radio
LATEST ARCHIVED BROADCAST
As data rates begin to move beyond 25 Gbps channels, new problems arise. Getting to 50 Gbps channels might not be possible with the traditional NRZ (2-level) signaling. PAM4 lets data rates double with only a small increase in channel bandwidth by sending two bits per symbol. But, it brings new measurement and analysis problems. Signal integrity sage Ransom Stephens will explain how PAM4 differs from NRZ and what to expect in design, measurement, and signal analysis.

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
The LTC®6363 is a low power, low noise, fully differential ...
Vincent Ching, applications engineer at Avago Technologies, ...
The LT®6375 is a unity-gain difference amplifier which ...
The LTC®4015 is a complete synchronous buck controller/ ...
10:35
The LTC®2983 measures a wide variety of temperature sensors ...
The LTC®3886 is a dual PolyPhase DC/DC synchronous ...
The LTC®2348-18 is an 18-bit, low noise 8-channel ...
The LT®3042 is a high performance low dropout linear ...
Chwan-Jye Foo (C.J Foo), product marketing manager for ...
The LT®3752/LT3752-1 are current mode PWM controllers ...
LED lighting is an important feature in today’s and future ...
Active balancing of series connected battery stacks exists ...
After a four-year absence, Infineon returns to Mobile World ...
A laptop’s 65-watt adapter can be made 6 times smaller and ...
An industry network should have device and data security at ...
The LTC2975 is a four-channel PMBus Power System Manager ...
In this video, a new high speed CMOS output comparator ...
The LT8640 is a 42V, 5A synchronous step-down regulator ...
The LTC2000 high-speed DAC has low noise and excellent ...
How do you protect the load and ensure output continues to ...