Stephen Siegel

Assuming undefined functions return a nondeterministic value of the right type and don't modify anything is one reasonable interpretation, but not the only one and not my preferred solution. In...

I don't see how it "closes the door" to ask a real-world developer to write a simple 1-line stub of a function. It's not that hard. But whatever ---- there...

In a real world use case, the person who wrote the stub would be the same person who is running the verification tool. They don't need to be told that...

I read above that there are "thousands of such functions". Wow --- that is fascinating. Where do these functions come from? Has someone actually gone through all of them and...

As for the calls through unknown function pointers... Is it correct that the only way such a function pointer could exist is because it was returned by __VERIFIER_nondet_something()? The only...