License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2010.151
URN: urn:nbn:de:0030-drops-26506
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2010/2650/
Go to the corresponding LIPIcs Volume Portal

Hills, Mark ; Rosu, Grigore

A Rewriting Logic Semantics Approach to Modular Program Analysis

pdf-format:
10002.HillsMark.2650.pdf (0.1 MB)

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 front-end, 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.

BibTeX - Entry

@InProceedings{hills_et_al:LIPIcs:2010:2650,
  author =	{Mark Hills and Grigore Rosu},
  title =	{{A Rewriting Logic Semantics Approach to Modular Program Analysis}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{151--160},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Christopher Lynch},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2010/2650},
  URN =		{urn:nbn:de:0030-drops-26506},
  doi =		{10.4230/LIPIcs.RTA.2010.151},
  annote =	{Keywords: K, rewriting logic semantics, program analysis}
}

Keywords: K, rewriting logic semantics, program analysis
Collection: Proceedings of the 21st International Conference on Rewriting Techniques and Applications
Issue Date: 2010
Date of publication: 06.07.2010

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI