Formal Systems Laboratory
© 2021. All rights reserved.
© 2021. All rights reserved.
Abstract. This invited paper describes an approach to language-independent deductive verification using the K semantics framework, in which an operational semantics of a language is defined and a program verifier together with other language tools are generated automatically, correct-by-construction.