Interpreting abstract interpretations in membership equational logic

Bernd Fischer, Grigore Roşu

Research output: Contribution to journalConference articlepeer-review

Abstract

We present a logical framework in which abstract interpretations can be naturally specified and then verified. Our approach is based on membership equational logic which extends equational logics by membership axioms, asserting that a term has a certain sort. We represent an abstract interpretation as a membership equational logic specification, usually as an overloaded order-sorted signature with membership axioms. It turns out that, for any term, its least sort over this specification corresponds to its most concrete abstract value. Maude implements membership equational logic and provides mechanisms to calculate the least sort of a term efficiently. We first show how Maude can be used to get prototyping of abstract interpretations "for free." Building on the meta-logic facilities of Maude, we further develop a tool that automatically checks an abstract interpretation against a set of user-defined properties. This can be used to select an appropriate abstract interpretation, to characterize the specific loss of information during abstraction, and to compare different abstractions with each other.

Original languageEnglish (US)
Pages (from-to)271-285
Number of pages15
JournalElectronic Notes in Theoretical Computer Science
Volume59
Issue number4
DOIs
StatePublished - Nov 2001
Externally publishedYes
EventRULE 2001, Second International Workshop on Rule-Based Programming (Satellite Event of PLI 2001) - Firenze, Italy
Duration: Sep 4 2001Sep 4 2001

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Interpreting abstract interpretations in membership equational logic'. Together they form a unique fingerprint.

Cite this