Semantics-based program verifiers for all languages
OOPSLA, pp. 74-91, 2016.
We present a language-independent verification framework that can be instantiated with an operational semantics to automatically generate a program verifier. The framework treats both the operational semantics and the program correctness specifications as reachability rules between matching logic patterns, and uses the sound and relativel...More
PPT (Upload PPT)
Best Paper of OOPSLA, 2016