apps.tex

\chapter{Some applications}

\begin{itemize}

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

\item CBMC -- Bounded Model Checker for C and C++ programs
\footnote{\url{http://www.cprover.org/cbmc/}}.

\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 \url{http://angr.io} - static and dynamic symbolic ("concolic") analysis.

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

\item Many theorem provers, including Isabelle.

\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 protcols\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 prooving it's correctness. Uses Z3.

\end{itemize}

\section{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 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}}.