TALK KEYWORD INDEX
This page contains an index consisting of author-provided keywords.
A | |
abstract interpretation | |
Approximation | |
automated reasonning | |
B | |
bit-blasting | |
Blockchain | |
C | |
Constrained Horn Clauses | |
D | |
Deductive programs verification | |
E | |
Egraph | |
Ethereum | |
F | |
first-order logic | |
Fixed Point Arithmetic | |
Floating Point Arithmetic | |
floating-point | |
formal verification | |
H | |
herbrand theorem | |
higher-order logic | |
I | |
ic3 | |
IEEE-754 | |
Inductive invariants | |
instantiation | |
Interpolation | |
K | |
Knapsack | |
L | |
Lemma learning | |
Linearization | |
M | |
MC-SAT | |
model checking | |
O | |
OMT | |
P | |
PDR | |
polymorphism | |
Program Verification | |
Proof generation | |
property directed reachability | |
Q | |
quantifier instantiation | |
quantifiers | |
R | |
Real Arithetmic | |
Rewrite Rules | |
rewriting | |
S | |
safety properties | |
SAT | |
Satisfiability modulo assignment | |
Satisfiability Modulo Theories | |
Satisfiablity Modulo Theories | |
Smart contracts | |
SMT | |
SMT-solving | |
superposition | |
Syntax-guided Synthesis | |
T | |
Tableaux | |
theorem proving | |
Theory combination | |
theory of bit-vectors | |
W | |
WSN |