Programming languages & software engineering
Building programming languages, tools, and software engineering techniques that make software more reliable, secure, and productive.
動画
Transition Invariants
Proof rules for the temporal verification of concurrent programs rely on auxiliary assertions. We propose a (sound and relatively complete) proof rule whose auxiliary assertions are transition invariants. A transition invariant of a program is…
