The Continuation of Automating Program Verification: Generating Automatic Methods to Determine the Behavior of Algorithms
by Charles D. Lindsey
Major: computer science
An algorithm is a sequence of steps to solve a problem. It can be represented as text. When this text is translated to a form of the guarded command language-a programming language created by Edsger Dijkstra-the algorithm can often be mechanically verified as a solution to the problem it is supposed to solve or as an inadequate solution to this problem. I am developing a program that will do this verification.
I received $500 from the fund this year to support this project. It has been spent on reference materials. This year I have stepped back from coding and focused on developing a formal mathematical model for programs, the data they operate on, and the verification functions used upon them. This composes the bulk of the text of my honors thesis.
I have completed a prototype model. There are other results of my research that should be useful in the future, but they are not yet verified. For instance, general recursion is not allowed within the prototype model, but I have a theory as to its verification.
The model still needs to be fully implemented. The coding that I have done in the past should compose part of this implementation. In the future I plan to fully develop the model and the code to implement it.
The research is significant because programming errors can be dangerous and costly. By automating the process, verification of algorithms may become easier.
Completion of the project may result in a project of great utility. The altered guarded command language can perhaps be further altered to support modern object-oriented programming. Programs, which translate a program written in one language to a program written in the altered guarded command language, may be developed. This may help all programmers to see whether their programs will do what they want them to do.