TU Darmstadt / ULB / TUbiblio

A Theorem Prover Backed Approach to Array Abstraction

Wasser, Nathan and Bubel, Richard (2014):
A Theorem Prover Backed Approach to Array Abstraction.
[Report]

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.

Item Type: Report
Erschienen: 2014
Creators: Wasser, Nathan and Bubel, Richard
Title: A Theorem Prover Backed Approach to Array Abstraction
Language: German
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.

Divisions: 20 Department of Computer Science > Software Engineering
20 Department of Computer Science
Date Deposited: 31 Dec 2016 10:40
Identification Number: TUD-CS-2014-0839
Related URLs:
Export:
Suche nach Titel in: TUfind oder in Google
Send an inquiry Send an inquiry

Options (only for editors)

View Item View Item