From rewriting logic, to programming language semantics, to program verification

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 핂, 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.

Original languageEnglish (US)
Title of host publicationLogic, Rewriting and Concurrency - Essays Dedicated to Jose Meseguer on the Occasion of His 65th Birthday
EditorsPeter Csaba Ölveczky, Carolyn Talcott, Narciso Martí-Oliet
PublisherSpringer
Pages598-616
Number of pages19
ISBN (Print)9783319231648
DOIs
StatePublished - Jan 1 2015
EventConference on Logic, Rewriting and Concurrency dedicated to Jose Meseguer on the Occasion of his 65th Birthday, 2015 - Champaign, United States
Duration: Sep 23 2015Sep 25 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9200
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

OtherConference on Logic, Rewriting and Concurrency dedicated to Jose Meseguer on the Occasion of his 65th Birthday, 2015
Country/TerritoryUnited States
CityChampaign
Period9/23/159/25/15

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'From rewriting logic, to programming language semantics, to program verification'. Together they form a unique fingerprint.

Cite this