Satisfiability Modulo Theories (SMT) solvers are general-purpose engines that can decide whether a given set of constraints is satisfiable.
Their expressiveness and efficiency make them well-suited for many applications, and they have been, and continue to be successfully adopted by both industry and academia.
I will start this talk by briefly describing what is the SMT problem, and why it is a useful one. Then, I will present several works that either use SMT-solvers or improve them (or both) to increase the level of trust in three application domains.
For compiler optimizations, it will be shown that correctness can be proven beyond what current approaches guarantee.
For smart contracts, I will describe some advancements in SMT-solving that are needed in order to verify them.
Finally, I will show how to improve the level of trust we can have in SMT-solvers themselves, and how they are being used in the process.
Yoni Zohar is a postdoctoral researcher at Stanford University. He obtained his PhD in 2018 from Tel Aviv University. His research interests include various aspects of automated reasoning, including formal verification, machine-checkable proofs, and satisfiability modulo theories.