Abstract

Software is used in many critical systems in the real world such as autonomous cars and medical devices. Such software must be reliable to protect the general public. One standard way to make reliable software is to use Hoare-style verification techniques. However, for Hoare-style verification of loop correctness, loop invariants are necessary but are difficult for people to write themselves. Since Java is one of the most popular programming languages in the world, it is useful to have a tool to generate loop invariants for Java programs. OpenJML is a widely used program verification tool for Java. However, it does not provide automatic loop invariant generation. Therefore, the problem that this thesis addresses is to automatically generate loop invariants in OpenJML. The plan is to use a third-party tool to achieve this goal. Since this external tool does not support Java, a package is necessary to translate from Java/JML to the syntax of the loop invariant tool. However, there are a few conditions that the package has to meet. Since the programming language that the third- party tool supports has a limited grammar, we have to work around unsupported syntax. The resulting package is successful because it can integrate a loop invariant generation tool with OpenJML. Therefore, this package may help developers produce more reliable Java programs.

Notes

If this is your thesis or dissertation, and want to learn how to access it or for more information about readership statistics, contact us at STARS@ucf.edu

Graduation Date

2022

Semester

Summer

Advisor

Leavens, Gary

Degree

Master of Science (M.S.)

College

College of Engineering and Computer Science

Department

Computer Science

Degree Program

Computer Science

Identifier

CFE0009206; DP0026810

URL

https://purls.library.ucf.edu/go/DP0026810

Language

English

Release Date

August 2022

Length of Campus-only Access

None

Access Status

Masters Thesis (Open Access)

Download

Share

COinS