Verification of correctness properties of programs that read input files

This thesis presents new techniques for verifying correctness properties of programs that process input files. These techniques apply to programs written in standard programming languages such as C and focus on relationships that must hold between program execution points, the current location of file position indicator of the open input file, and the contents of the input file. The thesis presents a specification language that developers can use to express these relationships and insert them into the program as assertions involving the file position indicator and file contents at different program points. It also presents a program verification system that verifies, for all possible input files and all possible input file contents, that the assertions hold in all program executions. The soundness of the verification system has been proved, based on the formal definition of the syntax and semantics of the specification language. The system synthesized verification conditions from the specifications for a PNG image viewer and a JPEG image converter, and successfully verified all of them.

Name thesis:degree_name

Doctoral

Department dc:contributor.department

Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science

Grantor dc:publisher

Massachusetts Institute of Technology

Year dc:date.issued

2019

Author dc:creator

• Kim, Deokhwan,Ph. D.Massachusetts Institute of Technology.

Advisor dc:contributor.advisor

• Martin C. Rinard.

• Electrical Engineering and Computer Science.

Statement dc:rights

• MIT theses are protected by copyright. They may be viewed, downloaded, or printed from this source but further reproduction or distribution in any format is prohibited without written permission.

Licence dc:rights.uri

• http://dspace.mit.edu/handle/1721.1/7582

Language dc:language.iso

eng

Handle dc:identifier.uri

https://hdl.handle.net/1721.1/124063

OAI identifier oai:identifier

oai:dspace.mit.edu:1721.1/124063