Interesting. I had never heard of QK, and I'm slightly surprised about that.
people should no longer be surprised when a small-but-meaningful codebase is certified correct
For the size of codebase you're talking about, I'm not really that surprised. But I still think that formal methods don't scale to multicore RTOSs, which is the area I study (I'm a CS grad student).
people should no longer be surprised when a small-but-meaningful codebase is certified correct
For the size of codebase you're talking about, I'm not really that surprised. But I still think that formal methods don't scale to multicore RTOSs, which is the area I study (I'm a CS grad student).