Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
Zur Ablage hinzufügen
 Lokale TagsFreigabegeschichteDetailsÜbersicht
  Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants

Kapur, D., Zhang, Z., Horbach, M., Zhao, H., Lu, Q., & Nguyen, T. (2013). Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants. In M. P. Bonacina, & M. E. Stickel (Eds.), Automated Reasoning and Mathematics (pp. 189-228). Berlin: Springer. doi:10.1007/978-3-642-36675-8_11.

Item is

 

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:
Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-0019-8385-C Versions-Permalink: https://hdl.handle.net/11858/00-001M-0000-0019-8387-8
Genre: Buchkapitel

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Kapur, Deepak1, Autor
Zhang, Zhihai1, Autor
Horbach, Matthias1, Autor           
Zhao, Hantao1, Autor
Lu, Qi1, Autor
Nguyen, ThanhVu1, Autor
Affiliations:
1External Organizations, ou_persistent22              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: Geometric heuristics for the quantifier elimination approach presented by Kapur (2004) are investigated to automatically derive loop invariants expressing weakly relational numerical properties (such as l ≤ x ≤ h or l ≤ \pm x \pm y ≤q h) for imperative programs. Such properties have been successfully used to analyze commercial software consisting of hundreds of thousands of lines of code (using for example, the Astrée tool based on abstract interpretation framework proposed by Cousot and his group). The main attraction of the proposed approach is its much lower complexity in contrast to the abstract interpretation approach (O(n^2) in contrast to O(n^4), where n is the number of variables) with the ability to still generate invariants of comparable strength. This approach has been generalized to consider disjunctive invariants of the similar form, expressed using maximum function (such as \max(x+a,y+b,z+c,d) ≤ \max(x+e,y+f,z+g,h)), thus enabling automatic generation of a subclass of disjunctive invariants for imperative programs as well.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 20132013
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: BibTex Citekey: Horbach2013McCune
DOI: 10.1007/978-3-642-36675-8_11
 Art des Abschluß: -

Veranstaltung

einblenden:

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Automated Reasoning and Mathematics
  Untertitel : Essays in Memory of William McCune
Genre der Quelle: Buch
 Urheber:
Bonacina, Maria Paola1, Herausgeber
Stickel, Mark E.1, Herausgeber
Affiliations:
1 External Organizations, ou_persistent22            
Ort, Verlag, Ausgabe: Berlin : Springer
Seiten: - Band / Heft: - Artikelnummer: - Start- / Endseite: 189 - 228 Identifikator: ISBN: 978-3-642-36674-1
ISBN: 978-3-642-36675-8

Quelle 2

einblenden:
ausblenden:
Titel: Lecture Notes in Computer Science
  Kurztitel : LNCS
Genre der Quelle: Reihe
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: -
Seiten: - Band / Heft: 7788 Artikelnummer: - Start- / Endseite: - Identifikator: ISSN: 0302-9743