Computing relaxed abstract semantics w.r.t. quadratic zones precisely

Thomas Martin Gawlitza, Helmut Seidl

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

16 Scopus citations

Abstract

In the present paper we compute numerical invariants of programs by abstract interpretation. For that we consider the abstract domain of quadratic zones recently introduced by Adjé et al. [2]. We use a relaxed abstract semantics which is at least as precise as the relaxed abstract semantics of Adjé et al. [2]. For computing our relaxed abstract semantics, we present a practical strategy improvement algorithm for precisely computing least solutions of fixpoint equation systems, whose right-hand sides use order-concave operators and the maximum operator. These fixpoint equation systems strictly generalize the fixpoint equation systems considered by Gawlitza and Seidl [11].

Original languageEnglish
Title of host publicationStatic Analysis - 17th International Symposium, SAS 2010, Proceedings
Pages271-286
Number of pages16
DOIs
StatePublished - 2010
Event17th International Static Analysis Symposium, SAS 2010 - Perpignan, France
Duration: 14 Sep 201016 Sep 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6337 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference17th International Static Analysis Symposium, SAS 2010
Country/TerritoryFrance
CityPerpignan
Period14/09/1016/09/10

Fingerprint

Dive into the research topics of 'Computing relaxed abstract semantics w.r.t. quadratic zones precisely'. Together they form a unique fingerprint.

Cite this