From Rewriting Logic, to Programming Language Semantics, to Program Verification

Grigore Rosu
Meseguer's Festschrift Springer, Volume 9200, pp 598-616, September 2015
PDF BIB Meseguer's Festschrift K

Abstract. Rewriting logic has proven to be an excellent formalism to define executable semantics of programming languages, concurrent or not, and then to derive formal analysis tools for the defined languages with very little effort, such as model checkers. In this paper we give an overview of recent results obtained in the context of the rewriting logic semantics framework K, such as complete semantics of large programming languages like C, Java, JavaScript, Python, and deductive program verification techniques that allow us to verify programs in these languages using a common verification infrastructure.