This class was taken by me in my Spring 2024 semester. This course goes through different software and methods for verifying correctness and model checking. This course was split into three parts: z3, Dafny, and model checking/NuSMV. Below I will go through each part and talk about what homeoworks were in that part. We also had a final project where we had to research and present on a formal method software and I chose Isabelle theorm prover.
z3 is an SMT checker and we worked with all kinds of logic and problems. The homework on this are hw1 through hw4.
Dafny is used to verify correcness of code using pre/posconditions and invarients. These homeworks are hw5 through hw7.
Lastly, we used NuSMV to verify the correctness of models. This is done in hw9.
Isabelle theorm prover is a software used to verify and formalize mathematics proofs, computer science theorms, and various protocals. In this folder you can find my power point presentation, transcript of my presentation, and a plethora of example files.