10.4230/LIPICS.RTA.2010.151
Hills, Mark
Mark
Hills
Rosu, Grigore
Grigore
Rosu
A Rewriting Logic Semantics Approach to Modular Program Analysis
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2010
Article
K
rewriting logic semantics
program analysis
Lynch, Christopher
Christopher
Lynch
2010
2010-07-06
2010-07-06
2010-07-06
en
urn:nbn:de:0030-drops-26506
10.4230/LIPIcs.RTA.2010
978-3-939897-18-7
1868-8969
10.4230/LIPIcs.RTA.2010
LIPIcs, Volume 6, RTA 2010
Proceedings of the 21st International Conference on Rewriting Techniques and Applications
2013
6
13
151
160
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Lynch, Christopher
Christopher
Lynch
1868-8969
Leibniz International Proceedings in Informatics (LIPIcs)
2010
6
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
10 pages
138463 bytes
application/pdf
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
info:eu-repo/semantics/openAccess
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.
LIPIcs, Vol. 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications, pages 151-160