The goal of this assignment is to write a simple program verification engine to verify a simple imperative language. For implementing the engine in this project you are free to use any programming language that you are comfortable with. The input to your engine is textual and the output is printed on the screen (standard output).

The small language of this assignment has the following expressions and statements. The type of identifiers in this language is (unbounded) integers. There is no need to type check a given program prior to verification, we assume that if the syntax of a program matches the given BNF then the program is valid. Due to simplicity of the language, no prior specific compiler construction knowledge is required for this assignment, you can use any simple syntax analysis technique to recognize the program structure.

• <Id> represents a sequence of letters, digits and underscores, starting with a letter and which is not a keyword. Identifiers are case-sensitive.
• <Int> the domain of (unbounded) integer numbers, with usual operations on them.
• <EOF> represents the special end-of-file character

Try to come up with a cool name for your verification engine that is related to what is does (e.g. bugkiller, securer, …). Your program will be called from the command-line using the following format where NAME is the name of your tool:

NAME [options] <sourcefile>.imp

Try to avoid using any other format since it will make grading the of your project difficult (and you may lose points if you do not follow this format). We will describe the possible options to your tool in each task.

Generate the control-flow-graph for the input program, as discussed in Lecture 23. For better testing the generated CFG, plot it using the dot program. dot is a very simple program for drawing directed graphs (http://www.graphviz.org/). If your program is called with the -c option, it will generate a png file that shows the CFG of the input imp program. Test your program with different benchmarks, it is important to ensure about the correctness of CFG generation before trying to verify programs.

Generate the set of Horn clauses representing the input program. If your verification engine is called with the -h option, it will print out the generated Horn clauses on the screen using the SMT-LIB format. Try a set of examples and inspect your Horn clauses to see if they are correct.

When the user calls your program with the -v argument, it will verify the input file by checking the satisfiability of the generated Horn clauses. For satisfiability you can consult an off-the-shelf Horn solver (e.g. Z3, Eldarica or Spacer). Your program will either print correct for a program with no bug. Or, it will write incorrect for a program that has bug. Note that if the program has no assert at all, we assume that there is nothing to be checked for it and it should be correct.

Bonus Print out the values under which the program will hit the error.

Note You can either install the theorem prover on your machine and your code executes the theorem prover as an external application (i.e. z3 can be called from the command line), or you can add the required libraries to call the theorem prover from its libraries.

The verification problem for the imp language in this project is undecidable. Can you find a simple program for which the back-end theorem prover runs forever? (if it does not return a result for e.g. half an hour it is a good sign that it will never stop)

The deadline of this project is November 10 at 11:59pm (https://mycourses.rit.edu). Please do not upload binary and executable files. Make a zip from your files to make uploading the files easier.

• Read the Homework Assignment Policies for the assignment policies of the course.
• This project can be done in groups of two students. If you choose to collaborate with another student, only one of you needs to upload the solution.
• Since you are free in choosing your programming language, it is important that you make it easy to build your project. Please include a Readme file in your submission to note how the user can build and run your program.