Automatically Verifying Temporal Alignment of Transformed Software
Abstract
We propose to develop scalable methods for automatically proving correctness of a wide range of programtransformations including fe"ature preservation, feature removal, and security hardening. Our key enabling insight isthat scalability can be achieved by automat""ically discovering an alignment between a source program and itstransformation, guided automatically extracted temporal logic speci"fications that focus on the differences betweenprograms. We believe that we can achieve impact by drawing together and building upon PI Stephen Magill sframework for analyzing binary programs and PI Eric Koskinen s recent work that have made temporal verificatio"n ofindustrial programs practical. At the core of our work will be a novel, multi-faced, compositional temporal verificationstrate""gy.We aim to achieve: (i) Foundational results that span systems, program analysis, and automated verification. (ii)Development of"" a corpus of examples and metrics, drawn from TA1, TA2, TA3. (iii) An integrated toolkit for verifyingthe correctness of transforme"d binary programs.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Sep 01, 2017
- Source ID
- N000141712787
Entities
People
- Eric Koskinen
Organizations
- Office of Naval Research
- Stevens Institute of Technology
- United States Navy