3 ms·
I've been writing a simple verifier for C over the last few months and one of the Yak Shaving libraries I needed to write was a proper range handling library.
by junon 5y ago
I've been writing a simple verifier for C over the last few months and one of the Yak Shaving libraries I needed to write was a proper range handling library.
Since the C programs I'm writing won't be using floating point types, I got lucky - because they are an absolute pain to deal with with any degree of certainty.
- siraben 5y agoIs there a public link for your verifier? What style of semantics are you using for it and what sort of programs and features can you reason about?
- junon 5y agoIt's not yet published unfortunately, I'll probably post it here once it's closer to completion. It's being written for a new OS kernel.