Online resources
This book and associated slides teach how the decision procedure works in the SMT solver for different theories such as bit-vectors or linear real arthimetic, which is helpful for understanding the solver statistics.
This website gives an online tutorial of Z3. It seems to cover the same topics as the Python version Programming Z3, which I am currently looking at, but instead this website uses SMT-LIBv2 language.
This website gives more examples on how to use z3 python API to do different things
This course teaches formal methods of verifications and synthesis. The instructor is famous.
This lecture slides introduces what is propositional interpolation.
This slide from JHU gives intresting examples of first-order logic.
This course covers many topics related to Z3, such as bounded model checking. The instructor also teaches other related courses.
- This instructor has research on functional program verification
Papers
The following papers are introduced by Programming Z3.
This paper introduces the algorithm of “cube and conquer”, which is a technique used in Z3 to increase the scalability by partitioning the search space into sub-problems that can be solved in parallel.
The above papers introduce algorithms to enumeraring all maximal satisfying subsets and minimal unsat cores together.
Thid book chapter introduces bounded model checking, which is a technique to check reachability problems between two states.