4 ms·
A driver is a pretty small program, and as you say, the "verifier" ("checker" would have been a better term) doesn't even try to verify that the driver will run
by ScottBurson 10y ago
A driver is a pretty small program, and as you say, the "verifier" ("checker" would have been a better term) doesn't even try to verify that the driver will run the device correctly.
Actually proving correctness of large programs like compilers and operating systems is not considered an easy problem. You surely know that; I don't know what you're thinking when you dismiss the problem.
What proof-of-correctness systems have you worked on?
- Retric 10y agoProof-of-correctness is an irrelevent concept. You can't specify the correct solutions to all edge cases for non trivial problems. You can however add constraints and test for those especially when you are willing to deal with a bunch of edge cases manually. First time I did static analysis I knew there was a lot of edge cases I could detect, but not deal with. But, in practice my code dealt with 99.97% percent of cases which was easily enough be be extremely useful.