An abstract specification language for static program analysis

Michael Vistein; Frank Ortmeier; Wolfgang Reif; Ralf Huuck; Ansgar Fehnker

doi:10.1016/j.entcs.2009.09.066

An abstract specification language for static program analysis

Michael Vistein, Frank Ortmeier, Wolfgang Reif, Ralf Huuck, Ansgar Fehnker

Research output: Contribution to journal › Article › peer-review

3 Citations (Scopus)

26 Downloads (Pure)

Abstract

Static program analysers typically come with a set of hard-coded checks, leaving little room for the user to add additional properties. In this work, we present a uniform approach to enable the specification of new static analysis checks in a concise manner. In particular, we present our GPSL/GXSL language to define new control flow checks. The language is closely related to CTL specifications that are combined with XPath queries. Moreover, we provide a number of specifications as implemented in our tool Goanna, and report on our experiences of adding new checks.

Original language	English
Pages (from-to)	181-197
Number of pages	17
Journal	Electronic Notes in Theoretical Computer Science
Volume	254
DOIs	https://doi.org/10.1016/j.entcs.2009.09.066
Publication status	Published - 28 Oct 2009
Externally published	Yes
Event	4th International Workshop on Systems Software Verification, SSV 2009 - Aachen, Germany Duration: 22 Jun 2009 → 24 Jun 2009

Bibliographical note

Copyright the Publisher 2009. Version archived for private and non-commercial use with the permission of the author/s and according to publisher conditions. For further rights please contact the publisher.

Keywords

Abstract specification
static analysis
CTL specification
GPSL/GXSL
XPATH query

Access to Document

10.1016/j.entcs.2009.09.066

Publisher version (open access)Final published version, 368 KBLicence: CC BY-NC-ND

Cite this

@article{5e6fbbf5a44b4d50a48b7f1b2dba10f8,

title = "An abstract specification language for static program analysis",

abstract = "Static program analysers typically come with a set of hard-coded checks, leaving little room for the user to add additional properties. In this work, we present a uniform approach to enable the specification of new static analysis checks in a concise manner. In particular, we present our GPSL/GXSL language to define new control flow checks. The language is closely related to CTL specifications that are combined with XPath queries. Moreover, we provide a number of specifications as implemented in our tool Goanna, and report on our experiences of adding new checks.",

keywords = "Abstract specification, static analysis, CTL specification, GPSL/GXSL, XPATH query",

author = "Michael Vistein and Frank Ortmeier and Wolfgang Reif and Ralf Huuck and Ansgar Fehnker",

note = "Copyright the Publisher 2009. Version archived for private and non-commercial use with the permission of the author/s and according to publisher conditions. For further rights please contact the publisher.; 4th International Workshop on Systems Software Verification, SSV 2009 ; Conference date: 22-06-2009 Through 24-06-2009",

year = "2009",

month = oct,

day = "28",

doi = "10.1016/j.entcs.2009.09.066",

language = "English",

volume = "254",

pages = "181--197",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier",

}

TY - JOUR

T1 - An abstract specification language for static program analysis

AU - Vistein, Michael

AU - Ortmeier, Frank

AU - Reif, Wolfgang

AU - Huuck, Ralf

AU - Fehnker, Ansgar

N1 - Copyright the Publisher 2009. Version archived for private and non-commercial use with the permission of the author/s and according to publisher conditions. For further rights please contact the publisher.

PY - 2009/10/28

Y1 - 2009/10/28

N2 - Static program analysers typically come with a set of hard-coded checks, leaving little room for the user to add additional properties. In this work, we present a uniform approach to enable the specification of new static analysis checks in a concise manner. In particular, we present our GPSL/GXSL language to define new control flow checks. The language is closely related to CTL specifications that are combined with XPath queries. Moreover, we provide a number of specifications as implemented in our tool Goanna, and report on our experiences of adding new checks.

AB - Static program analysers typically come with a set of hard-coded checks, leaving little room for the user to add additional properties. In this work, we present a uniform approach to enable the specification of new static analysis checks in a concise manner. In particular, we present our GPSL/GXSL language to define new control flow checks. The language is closely related to CTL specifications that are combined with XPath queries. Moreover, we provide a number of specifications as implemented in our tool Goanna, and report on our experiences of adding new checks.

KW - Abstract specification

KW - static analysis

KW - CTL specification

KW - GPSL/GXSL

KW - XPATH query

U2 - 10.1016/j.entcs.2009.09.066

DO - 10.1016/j.entcs.2009.09.066

M3 - Article

SN - 1571-0661

VL - 254

SP - 181

EP - 197

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

T2 - 4th International Workshop on Systems Software Verification, SSV 2009

Y2 - 22 June 2009 through 24 June 2009

ER -

An abstract specification language for static program analysis

Abstract

Bibliographical note

Keywords

Access to Document

Fingerprint

Cite this