reading.tex

\chapter{Further reading}

\begin{itemize}
\item Julien Vanegue, Sean Heelan, Rolf Rolles -- SMT Solvers for Software Security
\footnote{\url{https://yurichev.com/mirrors/SMT/woot12.pdf}}

\item Armin Biere, Marijn Heule, Hans van Maaren, Toby Walsh -- Handbook of Satisfiability (2009)

\item Rui Reis -- Practical Symbolic Execution and SATisfiability Module Theories (SMT) 101
\footnote{\url{http://deniable.org/reversing/symbolic-execution}}.

\item Daniel Kroening and Ofer Strichman -- Decision Procedures -- An Algorithmic Point of View
\footnote{\url{http://www.decision-procedures.org}}.

\item Henry Warren -- Hacker's Delight.
Some people say these branchless tricks and hacks were only relevant for old RISC CPUs, so you don't need to read it.
Nevertheless, these hacks and understanding them helps immensely to get into boolean algebra and all the mathematics.
\end{itemize}

Z3-specific:

\begin{itemize}
\item Z3 API in Python
\footnote{\url{http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/guide-examples.htm}}

\item Z3 Strategies
\footnote{\url{http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/strategies-examples.htm}}

\item Nikolaj Bjørner -- Recent Trends in SMT and Z3: An interactive taste of SMT with Z3
\footnote{\url{http://www.cse.chalmers.se/~laurako/links/ADuctSlides/L10.html}}.

\item Nikolaj Bjørner, Leonardo de Moura, Lev Nachmanson, Christoph Wintersteiger -- Programming Z3
\footnote{\url{http://theory.stanford.edu/~nikolaj/programmingz3.html}}.

\item Questions tagged [z3] on Stack Overflow
\footnote{\url{https://stackoverflow.com/questions/tagged/z3}}.
\end{itemize}

SAT-specific:

\begin{itemize}

\item Niklas Een, Niklas Sorensson -- Translating Pseudo-Boolean Constraints into SAT
\footnote{\url{http://minisat.se/downloads/MiniSat+.pdf}}.

\item Donald Knuth -- \ac{TAOCP} 7.2.2.2. Satisfiability
\footnote{\url{http://www-cs-faculty.stanford.edu/~knuth/fasc6a.ps.gz}}.

\item Armin Biere -- Using High Performance SAT and QBF Solvers\footnote{\url{http://fmv.jku.at/biere/talks/Biere-TPTPA11.pdf}}.

\item \url{https://en.wikipedia.org/wiki/Tseytin_transformation}

\item Martin Finke -- Equisatisfiable SAT Encodings of Arithmetical Operations
\footnote{\url{http://www.martin-finke.de/documents/Masterarbeit_bitblast_Finke.pdf}}.

\end{itemize}

SMT-specific:

\begin{itemize}
\item Theories: \url{http://smtlib.cs.uiowa.edu/logics.shtml}, \url{https://cs.nyu.edu/pipermail/smt-lib/2005/000046.html}.

\item SMT-LIB mailing list: \url{https://cs.nyu.edu/pipermail/smt-lib/}.

\item David R. Cok -- The SMT-LIBv2 Language and Tools: A Tutorial: \url{http://smtlib.github.io/jSMTLIB/SMTLIBTutorial.pdf}.

\end{itemize}

Also recommended by Armin Biere:

\begin{itemize}
\item Stuart Russell and Peter Norvig -- Artificial Intelligence: A Modern Approach

\item Helmut Veith, Edmund M. Clarke, Thomas A. Henzinger -- Handbook of Model Checking

\item Christos Papadimitriou -- Computational Complexity (1994)
\end{itemize}