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

Thomas Martin Gawlitza; Helmut Seidl

doi:10.1007/978-3-642-15769-1_17

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

Thomas Martin Gawlitza, Helmut Seidl

Informatik 2 - Lehrstuhl für Sprachen und Beschreibungsstrukturen in der Informatik

UJF-Grenoble 1, CNRS VERIMAG UMR 5104

Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

16 Zitate (Scopus)

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].

Originalsprache	Englisch
Titel	Static Analysis - 17th International Symposium, SAS 2010, Proceedings
Seiten	271-286
Seitenumfang	16
DOIs	https://doi.org/10.1007/978-3-642-15769-1_17
Publikationsstatus	Veröffentlicht - 2010
Veranstaltung	17th International Static Analysis Symposium, SAS 2010 - Perpignan, Frankreich Dauer: 14 Sept. 2010 → 16 Sept. 2010

Publikationsreihe

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Band	6337 LNCS
ISSN (Print)	0302-9743
ISSN (elektronisch)	1611-3349

Konferenz

Konferenz	17th International Static Analysis Symposium, SAS 2010
Land/Gebiet	Frankreich
Ort	Perpignan
Zeitraum	14/09/10 → 16/09/10

Zugriff auf Dokument

10.1007/978-3-642-15769-1_17

Andere Dateien und Links

Verknüpfung zur Publikation in Scopus

Dieses zitieren

Gawlitza, T. M., & Seidl, H. (2010). Computing relaxed abstract semantics w.r.t. quadratic zones precisely. in Static Analysis - 17th International Symposium, SAS 2010, Proceedings (S. 271-286). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 6337 LNCS). https://doi.org/10.1007/978-3-642-15769-1_17

@inproceedings{5c32dc1f0e654b1c97b76631a31262b3,

title = "Computing relaxed abstract semantics w.r.t. quadratic zones precisely",

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{\'e} et al. [2]. We use a relaxed abstract semantics which is at least as precise as the relaxed abstract semantics of Adj{\'e} 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].",

author = "Gawlitza, {Thomas Martin} and Helmut Seidl",

note = "Funding Information: This work was partially funded by the ANR project ASOPT.; 17th International Static Analysis Symposium, SAS 2010 ; Conference date: 14-09-2010 Through 16-09-2010",

year = "2010",

doi = "10.1007/978-3-642-15769-1_17",

language = "English",

isbn = "3642157688",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "271--286",

booktitle = "Static Analysis - 17th International Symposium, SAS 2010, Proceedings",

}

Gawlitza, TM & Seidl, H 2010, Computing relaxed abstract semantics w.r.t. quadratic zones precisely. in Static Analysis - 17th International Symposium, SAS 2010, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bd. 6337 LNCS, S. 271-286, 17th International Static Analysis Symposium, SAS 2010, Perpignan, Frankreich, 14/09/10. https://doi.org/10.1007/978-3-642-15769-1_17

Computing relaxed abstract semantics w.r.t. quadratic zones precisely. / Gawlitza, Thomas Martin; Seidl, Helmut.
Static Analysis - 17th International Symposium, SAS 2010, Proceedings. 2010. S. 271-286 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 6337 LNCS).

Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

TY - GEN

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

AU - Gawlitza, Thomas Martin

AU - Seidl, Helmut

N1 - Funding Information: This work was partially funded by the ANR project ASOPT.

PY - 2010

Y1 - 2010

N2 - 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].

AB - 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].

UR - http://www.scopus.com/inward/record.url?scp=78149246738&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-15769-1_17

DO - 10.1007/978-3-642-15769-1_17

M3 - Conference contribution

AN - SCOPUS:78149246738

SN - 3642157688

SN - 9783642157684

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 271

EP - 286

BT - Static Analysis - 17th International Symposium, SAS 2010, Proceedings

T2 - 17th International Static Analysis Symposium, SAS 2010

Y2 - 14 September 2010 through 16 September 2010

ER -

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

Abstract

Publikationsreihe

Konferenz

Zugriff auf Dokument

Andere Dateien und Links

Fingerprint

Dieses zitieren