\newchapter{Some applications}

\leveldown{}

\begin{itemize}
\item All sorts of theorem provers, including (but not limited to)
Isabelle\footnote{\url{http://isabelle.in.tum.de/}},
HOL...

\item Dafny (Microsoft Research)\footnote{\url{https://en.wikipedia.org/wiki/Dafny}}, uses Z3.

\item KLEE\footnote{\url{https://klee.github.io/}} (uses STP).

\item CBMC -- Bounded Model Checker for C and C++ programs: \url{http://www.cprover.org/cbmc/}.
Short intro to its innards: \url{http://www.cprover.org/cbmc/doc/cbmc-slides.pdf}.

\item Firewall checker, can check equivalence of two firewalls.
\url{https://github.com/Z3Prover/FirewallChecker}.
Nikolaj Bjørner and Karthick Jayaraman -- Checking Cloud Contracts in Microsoft Azure
\footnote{\url{https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-icdcit2015.pdf}},
Karthick Jayaraman, Nikolaj Bjørner, Geoff Outhred, Charlie Kaufman -- Automated Analysis and Debugging of Network Connectivity Policies
\footnote{\url{https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/secguru.pdf}}.

\item Frama-C -- a static analyzer, inspects programs without executing them
\footnote{\url{http://frama-c.com/}}.

\item VCC: A Verifier for Concurrent C
\footnote{\url{https://www.microsoft.com/en-us/research/project/vcc-a-verifier-for-concurrent-c/}}
-- a competitor to Frama-C from Microsoft Research. Seems to be stalled.

\item Boogie: An Intermediate Verification Language
\footnote{\url{https://www.microsoft.com/en-us/research/project/boogie-an-intermediate-verification-language/}}
(Microsoft Research). Used as a bridge between VCC and Z3.

\item Spec\# (Microsoft Research)

\item Why3 -- a platform for deductive program verification,
used in Frama-C\footnote{\url{http://why3.lri.fr/}}.

\item RISC-V Formal Verification Framework\footnote{\url{https://github.com/SymbioticEDA/riscv-formal}}

\item Yosys -- a framework for Verilog RTL synthesis\footnote{\url{http://www.clifford.at/yosys/}}.

\item IVy -- a tool for specifying, modeling, implementing and verifying protocols\footnote{\url{http://microsoft.github.io/ivy/}}. Uses Z3.

\item Cryptol
\footnote{\url{http://cryptol.net}, \url{https://github.com/GaloisInc/cryptol}}:
a language for cryptoalgorithms specification and proving it's correctness. Uses Z3.

\item SPARK -- a formally defined computer programming language based on the Ada.
It can use Alt-Ergo, Z3, CVC4, etc.

\item LiquidHaskell
\footnote{\url{https://ucsd-progsys.github.io/liquidhaskell-blog/}}.

\item Google's Operations Research tools has SAT/MaxSAT solver as an engine
\footnote{\url{https://github.com/google/or-tools/tree/v7.0/ortools/sat}}.

\item Musketeer -- A static analysis approach to automatic [memory] fence insertion
\footnote{\url{https://arxiv.org/pdf/1312.1411.pdf}, \url{http://www.cprover.org/wmm/musketeer/}}.

\item Averest is a framework for the specification, verification, and implementation of reactive systems
\footnote{\url{http://www.averest.org/}}.

\item OpenJML -- a program verification tool for Java programs that allows you to check the specifications of programs annotated in the Java Modeling Language
\footnote{\url{http://www.openjml.org/}}.
See also: ESC/Java.

\item Souper: A Synthesizing Superoptimizer\footnote{
\url{https://arxiv.org/abs/1711.04422},
\url{https://github.com/google/souper},
\url{https://news.ycombinator.com/item?id=10463312},
\url{https://blog.regehr.org/archives/1252}.}

\item See the list of "Use cases"
\footnote{\url{https://github.com/stp/stp/blob/master/docs/index.rst\#use-cases}} where the STP solver is used.
Also, for CVC4\footnote{\url{https://cvc4.github.io/third-party-applications.html}}.

\item Linux Kernel folks got interested in SAT:
\url{https://www.kernel.org/doc/html/latest/kbuild/kconfig-language.html\#full-sat-solver-for-kconfig},
\url{https://kernelnewbies.org/KernelProjects/kconfig-sat}.

\end{itemize}

\myheading{Compiler's optimization verification}

Your compiler optimized something out, but you're unsure if your optimization rules are correct, because there are lots of them.
You can prove the original expression and the optimized are equal to each other.

This is what I did for my toy decompiler: \ref{ToyDecompilerTestingZ3}.

``Alive'' project:

Nuno P. Lopes, David Menendez, Santosh Nagarakatte, John Regehr -- Practical Verification of Peephole Optimizations with Alive
\footnote{\url{http://web.ist.utl.pt/nuno.lopes/pubs/alive-cacm18.pdf}}.

Another paper: Provably Correct Peephole Optimizations with Alive
\footnote{\url{http://www.cs.utah.edu/~regehr/papers/pldi15.pdf}}.

At github: \url{https://github.com/nunoplopes/alive}.

Nuno Lopes -- Verifying Optimizations using SMT Solvers
\footnote{\url{https://llvm.org/devmtg/2013-11/slides/Lopes-SMT.pdf}}.

\myheading{All sorts of papers and articles I've found interesting}

\begin{itemize}

\item Martin Hořeňovský about master-key system
\footnote{\url{https://codingnest.com/modern-sat-solvers-fast-neat-and-underused-part-2-of-n/},
\url{https://codingnest.com/files/thesis.pdf}}.

\end{itemize}

\levelup{}