HW3 ‐ SMT (Satisfiability Modulo Theories) problems

The goal of this homework is to get familiar with solving SMT problems by using SMT solvers in Python to:

• formulate and solve simple SMT problems, and
• solve basic formal verification tasks via SMT.

Task

Your task is to walk through and solve each problem in the SMT.ipynb Jupyter notebook. Look for TODOs in the code which indicate the places where you need to add your solution. You have to submit the final version of your notebook as a single file.

There are points associated to the exercises in the notebook. Some basic introductory exercises have 0 points, they are required. You can achieve a maximum of 5 points; 2 points are required to pass the homework. Furthermore, you must solve at least one of the three exercises from the Verification exercises section. However, we recommend solving all tasks.

Workflow

You can download the notebook and work on your own computer or you can work with Google Colab for example. Below are some steps to import the notebook to Google Colab:

1. Go to Google Colab and sign in to your Google account.
2. Select File > Open notebook (this dialog may open automatically when you load Colab).
3. Select the GitHub option.
4. Provide the notebook URL: https://github.com/ftsrg-edu/avt-labs/blob/master/hw3-smt/SMT.ipynb
5. Select the notebook from the list.

Alternatively, you can download the file to your computer and upload it to Colab by choosing the Upload option. At the end of your work, download the notebook file by choosing File > Download > Download .ipynb.