Dafny-style verification of MiniJava programs

Software verification is the process of proving that a program fulfils all of its expected requirements. It is a crucial component of software engineering and is vital for successful software. This project is in the area of software verification and attempts to create a Dafny style verification system for the MiniJava language. The system is part of a MiniJava compiler so programs can be verified at compile time. t contains the basic features of the Dafny programming language, a language with inbuilt specification constructs, as well as some of its more advanced ones if time permits. The verification specifications are defined by the programmer as part of the MiniJava source code. Any verification errors are displayed to the user. The project research will build such a system and determine whether or not every desire verification feature can be recreated in MiniJava. The project is focused specifically around the MiniJava language as a MiniJava compiler is available for use in the project and MiniJava is a very basic language with a limited feature set. These two aspects allow for the task to be feasible for a project of this scale.