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 |
Optionen (nur für Redakteure)
Redaktionelle Details anzeigen |