Software Verification (Homework)
		   ================================


Homework archive
----------------
The archive encloses a skeleton of your project with:

- This README file.

- A description of the project in 'homework.pdf'.

- The '.mli' files that define the API of the whole project.
  Run 'make doc' to generate the HTML documentation of the
  modules and visit './doc/index.html' with a web browser to
  look at it.

- A few '.ml' files (implemented modules) to provide you functions to
  help you to focus on the heart of the program (look at it and use it
  to save time!).

- An example usage of the Z3 OCaml API in the file 'z3_ml_example.ml'.
  Compile it with 'make z3_ml_example.byte'.

- Once your have implemented enough of the two missing modules (see
  below), you can try to compile the whole thing with: 'make'.  You
  can also run a few unit tests with 'make test'.

- A binary program 'bmc.d.byte' to give you a taste of the final
  model-checking program that you should obtain.


What to code
------------
You need to implement the following OCaml modules:

- 'Semantics.ml': Translate the operators of the program
  into Z3 expressions in the integer theory module.

- 'BoundedModelChecking.ml': Explore all the feasible paths in
  depth-first search with a bounded depth. And, returns the result of
  the exploration.


How and when to send your homework
----------------------------------
The deadline for the project is on Friday, December 16, 2016 at 14h00.
Send an archive with your full project to gregoire.sutre@labri.fr.

Your archive should contain the whole project plus:

- The 'Semantics.ml' and the 'BoundedModelChecking.ml' modules fully
  implemented.

- A few extra tests for the implemented modules.

- A report (written in LaTeX but sent as a PDF file) about your
  implementation and the choices that you had to do while programming.