Blog

For this exercise you will build a Z3 model for reaching analysis for the factorial program we have been looking at in class. Reall the factorial program has the following form:

```
Y := X;
Z := 1;
while 1<Y do
Z := Z * Y;
Y := Y - 1;
Y := 0
```

In your model you should show that:

`X`

has not been initiatlized at the end of the program- The assignment of
`Z`

at either label 2 and 4 may reach label 6 - The assignment of
`Z`

at label 2 does not reach label 5 - There is no model where
`X`

has been assigned before program exit.

Each of these may involve one or more assertions and SAT checks based on how you build your model. There are many ways to accomplish this modeling task and I encourage you to be creative!

This project is a warm-up for the next project where you will build a general purpose reaching analysis tool.