“Satisfiability Modulo Theories: A Beginner's Tutorial” by Clark Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, and Yoni Zohar. In Proceedings of the 26^th International Symposium on Formal Methods (FM '24), Part II, (André Platzer, Kristin Yvonne Rozier, Matteo Pradella, and Matteo Rossi, eds.), Sep. 2024, pp. 571-596. Milan, Italy.
Great minds have long dreamed of creating machines that can function as general-purpose problem solvers. Satisfiability modulo theories (SMT) has emerged as one pragmatic realization of this dream, providing significant expressive power and automation. This tutorial is a beginner's guide to SMT. It includes an overview of SMT and its formal foundations, a catalog of the main theories used in SMT solvers, and illustrations of how to obtain models and proofs. Throughout the tutorial, examples and exercises are provided as hands-on activities for the reader. They can be run using either Python or the SMT-LIB language, using either the cvc5 or the Z3 SMT solver.
BibTeX entry:
@inproceedings{BTB+24,
author = {Clark Barrett and Cesare Tinelli and Haniel Barbosa and Aina
Niemetz and Mathias Preiner and Andrew Reynolds and Yoni Zohar},
editor = {Andr{\'e} Platzer and Kristin Yvonne Rozier and Matteo
Pradella and Matteo Rossi},
title = {Satisfiability Modulo Theories: A Beginner's Tutorial},
booktitle = {Proceedings of the {\it 26^{th}} International Symposium
on Formal Methods (FM '24), Part II},
series = {Lecture Notes in Computer Science},
volume = {14934},
pages = {571--596},
publisher = {Springer Nature Switzerland},
month = sep,
year = {2024},
doi = {10.1007/978-3-031-71177-0_31},
note = {Milan, Italy},
url = {https://link.springer.com/chapter/10.1007/978-3-031-71177-0_31}
}
(This webpage was created with bibtex2web.)