SMT 2012: Keyword Index

KeywordPapers
a
arithmeticAnatomy of Alternating Quantifier Satisfiability (Work in progress)
axiomatic theoryBuilt-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers
b
bit-precise reasoningOn the Complexity of Fixed-Size Bit-Vector Logics with Binary Encoded Bit-Width
bit-vector logicsOn the Complexity of Fixed-Size Bit-Vector Logics with Binary Encoded Bit-Width
bitvectorsA Theory of Arrays with set and copy Operations
c
complexityOn the Complexity of Fixed-Size Bit-Vector Logics with Binary Encoded Bit-Width
ConfigurationAn SMT-based approach to automated configuration
copyA Theory of Arrays with set and copy Operations
d
decision procedureOn the Complexity of Fixed-Size Bit-Vector Logics with Binary Encoded Bit-Width
Anatomy of Alternating Quantifier Satisfiability (Work in progress)
e
exotic semi-ringsExotic Semi-Ring Constraints
f
floating-pointBuilt-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers
h
High-level modelingSMT-Based System Verification with DVF
i
InstantiationReasoning with Triggers
integersA Theory of Arrays with set and copy Operations
m
machine learningA Machine Learning Technique for Hardness Estimation of QFBV SMT Problems
MappingAn SMT-based approach to automated configuration
memcpyA Theory of Arrays with set and copy Operations
memmoveA Theory of Arrays with set and copy Operations
memsetA Theory of Arrays with set and copy Operations
model checkingReachability Modulo Theory Library
n
NEXPTIMEOn the Complexity of Fixed-Size Bit-Vector Logics with Binary Encoded Bit-Width
o
order encodingExotic Semi-Ring Constraints
p
Presburger arithmeticAnatomy of Alternating Quantifier Satisfiability (Work in progress)
product linesAn SMT-based approach to automated configuration
program verificationProgram Verification as Satisfiability Modulo Theories
q
quantifier eliminationAnatomy of Alternating Quantifier Satisfiability (Work in progress)
quantifiersReasoning with Triggers
r
Reachability Modulo TheoriesReachability Modulo Theory Library
real arithmeticBuilt-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers
regular expressionsSMT-LIB Sequences and Regular Expressions
s
SAT encodingsExotic Semi-Ring Constraints
satisfiabilityAn SMT-based approach to automated configuration
satisfiability module theoriesThe 2012 SMT Competition
SETA Theory of Arrays with set and copy Operations
simplexBuilt-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers
SMTProgram Verification as Satisfiability Modulo Theories
Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers
Reasoning with Triggers
SMT-Based System Verification with DVF
On the Complexity of Fixed-Size Bit-Vector Logics with Binary Encoded Bit-Width
A Machine Learning Technique for Hardness Estimation of QFBV SMT Problems
SMT-LIB Sequences and Regular Expressions
A Theory of Arrays with set and copy Operations
An SMT-based approach to automated configuration
Anatomy of Alternating Quantifier Satisfiability (Work in progress)
The 2012 SMT Competition
SMT CompetitionThe 2012 SMT Competition
SMT solverThe 2012 SMT Competition
SMT-COMPThe 2012 SMT Competition
SMT-evaluationThe 2012 SMT Competition
SMT-IDLExotic Semi-Ring Constraints
SMT-LIAExotic Semi-Ring Constraints
SMT-LIBReachability Modulo Theory Library
SMT-LIB Sequences and Regular Expressions
Statistical Hardness modelsA Machine Learning Technique for Hardness Estimation of QFBV SMT Problems
STPAn SMT-based approach to automated configuration
stringsSMT-LIB Sequences and Regular Expressions
symbolic model checkingProgram Verification as Satisfiability Modulo Theories
system description languagesSMT-Based System Verification with DVF
t
theoriesReasoning with Triggers
SMT-LIB Sequences and Regular Expressions
Theory of ArraysA Theory of Arrays with set and copy Operations
transition systemsSMT-Based System Verification with DVF
triggersReasoning with Triggers
TVLAn SMT-based approach to automated configuration
v
variabilityAn SMT-based approach to automated configuration
verificationSMT-Based System Verification with DVF