Z3

Analyzing programs with Z3: https://www.youtube.com/watch?v=ruNFcH-KibY

Software Synthesis via sketching thesis http://people.csail.mit.edu/asolar/papers/thesis.pdf

ericpony.github.io/z3py-tutorial/guide-examples.htm
http://ericpony.github.io/z3py-tutorial/advanced-examples.htm
https://theory.stanford.edu/~nikolaj/programmingz3.html
A big tutorial: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.225.8231&rep=rep1&type=pdf
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.367.9961&rep=rep1&type=pdf

Strategies/goals/tactics: http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/strategies-examples.htm

Modelling a logic puzzle. Interesting because it uses uninterpreted functions https://stackoverflow.com/questions/53711168/modelling-a-logic-puzzle

An example of using z3 regular expressions to restrict possible strings: https://stackoverflow.com/questions/53808101/defining-constraints-in-z3-using-boolean-operators

In the 2018 talks, there’s a section on code synthesis using z3 https://cseweb.ucsd.edu/~npolikarpova/

A series of posts on using z3 to generate traces for ARM instructions https://alastairreid.github.io/tracing-smt3/

A  book chapter on ways to apply z3 to program verification https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-smt-application-chapter.pdf

Showing how to do logic puzzles in z3 https://davidsherenowitsa.party/2018/09/19/solving-logic-puzzles-with-z3.html It’s a nice example of using z3 Function types 


https://colab.research.google.com/github/philzook58/z3_tutorial/blob/master/Z3%20Tutorial.ipynb