Index

Symbols

(scene)=

A

axiom

B

beta version

C

call trace CFG

control flow graph control flow path counterexample

E

environment Ethereum Virtual Machine EVM EVM bytecode

EVM memory EVM storage exact example

H

havoc

hyperproperty

I

induction install beta version vyper

invariant, [1], [2] and induction preserved block, [1]

L

linear arithmetic

M

model

N

nonlinear arithmetic

O

optimistic assumptions

overapproximation

P

parametric rule, [1]

pessimistic assertions preserved block, [1]

Q

quantified expression

quantifier

R

receiveOrFallback requireInvariant, [1]

rule parametric

S

sanity SAT SAT result scene SMT SMT solver solc solc executables solc-select

sound split split leaf split leaves summarize summary

T

TAC

tautology

U

underapproximation UNSAT

UNSAT result unsound

V

vacuity vacuous

verification condition VS code extension

W

wildcard

witness example