3 ms·
The term "formally verified" could be misleading. Some people assume it means "100% bug free". Whenever someone claims something is formlally verified one shoul
by vzaliva 6y ago
The term "formally verified" could be misleading. Some people assume it means "100% bug free". Whenever someone claims something is formlally verified one should ask what properties were verified exactly. In this work the approach they use (bounded model checking) could find some bugs on a subset of RISCV archictecure they formalized. I recommend looking at their slides for better understanding of the scope of the work: http://www.clifford.at/papers/2017/riscv-formal/slides.pdf http://www.clifford.at/papers/2017/riscv-formal/slides.pdf Nevertheless it is definetely a very impressive work and pracrically useful.
- mhh__ 6y agoThere are many (probably apocryphal) tales of "formally" verified systems being turned on then immediately crashing for this very reason
- capableweb 6y agoIn the end it's up to the reader to understand what it means. Many think "100% test coverage" is something you should strive towards as they think it means less bugs while in reality it just means that the test runner at one point or another accessed that line of code.