TU Darmstadt / ULB / TUbiblio

A Theorem Prover Backed Approach to Array Abstraction

Wasser, Nathan ; Bubel, Richard (2014)
A Theorem Prover Backed Approach to Array Abstraction.
Report, Bibliographie

Kurzbeschreibung (Abstract)

We present an extension to an on-demand abstraction framework, which integrates deductive verification and abstract interpretation. Our extension allows for a significantly higher precision when reasoning about programs containing arrays. We demonstrate the usefulness of our approach in the context of reasoning about secure information flow. In addition to abstracting arrays that may have been modified, our approach can also keep full precision while adding additional information about array elements which have been only read but not modified.

Typ des Eintrags: Report
Erschienen: 2014
Autor(en): Wasser, Nathan ; Bubel, Richard
Art des Eintrags: Bibliographie
Titel: A Theorem Prover Backed Approach to Array Abstraction
Sprache: Deutsch
Publikationsjahr: 2014
Zugehörige Links:
Kurzbeschreibung (Abstract):

We present an extension to an on-demand abstraction framework, which integrates deductive verification and abstract interpretation. Our extension allows for a significantly higher precision when reasoning about programs containing arrays. We demonstrate the usefulness of our approach in the context of reasoning about secure information flow. In addition to abstracting arrays that may have been modified, our approach can also keep full precision while adding additional information about array elements which have been only read but not modified.

ID-Nummer: TUD-CS-2014-0839
Fachbereich(e)/-gebiet(e): 20 Fachbereich Informatik > Software Engineering
20 Fachbereich Informatik
Hinterlegungsdatum: 31 Dez 2016 10:40
Letzte Änderung: 30 Mai 2018 12:51
PPN:
Export:
Suche nach Titel in: TUfind oder in Google
Frage zum Eintrag Frage zum Eintrag

Optionen (nur für Redakteure)
Redaktionelle Details anzeigen Redaktionelle Details anzeigen