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 |
| Corresponding Links: | |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Send an inquiry |
Options (only for editors)
 |
Show editorial Details |
Drucken
Impressum