Paper Info
Title
SMT Solving for Arithmetic Theories: Theory and Tool Support
Abstract
Satisfiability checking aims to develop algorithms and tools for checking the satisfiability of logical formulas. Driven by the impressive success of SAT solvers for propositional logic, Satisfiability-Modulo-Theories (SMT) solvers were developed to extend the scope also to different theories. Today, SMT solving is widely used in many applications, for example verification, synthesis, planning or product design automation. In this tutorial paper we give a short introduction to the foundations of SMT solving, describe some popular SMT solvers and illustrate their usage. We also present our own solver SMT-RAT, which was developed to support the strategic combination of different decision procedures, putting a focus on arithmetic theories.
Year
DOI
Venue
2017
10.1109/SYNASC.2017.00009
2017 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC)
Keywords
Field
DocType
Logic,Algorithms,Algebra,Arithmetic,Computer aided analysis
Computer science,Satisfiability,Arithmetic,Theoretical computer science,Automation,Solver,Product design,Semantics,Encoding (memory)
Conference
ISSN
ISBN
Citations 
2470-8801
978-1-5386-2627-6
0
PageRank 
References 
Authors
0.34
0
2
Name
Order
Citations
PageRank
Erika Ábrahám183063.17
Gereon Kremer231.76