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

From FSL
Revision as of 17:15, 1 October 2015 by Grosu (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

From Rewriting Logic, to Programming Language Semantics, to Program Verification
Grigore Rosu
Meseguer's Festschrift, LNCS 9200, pp 598-616. 2015
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.
PDF, Slides(PPTX), K, DOI, Meseguer's Festschrift, BIB

Personal tools
Namespaces

Variants
Actions
Navigation