-
VeriFast
- Referenced in 57 articles
[sw07705]
- primitive recursive functions. An SMT solver is used to solve queries over data values ... described that prevents non-termination of the SMT solver while enabling reduction of any ground...
-
SMT-RAT
- Referenced in 18 articles
[sw13091]
- toolbox for strategic and parallel SMT solving consisting of a collection of SMT compliant implementations ... methods for solving quantifier-free (non)linear real and integer arithmetic ... modules can be combined to (1) an SMT solver or (2) a theory solver...
-
F*
- Referenced in 20 articles
[sw27563]
- their specifications using a combination of SMT solving and interactive proofs...
-
Beaver
- Referenced in 9 articles
[sw00071]
- vector arithmetic. Beaver is an SMT solver (theorem prover) for the theory of quantifier-free ... operators. Beaver is specially adapted for solving SMT formulae arising out of program analysis (rich...
-
Mcmt
- Referenced in 21 articles
[sw11911]
- safety and fix-points by solving Satisfiability Modulo Theories (SMT) problems. Besides standard SMT techniques...
-
CalCS
- Referenced in 7 articles
[sw13098]
- CalCS: SMT solving for non-linear convex constraints. Certain formal verification tasks require reasoning about ... present a new technique for satisfiability solving of Boolean combinations of non-linear constraints that ... programming to realize a satisfiability modulo theory (SMT) solver. Our solver, CalCS, uses a lazy...
-
PAGAI
- Referenced in 7 articles
[sw13095]
- combining abstract interpretation and decision procedures (SMT-solving), focusing on distinction of paths inside...
-
TACO
- Referenced in 6 articles
[sw07668]
- solving, model checking or SMT-solving...
-
vZ
- Referenced in 10 articles
[sw22666]
- users to pose and solve optimization problems modulo theories. Many SMT applications use models ... portfolio of approaches for solving linear optimization problems over SMT formulas, MaxSMT, and their combinations...
-
VeriMAP
- Referenced in 6 articles
[sw22866]
- fields of constraint logic programming and SMT solving...
-
NLambda
- Referenced in 5 articles
[sw23172]
- about the language in an article: ’SMT Solving for Functional Programming over Infinite Structures...
-
Psyche
- Referenced in 5 articles
[sw28518]
- illustrate Psyche by using it for SMT-solving...
-
raSAT
- Referenced in 8 articles
[sw15206]
- Real numbers. raSAT is an SMT to solve problems in QF_NRA category, i.e., bounded ... raSAT is based on an interval constraint solving, similar to HySAT. raSAT prepares various interval ... linux. raSAT accepts inequality problems in SMT-LIB format (.smt2) (including...
-
ac2lus
- Referenced in 2 articles
[sw17953]
- ac2lus: Bringing SMT-solving and Abstract Interpretation Techniques to Real-Time Calculus through the Synchronous ... allowing the use of techniques like SMT-solving and abstract interpretation which were not previously...
-
TSAT++
- Referenced in 3 articles
[sw21350]
- based approach to satisfiability modulo theories (SMT). SMT is the problem of determining satisfiability ... satisfiability checker cooperate in order to solve SMT. Modularity allows both different enumerators, and satisfiability...
-
dReach
- Referenced in 13 articles
[sw20164]
- numbers, which are solved by delta-decision procedures in the SMT solver dReach. In this...
-
InvA
- Referenced in 2 articles
[sw10124]
- narrowing, equationally-defined equality predicates, and SMT solving, InvA achieves a significant degree of automation...
-
JavaSMT
- Referenced in 1 article
[sw18525]
- newly developed tools rely on SMT solving. The SMT-LIB initiative defines a common format ... solver-independent API layer for SMT solving. Our library aims to close the gap between...
-
Clingcon
- Referenced in 34 articles
[sw09892]
- Answer Set Programming (ASP) with constraint solving. Constraints over non-linear finite integers ... adopts state-of-the-art techniques from SMT and uses conflict-driven learning and theory...
-
smt
- Referenced in 14 articles
[sw09205]
- arithmetic operators and functions on them. The smt toolbox for Matlab introduces two new classes ... toolbox new routines for solving Toeplitz linear systems. (netlib numeralgo na30...