For this class, we are going to look at the DIVA artifact. ICSE has a great artifact culture, so the artifact is all packaged up and ready to go for us in a VM. (With that said, please install the VM before class, and make sure it works on your computer.)
We will rerun parts of the evaluation of DIVA, and peek into the output to see what the proofs it produces looks like, and how it fails when it fails. We'll also discuss a bit about what reproducibility really means in the context of machine learning tools (we would need fancy hardware to retrain the model, for example, and determinism seems to be near impossible), and how tactic prediction models could be integrated into proof engineering workflows.
- Install VirtualBox if you do not already have it.
icse2022.ovafrom the official artifact package.
README.mdfrom the unzipped directory.
- Follow the instructions from
README.mdto install the VM and run DIVA on a single project.
If you have any trouble, please post your questions in this thread. Please also drop any installation tips you have in that thread.
If installation fails, and the class forums are no help, do not panic; we will try to match you with someone in class for whom installation worked.
You can find the exercise we will do together in class below.