Satisﬁability Modulo Theories

By Silvio Ranise, Cesare Tinelli. 2006

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Citations in the corpus

Syntax-guided synthesis (2013, positive): “An SMT solver determines the truth of a given logical formula built from typed variables, logical connectives, and typical operations such as arithmetic and array accesses (see [1], [2]).”
The MathSAT5 SMT Solver (2013, unknown): “…if-then-else constructs ITE ( c, t, e ) from a formula by replacing them with fresh variables x ITE and by adding to the formula the clauses ( ¬ c The core of M ATH SAT5 is composed of the SAT engine and the theory solvers, which interact following the standard lazy/DPLL( T ) approach [2].”
The nuXmv Symbolic Model Checker (2014, unknown): “To analyze such kind of designs, we integrated in NU X MV several new veriﬁcation algorithms based on Satisﬁability Modulo Theory (SMT) [18] and on abstraction, or combination of abstraction with other techniques.”
Achieving Verified Robustness to Symbol Substitutions via Interval Bound Propagation (2019, unknown): “Rather than continuing the race with adversaries, formal veriﬁcation (Baier and Katoen, 2008; Barrett and Tinelli, 2018; Katz et al., 2017) offers a different approach: it aims at providing provable guarantees to a given model speciﬁcation.”
Moat: Verifying Confidentiality of Enclave Programs (2015, unknown): “Operations on arrays consist of reads x := X [ y ] and writes X [ y ] := x , which are interpreted by the Theory of Arrays [8].”
Towards Verified Artificial Intelligence (2016, unknown): “At the heart of these advances are computational proof engines such as Boolean satisﬁability (SAT) solvers [34], Boolean reasoning and manipulation routines based on Binary Decision Diagrams (BDDs) [8], and satisﬁability modulo theories (SMT) solvers [5].”