How would you use Hoare logic to verify an API migration did not introduce new behaviors? If the API spec allows multiple implementation choices, you need to reason about relational liveness over nondeterministic executions, but relational Hoare logics don't support this kind of reasoning... until now!
Check out my APLAS talk "RHLE: Modular Deductive Verification of Relational ∀∃ Properties" Monday at 1:30p.
📄 Preprint: https://arxiv.org/pdf/2002.02904.pdf
I have lived seeing my work appear "years after the shine has dulled," and I can say it is without question a more discouraging experience than the rejections themselves.
Update: I have typed the hole.
Having a real hard time reheating food in this microwaved-sized void for some reason.
Also some of the attempts to match books from the import are pretty amazing. I'm sure these two books are basically the same thing.
PhD Student at Purdue advised by Ben Delaware. PL, formal methods, verification and synthesis.
A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.