A rewriting logic semantics approach to modular program analysis

Mark Hills, Grigore Roşu

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

Abstract

The K framework, based on rewriting logic semantics, provides a powerful logic for defining the semantics of programming languages. While most work in this area has focused on defining an evaluation semantics for a language, it is also possible to define an abstract semantics that can be used for program analysis. Using the SILF language (Hills, Serbanuta and Rosu, 2007), this paper describes one technique for defining such a semantics: policy frameworks. In policy frameworks, an analysis-generic, modular framework is first defined for a language. Individual analyses, called policies, are then defined as extensions of this framework, with each policy defining analysis-specific semantic rules and an annotation language which, in combination with support in the language frontend, allows users to annotate program types and functions with information used during program analysis. Standard term rewriting techniques are used to analyze programs by evaluating them in the policy semantics.

Original languageEnglish (US)
Title of host publicationProceedings of the 21st International Conference on Rewriting Techniques and Applications, RTA 2010
Pages151-160
Number of pages10
StatePublished - Dec 1 2010
Event21st International Conference on Rewriting Techniques and Applications, RTA 2010 - Edinburgh, United Kingdom
Duration: Jul 11 2010Jul 13 2010

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume6
ISSN (Print)1868-8969

Other

Other21st International Conference on Rewriting Techniques and Applications, RTA 2010
CountryUnited Kingdom
CityEdinburgh
Period7/11/107/13/10

Keywords

  • K
  • Program analysis
  • Rewriting logic semantics

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'A rewriting logic semantics approach to modular program analysis'. Together they form a unique fingerprint.

Cite this