Austin Levi Carter
Title
Reverse Engineering Programs to Descartes Specification to Provide Proof of Validity and Accuracy with Desired Specifications
Abstract
The ability to do a check of fulfilled specifications on recently developed software is a need; as is the need to check that the software contains no malicious code. Reverse engineering programs (focusing on C++ in the early stages) to its specifications can help to show if the program fully fulfills its intended design. This method of reverse engineering programs helps with error checking and testing, making the whole process more efficient and less expensive. This research effort focuses on developing a method to transform C++ programs into Descartes specifications and to determine if it is possible to transform more complex programs into specification.