| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (986 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (17 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (649 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (11 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (67 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (81 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (16 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (122 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
Global Index
A
a [definition, in WiSE.implem.bugfinder]Add [constructor, in WiSE.lang.imprec]
Add [constructor, in WiSE.lang.imp]
aeq [definition, in WiSE.lang.imp]
aeq_spec [lemma, in WiSE.lang.imp]
aeval [definition, in WiSE.lang.imprec]
aeval [definition, in WiSE.lang.imp]
aeval_comp [lemma, in WiSE.symbolic.symex]
aeval_stable [lemma, in WiSE.lang.imp]
aeval_inst [lemma, in WiSE.lang.imp]
aeval_asubst [lemma, in WiSE.lang.imp]
aexpr [inductive, in WiSE.lang.imprec]
aexpr [inductive, in WiSE.lang.imp]
Aff [constructor, in WiSE.lang.imprec]
Aff [constructor, in WiSE.lang.imp]
ainst [definition, in WiSE.lang.imp]
all_some [definition, in WiSE.utils]
alocals [definition, in WiSE.lang.imprec]
asimp [definition, in WiSE.symbolic.solver]
asimp_correct [lemma, in WiSE.symbolic.solver]
Assert [definition, in WiSE.lang.imprec]
Assert [definition, in WiSE.lang.imp]
asubst [definition, in WiSE.lang.imp]
a0 [definition, in WiSE.implem.bugfinder]
a1:1 [binder, in WiSE.symbolic.solver]
a1:13 [binder, in WiSE.symbolic.solver]
a1:16 [binder, in WiSE.symbolic.solver]
a1:24 [binder, in WiSE.relations]
a1:3 [binder, in WiSE.lang.imp]
a1:5 [binder, in WiSE.symbolic.solver]
a2:14 [binder, in WiSE.symbolic.solver]
a2:17 [binder, in WiSE.symbolic.solver]
a2:2 [binder, in WiSE.symbolic.solver]
a2:25 [binder, in WiSE.relations]
a2:4 [binder, in WiSE.lang.imp]
a2:6 [binder, in WiSE.symbolic.solver]
A:1 [binder, in WiSE.streams]
A:1 [binder, in WiSE.equalities]
A:1 [binder, in WiSE.utils]
A:1 [binder, in WiSE.implem.bugfinder_proof]
a:10 [binder, in WiSE.equalities]
A:103 [binder, in WiSE.streams]
A:106 [binder, in WiSE.streams]
A:109 [binder, in WiSE.streams]
A:11 [binder, in WiSE.streams]
A:113 [binder, in WiSE.streams]
A:117 [binder, in WiSE.streams]
A:12 [binder, in WiSE.equalities]
A:123 [binder, in WiSE.streams]
A:124 [binder, in WiSE.streams]
A:128 [binder, in WiSE.streams]
A:132 [binder, in WiSE.streams]
A:133 [binder, in WiSE.streams]
A:134 [binder, in WiSE.streams]
A:138 [binder, in WiSE.streams]
A:14 [binder, in WiSE.utils]
A:142 [binder, in WiSE.streams]
A:17 [binder, in WiSE.streams]
a:19 [binder, in WiSE.symbolic.solver]
A:19 [binder, in WiSE.utils]
A:19 [binder, in WiSE.relations]
a:19 [binder, in WiSE.lang.imp]
A:23 [binder, in WiSE.streams]
A:27 [binder, in WiSE.streams]
A:28 [binder, in WiSE.relations]
A:31 [binder, in WiSE.streams]
A:37 [binder, in WiSE.streams]
A:4 [binder, in WiSE.equalities]
A:43 [binder, in WiSE.streams]
A:48 [binder, in WiSE.streams]
A:53 [binder, in WiSE.streams]
A:58 [binder, in WiSE.streams]
A:6 [binder, in WiSE.streams]
a:6 [binder, in WiSE.implem.bugfinder_proof]
A:62 [binder, in WiSE.streams]
A:66 [binder, in WiSE.streams]
A:67 [binder, in WiSE.streams]
A:7 [binder, in WiSE.utils]
A:70 [binder, in WiSE.streams]
A:74 [binder, in WiSE.streams]
A:78 [binder, in WiSE.streams]
a:8 [binder, in WiSE.lang.imp]
A:82 [binder, in WiSE.streams]
A:86 [binder, in WiSE.streams]
a:9 [binder, in WiSE.symbolic.solver]
A:9 [binder, in WiSE.streams]
A:90 [binder, in WiSE.streams]
A:93 [binder, in WiSE.streams]
A:97 [binder, in WiSE.streams]
B
b [definition, in WiSE.implem.bugfinder]BadInput [definition, in WiSE.symbolic.symex]
BadInput [definition, in WiSE.lang.imp]
BadInput_correct [lemma, in WiSE.symbolic.symex]
Band [constructor, in WiSE.lang.imprec]
Band [constructor, in WiSE.lang.imp]
Bcst [constructor, in WiSE.lang.imprec]
Bcst [constructor, in WiSE.lang.imp]
Beq [constructor, in WiSE.lang.imprec]
beq [definition, in WiSE.lang.imp]
Beq [constructor, in WiSE.lang.imp]
beq_spec [lemma, in WiSE.lang.imp]
beval [definition, in WiSE.lang.imp]
beval_comp [lemma, in WiSE.symbolic.symex]
beval_inst [lemma, in WiSE.lang.imp]
beval_bsubst [lemma, in WiSE.lang.imp]
bexpr [inductive, in WiSE.lang.imprec]
bexpr [inductive, in WiSE.lang.imp]
bijection [definition, in WiSE.equalities]
binst [definition, in WiSE.lang.imp]
Ble [constructor, in WiSE.lang.imprec]
Ble [constructor, in WiSE.lang.imp]
blocals [definition, in WiSE.lang.imprec]
Bnot [constructor, in WiSE.lang.imprec]
Bnot [constructor, in WiSE.lang.imp]
body [projection, in WiSE.lang.imprec]
Bor [definition, in WiSE.lang.imprec]
Bor [definition, in WiSE.lang.imp]
bsimp [definition, in WiSE.symbolic.solver]
bsimp_correct [lemma, in WiSE.symbolic.solver]
bsubst [definition, in WiSE.lang.imp]
bug [definition, in WiSE.lang.imp]
bugfinder [library]
bugfinder_proof [library]
BugFound [constructor, in WiSE.implem.bugfinder]
bug_found [definition, in WiSE.implem.bugfinder_proof]
b0 [definition, in WiSE.implem.bugfinder]
b1:12 [binder, in WiSE.lang.imp]
b1:14 [binder, in WiSE.lang.imp]
b1:20 [binder, in WiSE.symbolic.solver]
b1:26 [binder, in WiSE.relations]
b1:30 [binder, in WiSE.symbolic.solver]
b1:9 [binder, in WiSE.lang.imprec]
b2:10 [binder, in WiSE.lang.imprec]
b2:13 [binder, in WiSE.lang.imp]
b2:15 [binder, in WiSE.lang.imp]
b2:21 [binder, in WiSE.symbolic.solver]
b2:27 [binder, in WiSE.relations]
b2:31 [binder, in WiSE.symbolic.solver]
b:11 [binder, in WiSE.equalities]
B:13 [binder, in WiSE.equalities]
b:153 [binder, in WiSE.lang.imp]
b:163 [binder, in WiSE.lang.imp]
b:18 [binder, in WiSE.lang.imprec]
B:2 [binder, in WiSE.implem.bugfinder_proof]
B:20 [binder, in WiSE.relations]
b:20 [binder, in WiSE.lang.imp]
b:24 [binder, in WiSE.symbolic.solver]
b:26 [binder, in WiSE.symbolic.solver]
B:29 [binder, in WiSE.relations]
b:33 [binder, in WiSE.symbolic.solver]
b:35 [binder, in WiSE.symbolic.solver]
b:38 [binder, in WiSE.symbolic.solver]
B:38 [binder, in WiSE.streams]
b:39 [binder, in WiSE.symbolic.solver]
b:42 [binder, in WiSE.symbolic.solver]
B:44 [binder, in WiSE.streams]
B:5 [binder, in WiSE.equalities]
b:5 [binder, in WiSE.implem.bugfinder_proof]
B:59 [binder, in WiSE.streams]
B:8 [binder, in WiSE.utils]
b:9 [binder, in WiSE.lang.imp]
B:98 [binder, in WiSE.streams]
C
comp [definition, in WiSE.symbolic.symex]complete_bug_finding [definition, in WiSE.symbolic.symex]
comp_update [lemma, in WiSE.symbolic.symex]
comp_id [lemma, in WiSE.symbolic.symex]
Concrete [definition, in WiSE.symbolic.symex]
cond:29 [binder, in WiSE.implem.bugfinder]
cond:31 [binder, in WiSE.implem.bugfinder]
Cst [constructor, in WiSE.lang.imprec]
Cst [constructor, in WiSE.lang.imp]
c1:106 [binder, in WiSE.lang.imp]
c1:113 [binder, in WiSE.lang.imp]
c1:117 [binder, in WiSE.lang.imp]
c1:131 [binder, in WiSE.lang.imp]
c1:137 [binder, in WiSE.lang.imp]
c1:39 [binder, in WiSE.symbolic.symex]
c1:47 [binder, in WiSE.symbolic.symex]
c1:52 [binder, in WiSE.symbolic.symex]
c1:67 [binder, in WiSE.symbolic.symex]
c1:72 [binder, in WiSE.symbolic.symex]
c1:78 [binder, in WiSE.lang.imp]
c1:81 [binder, in WiSE.symbolic.symex]
c1:83 [binder, in WiSE.lang.imp]
c1:88 [binder, in WiSE.lang.imp]
c1:92 [binder, in WiSE.symbolic.symex]
c1:99 [binder, in WiSE.symbolic.symex]
c2:100 [binder, in WiSE.symbolic.symex]
c2:107 [binder, in WiSE.lang.imp]
c2:114 [binder, in WiSE.lang.imp]
c2:118 [binder, in WiSE.lang.imp]
c2:132 [binder, in WiSE.lang.imp]
c2:138 [binder, in WiSE.lang.imp]
c2:40 [binder, in WiSE.symbolic.symex]
c2:48 [binder, in WiSE.symbolic.symex]
c2:53 [binder, in WiSE.symbolic.symex]
c2:68 [binder, in WiSE.symbolic.symex]
c2:75 [binder, in WiSE.symbolic.symex]
c2:79 [binder, in WiSE.lang.imp]
c2:84 [binder, in WiSE.symbolic.symex]
c2:84 [binder, in WiSE.lang.imp]
c2:89 [binder, in WiSE.lang.imp]
c2:93 [binder, in WiSE.symbolic.symex]
c3:108 [binder, in WiSE.lang.imp]
c3:133 [binder, in WiSE.lang.imp]
c3:41 [binder, in WiSE.symbolic.symex]
c:110 [binder, in WiSE.lang.imp]
c:121 [binder, in WiSE.lang.imp]
c:124 [binder, in WiSE.lang.imp]
c:13 [binder, in WiSE.lang.imprec]
c:23 [binder, in WiSE.lang.imp]
c:43 [binder, in WiSE.symbolic.symex]
c:57 [binder, in WiSE.symbolic.symex]
c:57 [binder, in WiSE.lang.imp]
c:61 [binder, in WiSE.symbolic.symex]
c:65 [binder, in WiSE.lang.imp]
c:94 [binder, in WiSE.lang.imp]
c:97 [binder, in WiSE.lang.imp]
D
declaration [record, in WiSE.lang.imprec]decls [projection, in WiSE.lang.imprec]
display [definition, in WiSE.implem.bugfinder]
done [definition, in WiSE.implem.bugfinder_proof]
E
enum [definition, in WiSE.streams]enum_equ [definition, in WiSE.streams]
env0:106 [binder, in WiSE.symbolic.symex]
env0:114 [binder, in WiSE.symbolic.symex]
env0:117 [binder, in WiSE.symbolic.symex]
env0:129 [binder, in WiSE.symbolic.symex]
env0:130 [binder, in WiSE.symbolic.symex]
env1:125 [binder, in WiSE.lang.imp]
env1:132 [binder, in WiSE.symbolic.symex]
env2:126 [binder, in WiSE.lang.imp]
env:10 [binder, in WiSE.implem.bugfinder]
env:102 [binder, in WiSE.symbolic.symex]
env:108 [binder, in WiSE.symbolic.symex]
env:115 [binder, in WiSE.symbolic.symex]
env:118 [binder, in WiSE.symbolic.symex]
env:12 [binder, in WiSE.symbolic.solver]
env:12 [binder, in WiSE.implem.bugfinder_proof]
env:15 [binder, in WiSE.symbolic.solver]
env:151 [binder, in WiSE.lang.imp]
env:152 [binder, in WiSE.lang.imp]
env:156 [binder, in WiSE.lang.imp]
env:159 [binder, in WiSE.lang.imp]
env:16 [binder, in WiSE.implem.bugfinder_proof]
env:162 [binder, in WiSE.lang.imp]
env:18 [binder, in WiSE.symbolic.symex]
env:18 [binder, in WiSE.symbolic.solver]
env:21 [binder, in WiSE.symbolic.symex]
env:23 [binder, in WiSE.implem.bugfinder_proof]
env:24 [binder, in WiSE.symbolic.symex]
env:29 [binder, in WiSE.symbolic.solver]
env:32 [binder, in WiSE.symbolic.solver]
env:34 [binder, in WiSE.symbolic.solver]
env:35 [binder, in WiSE.implem.bugfinder_proof]
env:40 [binder, in WiSE.symbolic.solver]
env:41 [binder, in WiSE.symbolic.solver]
env:6 [binder, in WiSE.symbolic.symex]
env:6 [binder, in WiSE.implem.bugfinder]
env:62 [binder, in WiSE.symbolic.symex]
env:69 [binder, in WiSE.symbolic.symex]
env:76 [binder, in WiSE.symbolic.symex]
env:8 [binder, in WiSE.implem.bugfinder_proof]
env:85 [binder, in WiSE.symbolic.symex]
env:9 [binder, in WiSE.symbolic.symex]
env:94 [binder, in WiSE.symbolic.symex]
Eq [record, in WiSE.equalities]
EQ [constructor, in WiSE.equalities]
equalities [library]
eq_op [projection, in WiSE.equalities]
Err [constructor, in WiSE.lang.imprec]
Err [constructor, in WiSE.lang.imp]
error [inductive, in WiSE.lang.imp]
error_state_error [lemma, in WiSE.lang.imp]
error_Seq [constructor, in WiSE.lang.imp]
error_Err [constructor, in WiSE.lang.imp]
error_state_seq [lemma, in WiSE.lang.imp]
error_state [definition, in WiSE.lang.imp]
eventually [definition, in WiSE.streams]
Examples [section, in WiSE.implem.bugfinder]
Examples.Gcd [section, in WiSE.implem.bugfinder]
Bug _ [notation, in WiSE.implem.bugfinder]
Examples.Simple [section, in WiSE.implem.bugfinder]
exec [inductive, in WiSE.lang.imp]
execute_gcd_err [definition, in WiSE.implem.bugfinder]
execute_gcd_noerr [definition, in WiSE.implem.bugfinder]
execute_gcd [definition, in WiSE.implem.bugfinder]
exec_steps [lemma, in WiSE.lang.imp]
exec_loop_false [constructor, in WiSE.lang.imp]
exec_loop_true [constructor, in WiSE.lang.imp]
exec_Ite_false [constructor, in WiSE.lang.imp]
exec_Ite_true [constructor, in WiSE.lang.imp]
exec_Seq [constructor, in WiSE.lang.imp]
exec_Aff [constructor, in WiSE.lang.imp]
exec_Skip [constructor, in WiSE.lang.imp]
expand [definition, in WiSE.implem.bugfinder]
expand_inv [lemma, in WiSE.implem.bugfinder_proof]
expand_complete [lemma, in WiSE.implem.bugfinder_proof]
expand_sound [lemma, in WiSE.implem.bugfinder_proof]
extract [library]
e':30 [binder, in WiSE.lang.imp]
e':42 [binder, in WiSE.lang.imp]
e':55 [binder, in WiSE.lang.imp]
e:102 [binder, in WiSE.lang.imp]
e:11 [binder, in WiSE.symbolic.symex]
e:112 [binder, in WiSE.lang.imp]
e:116 [binder, in WiSE.lang.imp]
e:120 [binder, in WiSE.lang.imp]
e:123 [binder, in WiSE.lang.imp]
e:127 [binder, in WiSE.lang.imp]
e:14 [binder, in WiSE.lang.imprec]
e:15 [binder, in WiSE.symbolic.symex]
e:158 [binder, in WiSE.lang.imp]
e:20 [binder, in WiSE.symbolic.symex]
e:23 [binder, in WiSE.symbolic.symex]
e:25 [binder, in WiSE.lang.imp]
e:26 [binder, in WiSE.symbolic.symex]
e:28 [binder, in WiSE.lang.imp]
e:33 [binder, in WiSE.symbolic.symex]
e:33 [binder, in WiSE.lang.imp]
e:36 [binder, in WiSE.lang.imprec]
e:37 [binder, in WiSE.lang.imp]
e:4 [binder, in WiSE.symbolic.symex]
e:40 [binder, in WiSE.lang.imp]
e:45 [binder, in WiSE.lang.imp]
e:46 [binder, in WiSE.symbolic.symex]
e:51 [binder, in WiSE.symbolic.symex]
e:53 [binder, in WiSE.lang.imp]
e:56 [binder, in WiSE.symbolic.symex]
e:59 [binder, in WiSE.lang.imp]
e:60 [binder, in WiSE.symbolic.symex]
e:61 [binder, in WiSE.lang.imp]
e:73 [binder, in WiSE.lang.imp]
e:82 [binder, in WiSE.lang.imp]
e:87 [binder, in WiSE.lang.imp]
e:93 [binder, in WiSE.lang.imp]
e:96 [binder, in WiSE.lang.imp]
F
filter [definition, in WiSE.streams]find_bugs_complete [lemma, in WiSE.implem.bugfinder_proof]
find_bugs_sound [lemma, in WiSE.implem.bugfinder_proof]
find_bugs_assuming [definition, in WiSE.implem.bugfinder]
find_bugs [definition, in WiSE.implem.bugfinder]
Finished [constructor, in WiSE.implem.bugfinder]
first [definition, in WiSE.utils]
force [definition, in WiSE.streams]
force_id [lemma, in WiSE.streams]
func_to_stream_correct [lemma, in WiSE.streams]
func_to_stream [definition, in WiSE.streams]
fun_Eq [instance, in WiSE.streams]
f1:129 [binder, in WiSE.streams]
f2:130 [binder, in WiSE.streams]
f:105 [binder, in WiSE.streams]
f:136 [binder, in WiSE.streams]
f:140 [binder, in WiSE.streams]
f:16 [binder, in WiSE.equalities]
f:2 [binder, in WiSE.utils]
f:3 [binder, in WiSE.implem.bugfinder_proof]
f:39 [binder, in WiSE.streams]
f:45 [binder, in WiSE.streams]
f:49 [binder, in WiSE.streams]
f:54 [binder, in WiSE.streams]
f:60 [binder, in WiSE.streams]
f:8 [binder, in WiSE.equalities]
f:9 [binder, in WiSE.utils]
f:99 [binder, in WiSE.streams]
G
gcd [definition, in WiSE.implem.bugfinder]gcd_buggy [definition, in WiSE.implem.bugfinder]
gcd_assertions [definition, in WiSE.implem.bugfinder]
get [definition, in WiSE.streams]
get_map [lemma, in WiSE.streams]
get_filter [lemma, in WiSE.streams]
get_shift [lemma, in WiSE.streams]
Global [constructor, in WiSE.lang.imprec]
globally [definition, in WiSE.streams]
global_store [definition, in WiSE.lang.imprec]
gs:34 [binder, in WiSE.lang.imprec]
g:17 [binder, in WiSE.equalities]
g:9 [binder, in WiSE.equalities]
H
HasBug [definition, in WiSE.symbolic.symex]HasBug [definition, in WiSE.lang.imp]
HasBug_correct [lemma, in WiSE.symbolic.symex]
here [definition, in WiSE.implem.bugfinder_proof]
Hlocals [projection, in WiSE.lang.imprec]
H0:15 [binder, in WiSE.equalities]
H0:7 [binder, in WiSE.equalities]
H:14 [binder, in WiSE.equalities]
H:6 [binder, in WiSE.equalities]
I
id [definition, in WiSE.symbolic.symex]ident [definition, in WiSE.lang.imprec]
ident [definition, in WiSE.lang.imp]
IMP [inductive, in WiSE.lang.imp]
imp [library]
IMPREC [record, in WiSE.lang.imprec]
imprec [library]
init [definition, in WiSE.implem.bugfinder]
init_store' [definition, in WiSE.implem.bugfinder]
init_store [definition, in WiSE.implem.bugfinder]
init_assuming [definition, in WiSE.implem.bugfinder]
IsBug [definition, in WiSE.symbolic.symex]
IsBug [definition, in WiSE.lang.imp]
IsBug_correct [lemma, in WiSE.symbolic.symex]
isomorph [definition, in WiSE.equalities]
is_sat [definition, in WiSE.symbolic.solver]
is_error_Stuck [lemma, in WiSE.lang.imp]
is_skip [definition, in WiSE.lang.imp]
is_error_correct [lemma, in WiSE.lang.imp]
is_error [definition, in WiSE.lang.imp]
Ite [constructor, in WiSE.lang.imprec]
Ite [constructor, in WiSE.lang.imp]
L
Local [constructor, in WiSE.lang.imprec]locals [definition, in WiSE.lang.imprec]
local_store [definition, in WiSE.lang.imprec]
Loop [constructor, in WiSE.lang.imprec]
Loop [constructor, in WiSE.lang.imp]
ls:35 [binder, in WiSE.lang.imprec]
LTL [module, in WiSE.streams]
LTL.and [definition, in WiSE.streams]
LTL.eventually [definition, in WiSE.streams]
LTL.globally [definition, in WiSE.streams]
LTL.globally_map [lemma, in WiSE.streams]
LTL.imp [definition, in WiSE.streams]
LTL.model [definition, in WiSE.streams]
LTL.next [definition, in WiSE.streams]
LTL.not [definition, in WiSE.streams]
LTL.now [definition, in WiSE.streams]
LTL.or [definition, in WiSE.streams]
LTL.shift_shift [lemma, in WiSE.streams]
LTL.t [definition, in WiSE.streams]
_ ⊨ _ [notation, in WiSE.streams]
_ ∧ _ [notation, in WiSE.streams]
_ ∨ _ [notation, in WiSE.streams]
_ → _ [notation, in WiSE.streams]
!! _ [notation, in WiSE.streams]
! _ [notation, in WiSE.streams]
¬ _ [notation, in WiSE.streams]
□ _ [notation, in WiSE.streams]
◊ _ [notation, in WiSE.streams]
◯ _ [notation, in WiSE.streams]
l1:29 [binder, in WiSE.implem.bugfinder_proof]
l1:32 [binder, in WiSE.implem.bugfinder_proof]
l2:30 [binder, in WiSE.implem.bugfinder_proof]
l2:33 [binder, in WiSE.implem.bugfinder_proof]
l3:31 [binder, in WiSE.implem.bugfinder_proof]
l3:37 [binder, in WiSE.implem.bugfinder_proof]
l:10 [binder, in WiSE.utils]
l:14 [binder, in WiSE.implem.bugfinder]
l:15 [binder, in WiSE.utils]
l:20 [binder, in WiSE.utils]
l:21 [binder, in WiSE.implem.bugfinder_proof]
l:27 [binder, in WiSE.implem.bugfinder_proof]
l:3 [binder, in WiSE.utils]
l:4 [binder, in WiSE.implem.bugfinder_proof]
l:55 [binder, in WiSE.implem.bugfinder_proof]
l:56 [binder, in WiSE.implem.bugfinder_proof]
l:62 [binder, in WiSE.implem.bugfinder_proof]
l:65 [binder, in WiSE.implem.bugfinder_proof]
l:66 [binder, in WiSE.implem.bugfinder_proof]
M
main [projection, in WiSE.lang.imprec]map [definition, in WiSE.streams]
map_eq [lemma, in WiSE.streams]
map_opt [definition, in WiSE.utils]
map_in [lemma, in WiSE.implem.bugfinder_proof]
MAYBE [constructor, in WiSE.symbolic.solver]
mk_not_correct [lemma, in WiSE.symbolic.solver]
mk_and_correct [lemma, in WiSE.symbolic.solver]
mk_not [definition, in WiSE.symbolic.solver]
mk_and [definition, in WiSE.symbolic.solver]
mk_sub_correct [lemma, in WiSE.symbolic.solver]
mk_add_correct [lemma, in WiSE.symbolic.solver]
mk_sub [definition, in WiSE.symbolic.solver]
mk_add [definition, in WiSE.symbolic.solver]
my_prog [definition, in WiSE.implem.bugfinder]
m:122 [binder, in WiSE.streams]
m:141 [binder, in WiSE.streams]
m:26 [binder, in WiSE.streams]
m:63 [binder, in WiSE.streams]
N
next_next:23 [binder, in WiSE.implem.bugfinder]next_next:17 [binder, in WiSE.implem.bugfinder]
none [definition, in WiSE.implem.bugfinder_proof]
now [definition, in WiSE.streams]
n:112 [binder, in WiSE.streams]
n:116 [binder, in WiSE.streams]
n:12 [binder, in WiSE.streams]
n:121 [binder, in WiSE.streams]
n:127 [binder, in WiSE.streams]
n:131 [binder, in WiSE.streams]
n:135 [binder, in WiSE.streams]
n:139 [binder, in WiSE.streams]
n:144 [binder, in WiSE.streams]
n:146 [binder, in WiSE.streams]
n:18 [binder, in WiSE.streams]
n:18 [binder, in WiSE.implem.bugfinder]
n:25 [binder, in WiSE.streams]
n:25 [binder, in WiSE.implem.bugfinder_proof]
n:26 [binder, in WiSE.implem.bugfinder_proof]
n:28 [binder, in WiSE.streams]
n:28 [binder, in WiSE.implem.bugfinder_proof]
n:32 [binder, in WiSE.streams]
n:56 [binder, in WiSE.streams]
n:57 [binder, in WiSE.streams]
n:64 [binder, in WiSE.streams]
n:73 [binder, in WiSE.streams]
n:77 [binder, in WiSE.streams]
P
params [projection, in WiSE.lang.imprec]path:11 [binder, in WiSE.implem.bugfinder_proof]
path:126 [binder, in WiSE.symbolic.symex]
path:15 [binder, in WiSE.implem.bugfinder_proof]
path:22 [binder, in WiSE.implem.bugfinder_proof]
path:34 [binder, in WiSE.implem.bugfinder_proof]
path:7 [binder, in WiSE.implem.bugfinder_proof]
path:7 [binder, in WiSE.implem.bugfinder]
path:9 [binder, in WiSE.implem.bugfinder]
pat:109 [binder, in WiSE.symbolic.symex]
pat:113 [binder, in WiSE.symbolic.symex]
pat:147 [binder, in WiSE.lang.imp]
pat:8 [binder, in WiSE.implem.bugfinder]
peek [definition, in WiSE.streams]
Pending [constructor, in WiSE.implem.bugfinder]
potential_bug [definition, in WiSE.symbolic.symex]
potential_bug [definition, in WiSE.implem.bugfinder_proof]
progress [definition, in WiSE.lang.imp]
progress_Loop [lemma, in WiSE.lang.imp]
progress_Seq [lemma, in WiSE.lang.imp]
progress_Aff [lemma, in WiSE.lang.imp]
progress_Ite [lemma, in WiSE.lang.imp]
progress_Skip [lemma, in WiSE.lang.imp]
prog0:125 [binder, in WiSE.symbolic.symex]
prog0:131 [binder, in WiSE.symbolic.symex]
prog1:133 [binder, in WiSE.symbolic.symex]
prog:11 [binder, in WiSE.implem.bugfinder]
prog:128 [binder, in WiSE.symbolic.symex]
prog:13 [binder, in WiSE.implem.bugfinder_proof]
prog:136 [binder, in WiSE.symbolic.symex]
prog:17 [binder, in WiSE.implem.bugfinder_proof]
prog:24 [binder, in WiSE.implem.bugfinder_proof]
prog:36 [binder, in WiSE.implem.bugfinder_proof]
prog:9 [binder, in WiSE.implem.bugfinder_proof]
p':107 [binder, in WiSE.symbolic.symex]
p':149 [binder, in WiSE.lang.imp]
p1:104 [binder, in WiSE.symbolic.symex]
p1:154 [binder, in WiSE.lang.imp]
p1:160 [binder, in WiSE.lang.imp]
p1:166 [binder, in WiSE.lang.imp]
p1:170 [binder, in WiSE.lang.imp]
p2:105 [binder, in WiSE.symbolic.symex]
p2:155 [binder, in WiSE.lang.imp]
p2:161 [binder, in WiSE.lang.imp]
p2:167 [binder, in WiSE.lang.imp]
p2:171 [binder, in WiSE.lang.imp]
P:100 [binder, in WiSE.streams]
P:108 [binder, in WiSE.streams]
p:110 [binder, in WiSE.symbolic.symex]
P:111 [binder, in WiSE.streams]
P:115 [binder, in WiSE.streams]
p:116 [binder, in WiSE.symbolic.symex]
p:119 [binder, in WiSE.symbolic.symex]
P:119 [binder, in WiSE.streams]
p:134 [binder, in WiSE.lang.imp]
p:137 [binder, in WiSE.symbolic.symex]
p:138 [binder, in WiSE.symbolic.symex]
p:142 [binder, in WiSE.lang.imp]
p:143 [binder, in WiSE.symbolic.symex]
p:145 [binder, in WiSE.symbolic.symex]
p:145 [binder, in WiSE.lang.imp]
p:147 [binder, in WiSE.symbolic.symex]
p:151 [binder, in WiSE.symbolic.symex]
p:153 [binder, in WiSE.symbolic.symex]
p:155 [binder, in WiSE.symbolic.symex]
p:156 [binder, in WiSE.symbolic.symex]
p:158 [binder, in WiSE.symbolic.symex]
p:164 [binder, in WiSE.lang.imp]
p:173 [binder, in WiSE.lang.imp]
p:174 [binder, in WiSE.lang.imp]
p:177 [binder, in WiSE.lang.imp]
p:178 [binder, in WiSE.lang.imp]
p:184 [binder, in WiSE.lang.imp]
p:185 [binder, in WiSE.lang.imp]
p:189 [binder, in WiSE.lang.imp]
p:191 [binder, in WiSE.lang.imp]
p:193 [binder, in WiSE.lang.imp]
p:197 [binder, in WiSE.lang.imp]
p:26 [binder, in WiSE.implem.bugfinder]
p:27 [binder, in WiSE.implem.bugfinder]
p:28 [binder, in WiSE.implem.bugfinder]
p:30 [binder, in WiSE.implem.bugfinder]
p:48 [binder, in WiSE.implem.bugfinder_proof]
p:5 [binder, in WiSE.implem.bugfinder]
p:67 [binder, in WiSE.implem.bugfinder_proof]
P:68 [binder, in WiSE.streams]
p:68 [binder, in WiSE.implem.bugfinder_proof]
p:70 [binder, in WiSE.implem.bugfinder_proof]
P:71 [binder, in WiSE.streams]
p:73 [binder, in WiSE.implem.bugfinder_proof]
P:75 [binder, in WiSE.streams]
P:79 [binder, in WiSE.streams]
p:79 [binder, in WiSE.implem.bugfinder_proof]
p:81 [binder, in WiSE.implem.bugfinder_proof]
p:82 [binder, in WiSE.implem.bugfinder_proof]
P:83 [binder, in WiSE.streams]
P:87 [binder, in WiSE.streams]
P:91 [binder, in WiSE.streams]
P:94 [binder, in WiSE.streams]
Q
Q:120 [binder, in WiSE.streams]q:4 [binder, in WiSE.implem.bugfinder]
Q:80 [binder, in WiSE.streams]
Q:84 [binder, in WiSE.streams]
Q:88 [binder, in WiSE.streams]
R
RA:21 [binder, in WiSE.relations]RA:30 [binder, in WiSE.relations]
RB:22 [binder, in WiSE.relations]
RB:31 [binder, in WiSE.relations]
Reach [definition, in WiSE.symbolic.symex]
Reach [definition, in WiSE.lang.imp]
reachable_from [definition, in WiSE.implem.bugfinder_proof]
Reach_complete [lemma, in WiSE.symbolic.symex]
Reach_sound [lemma, in WiSE.symbolic.symex]
reduce [definition, in WiSE.utils]
relations [library]
relatively_sound_bug_finding [definition, in WiSE.symbolic.symex]
relative_soundness [lemma, in WiSE.implem.bugfinder_proof]
relative_completeness [lemma, in WiSE.implem.bugfinder_proof]
run [definition, in WiSE.implem.bugfinder]
run_finished [lemma, in WiSE.implem.bugfinder_proof]
run_finished_nil [lemma, in WiSE.implem.bugfinder_proof]
run_complete [lemma, in WiSE.implem.bugfinder_proof]
run_steps_complete [lemma, in WiSE.implem.bugfinder_proof]
run_here [lemma, in WiSE.implem.bugfinder_proof]
run_step_complete [lemma, in WiSE.implem.bugfinder_proof]
run_sound [lemma, in WiSE.implem.bugfinder_proof]
run_n_S_length [lemma, in WiSE.implem.bugfinder_proof]
run_n_length [lemma, in WiSE.implem.bugfinder_proof]
run_n_nil [lemma, in WiSE.implem.bugfinder_proof]
run_run_n [lemma, in WiSE.implem.bugfinder_proof]
run_nil [lemma, in WiSE.implem.bugfinder_proof]
run_eq [lemma, in WiSE.implem.bugfinder_proof]
run_n [definition, in WiSE.implem.bugfinder]
S
SAT [constructor, in WiSE.symbolic.solver]sat [inductive, in WiSE.symbolic.solver]
scons [constructor, in WiSE.streams]
senv1:63 [binder, in WiSE.symbolic.symex]
senv1:71 [binder, in WiSE.symbolic.symex]
senv1:80 [binder, in WiSE.symbolic.symex]
senv1:88 [binder, in WiSE.symbolic.symex]
senv1:95 [binder, in WiSE.symbolic.symex]
senv2:64 [binder, in WiSE.symbolic.symex]
senv2:74 [binder, in WiSE.symbolic.symex]
senv2:83 [binder, in WiSE.symbolic.symex]
senv2:89 [binder, in WiSE.symbolic.symex]
senv2:96 [binder, in WiSE.symbolic.symex]
senv:103 [binder, in WiSE.symbolic.symex]
senv:111 [binder, in WiSE.symbolic.symex]
senv:127 [binder, in WiSE.symbolic.symex]
senv:135 [binder, in WiSE.symbolic.symex]
senv:19 [binder, in WiSE.symbolic.symex]
senv:22 [binder, in WiSE.symbolic.symex]
senv:25 [binder, in WiSE.symbolic.symex]
Seq [constructor, in WiSE.lang.imprec]
Seq [constructor, in WiSE.lang.imp]
Sequences [section, in WiSE.relations]
Sequences.A [variable, in WiSE.relations]
Sequences.R [variable, in WiSE.relations]
shift [definition, in WiSE.streams]
shift_eq [lemma, in WiSE.streams]
sim [definition, in WiSE.symbolic.symex]
simulation [definition, in WiSE.relations]
Simulation [section, in WiSE.relations]
sim_init [lemma, in WiSE.symbolic.symex]
sim:23 [binder, in WiSE.relations]
sim:32 [binder, in WiSE.relations]
Skip [constructor, in WiSE.lang.imprec]
Skip [constructor, in WiSE.lang.imp]
solver [definition, in WiSE.symbolic.solver]
solver [library]
solver_correct [lemma, in WiSE.symbolic.solver]
sound_termination [lemma, in WiSE.implem.bugfinder_proof]
star [inductive, in WiSE.relations]
starr [inductive, in WiSE.relations]
starr_star [lemma, in WiSE.relations]
starr_reflexive [instance, in WiSE.relations]
starr_trans [instance, in WiSE.relations]
starr_step [constructor, in WiSE.relations]
starr_refl [constructor, in WiSE.relations]
star_simulation [lemma, in WiSE.relations]
star_trans [instance, in WiSE.relations]
star_reflexive [instance, in WiSE.relations]
star_one [lemma, in WiSE.relations]
star_step [constructor, in WiSE.relations]
star_refl [constructor, in WiSE.relations]
status [inductive, in WiSE.implem.bugfinder]
step [inductive, in WiSE.lang.imp]
steps [definition, in WiSE.lang.imp]
steps_simulation_diagram [lemma, in WiSE.symbolic.symex]
steps_exec [lemma, in WiSE.lang.imp]
steps_seq [lemma, in WiSE.lang.imp]
step_simulation_diagram [lemma, in WiSE.symbolic.symex]
step_exec_exec [lemma, in WiSE.lang.imp]
step_Loop_false [constructor, in WiSE.lang.imp]
step_Loop_true [constructor, in WiSE.lang.imp]
step_Ite_false [constructor, in WiSE.lang.imp]
step_Ite_true [constructor, in WiSE.lang.imp]
step_Seq_Skip [constructor, in WiSE.lang.imp]
step_Seq [constructor, in WiSE.lang.imp]
step_Aff [constructor, in WiSE.lang.imp]
stmt [inductive, in WiSE.lang.imprec]
store [definition, in WiSE.lang.imp]
stream [inductive, in WiSE.streams]
streams [library]
stream_func_iso [lemma, in WiSE.streams]
stream_Eq [instance, in WiSE.streams]
stream_equ [definition, in WiSE.streams]
str:101 [binder, in WiSE.streams]
str:65 [binder, in WiSE.streams]
Stuck [definition, in WiSE.lang.imp]
st:150 [binder, in WiSE.lang.imp]
st:24 [binder, in WiSE.implem.bugfinder]
st:43 [binder, in WiSE.implem.bugfinder_proof]
st:46 [binder, in WiSE.implem.bugfinder_proof]
st:49 [binder, in WiSE.implem.bugfinder_proof]
st:51 [binder, in WiSE.implem.bugfinder_proof]
st:53 [binder, in WiSE.implem.bugfinder_proof]
st:74 [binder, in WiSE.implem.bugfinder_proof]
st:77 [binder, in WiSE.implem.bugfinder_proof]
Sub [constructor, in WiSE.lang.imprec]
Sub [constructor, in WiSE.lang.imp]
Symbolic [definition, in WiSE.implem.bugfinder_proof]
symex [library]
symex_complete [lemma, in WiSE.symbolic.symex]
symex_sound [lemma, in WiSE.symbolic.symex]
sym_steps_steps [lemma, in WiSE.symbolic.symex]
sym_steps_steps_aux [lemma, in WiSE.symbolic.symex]
sym_steps_path [lemma, in WiSE.symbolic.symex]
sym_step_path [lemma, in WiSE.symbolic.symex]
sym_step_step [lemma, in WiSE.symbolic.symex]
sym_steps [definition, in WiSE.symbolic.symex]
sym_step_Loop_false [constructor, in WiSE.symbolic.symex]
sym_step_Loop_true [constructor, in WiSE.symbolic.symex]
sym_step_Ite_false [constructor, in WiSE.symbolic.symex]
sym_step_Ite_true [constructor, in WiSE.symbolic.symex]
sym_step_Seq_Skip [constructor, in WiSE.symbolic.symex]
sym_step_Seq [constructor, in WiSE.symbolic.symex]
sym_step_Aff [constructor, in WiSE.symbolic.symex]
sym_step [inductive, in WiSE.symbolic.symex]
sym_state [definition, in WiSE.symbolic.symex]
sym_beval [definition, in WiSE.symbolic.symex]
sym_aeval [definition, in WiSE.symbolic.symex]
sym_update [definition, in WiSE.symbolic.symex]
sym_store [definition, in WiSE.symbolic.symex]
s'':77 [binder, in WiSE.lang.imp]
s'':92 [binder, in WiSE.lang.imp]
s':121 [binder, in WiSE.symbolic.symex]
s':123 [binder, in WiSE.symbolic.symex]
s':136 [binder, in WiSE.lang.imp]
s':144 [binder, in WiSE.lang.imp]
s':148 [binder, in WiSE.lang.imp]
s':181 [binder, in WiSE.lang.imp]
s':58 [binder, in WiSE.implem.bugfinder_proof]
s':61 [binder, in WiSE.implem.bugfinder_proof]
s':64 [binder, in WiSE.implem.bugfinder_proof]
s':69 [binder, in WiSE.implem.bugfinder_proof]
s':76 [binder, in WiSE.lang.imp]
s':81 [binder, in WiSE.lang.imp]
s':86 [binder, in WiSE.lang.imp]
s':91 [binder, in WiSE.lang.imp]
s0:41 [binder, in WiSE.implem.bugfinder_proof]
s1:104 [binder, in WiSE.lang.imp]
s1:125 [binder, in WiSE.streams]
s1:129 [binder, in WiSE.lang.imp]
s1:139 [binder, in WiSE.lang.imp]
s1:19 [binder, in WiSE.implem.bugfinder_proof]
s1:37 [binder, in WiSE.symbolic.symex]
s2:105 [binder, in WiSE.lang.imp]
s2:126 [binder, in WiSE.streams]
s2:130 [binder, in WiSE.lang.imp]
s2:140 [binder, in WiSE.lang.imp]
s2:20 [binder, in WiSE.implem.bugfinder_proof]
s2:38 [binder, in WiSE.symbolic.symex]
s3:141 [binder, in WiSE.lang.imp]
s:10 [binder, in WiSE.symbolic.symex]
s:10 [binder, in WiSE.streams]
s:100 [binder, in WiSE.lang.imp]
s:104 [binder, in WiSE.streams]
s:107 [binder, in WiSE.streams]
s:109 [binder, in WiSE.lang.imp]
s:110 [binder, in WiSE.streams]
s:111 [binder, in WiSE.lang.imp]
s:114 [binder, in WiSE.streams]
s:115 [binder, in WiSE.lang.imp]
s:118 [binder, in WiSE.streams]
s:119 [binder, in WiSE.lang.imp]
s:120 [binder, in WiSE.symbolic.symex]
s:122 [binder, in WiSE.symbolic.symex]
s:122 [binder, in WiSE.lang.imp]
s:13 [binder, in WiSE.streams]
s:135 [binder, in WiSE.lang.imp]
s:14 [binder, in WiSE.symbolic.symex]
s:143 [binder, in WiSE.lang.imp]
s:146 [binder, in WiSE.lang.imp]
s:165 [binder, in WiSE.lang.imp]
s:172 [binder, in WiSE.lang.imp]
s:18 [binder, in WiSE.implem.bugfinder_proof]
s:180 [binder, in WiSE.lang.imp]
s:19 [binder, in WiSE.streams]
s:2 [binder, in WiSE.symbolic.symex]
s:22 [binder, in WiSE.lang.imprec]
s:24 [binder, in WiSE.streams]
s:24 [binder, in WiSE.lang.imp]
s:3 [binder, in WiSE.implem.bugfinder]
s:30 [binder, in WiSE.symbolic.symex]
s:33 [binder, in WiSE.streams]
s:36 [binder, in WiSE.implem.bugfinder]
s:36 [binder, in WiSE.lang.imp]
s:39 [binder, in WiSE.implem.bugfinder_proof]
s:40 [binder, in WiSE.streams]
s:42 [binder, in WiSE.symbolic.symex]
s:42 [binder, in WiSE.implem.bugfinder_proof]
s:45 [binder, in WiSE.symbolic.symex]
s:45 [binder, in WiSE.implem.bugfinder_proof]
s:48 [binder, in WiSE.lang.imp]
s:50 [binder, in WiSE.symbolic.symex]
s:50 [binder, in WiSE.streams]
s:52 [binder, in WiSE.lang.imp]
s:55 [binder, in WiSE.symbolic.symex]
s:55 [binder, in WiSE.streams]
s:56 [binder, in WiSE.lang.imp]
s:57 [binder, in WiSE.implem.bugfinder_proof]
s:59 [binder, in WiSE.symbolic.symex]
s:59 [binder, in WiSE.implem.bugfinder_proof]
s:60 [binder, in WiSE.implem.bugfinder_proof]
s:60 [binder, in WiSE.lang.imp]
s:61 [binder, in WiSE.streams]
s:63 [binder, in WiSE.implem.bugfinder_proof]
s:64 [binder, in WiSE.lang.imp]
s:69 [binder, in WiSE.streams]
s:7 [binder, in WiSE.symbolic.symex]
s:7 [binder, in WiSE.streams]
s:70 [binder, in WiSE.lang.imp]
s:71 [binder, in WiSE.lang.imp]
s:72 [binder, in WiSE.streams]
s:75 [binder, in WiSE.lang.imp]
s:76 [binder, in WiSE.streams]
s:80 [binder, in WiSE.lang.imp]
s:81 [binder, in WiSE.streams]
s:85 [binder, in WiSE.streams]
s:85 [binder, in WiSE.lang.imp]
s:89 [binder, in WiSE.streams]
s:90 [binder, in WiSE.lang.imp]
s:92 [binder, in WiSE.streams]
s:95 [binder, in WiSE.streams]
s:95 [binder, in WiSE.lang.imp]
T
tasks [definition, in WiSE.implem.bugfinder]tasks:19 [binder, in WiSE.implem.bugfinder]
tasks:38 [binder, in WiSE.implem.bugfinder_proof]
then_do [definition, in WiSE.implem.bugfinder]
trivial_assertion [definition, in WiSE.implem.bugfinder]
t:10 [binder, in WiSE.implem.bugfinder_proof]
t:14 [binder, in WiSE.implem.bugfinder_proof]
U
UNSAT [constructor, in WiSE.symbolic.solver]untill [definition, in WiSE.streams]
update [definition, in WiSE.lang.imp]
utils [library]
V
ValidBug [definition, in WiSE.implem.bugfinder_proof]ValidStatus [definition, in WiSE.implem.bugfinder_proof]
Var [constructor, in WiSE.lang.imprec]
Var [constructor, in WiSE.lang.imp]
variable [inductive, in WiSE.lang.imprec]
ve:103 [binder, in WiSE.lang.imp]
ve:34 [binder, in WiSE.symbolic.symex]
ve:74 [binder, in WiSE.lang.imp]
vx:35 [binder, in WiSE.lang.imp]
vx:47 [binder, in WiSE.lang.imp]
vx:63 [binder, in WiSE.lang.imp]
vx:67 [binder, in WiSE.lang.imp]
V0:141 [binder, in WiSE.symbolic.symex]
V0:148 [binder, in WiSE.symbolic.symex]
V0:159 [binder, in WiSE.symbolic.symex]
V0:163 [binder, in WiSE.symbolic.symex]
V0:188 [binder, in WiSE.lang.imp]
V0:194 [binder, in WiSE.lang.imp]
V:196 [binder, in WiSE.lang.imp]
v:50 [binder, in WiSE.lang.imp]
X
xs:13 [binder, in WiSE.utils]xs:18 [binder, in WiSE.utils]
xs:30 [binder, in WiSE.streams]
xs:47 [binder, in WiSE.streams]
xs:5 [binder, in WiSE.streams]
x:1 [binder, in WiSE.symbolic.symex]
x:101 [binder, in WiSE.lang.imp]
x:102 [binder, in WiSE.streams]
x:128 [binder, in WiSE.lang.imp]
x:13 [binder, in WiSE.relations]
x:14 [binder, in WiSE.relations]
x:143 [binder, in WiSE.streams]
x:145 [binder, in WiSE.streams]
x:15 [binder, in WiSE.lang.imprec]
x:157 [binder, in WiSE.lang.imp]
x:17 [binder, in WiSE.relations]
x:19 [binder, in WiSE.lang.imprec]
x:23 [binder, in WiSE.lang.imprec]
x:27 [binder, in WiSE.symbolic.symex]
x:29 [binder, in WiSE.lang.imprec]
x:29 [binder, in WiSE.streams]
x:29 [binder, in WiSE.lang.imp]
x:3 [binder, in WiSE.lang.imprec]
x:3 [binder, in WiSE.symbolic.symex]
x:32 [binder, in WiSE.symbolic.symex]
x:32 [binder, in WiSE.implem.bugfinder]
x:34 [binder, in WiSE.implem.bugfinder]
x:34 [binder, in WiSE.lang.imp]
x:4 [binder, in WiSE.lang.imprec]
x:4 [binder, in WiSE.streams]
x:41 [binder, in WiSE.lang.imp]
x:46 [binder, in WiSE.streams]
x:46 [binder, in WiSE.lang.imp]
x:49 [binder, in WiSE.lang.imp]
x:5 [binder, in WiSE.relations]
x:54 [binder, in WiSE.lang.imp]
x:58 [binder, in WiSE.lang.imp]
x:6 [binder, in WiSE.relations]
x:62 [binder, in WiSE.lang.imp]
x:66 [binder, in WiSE.lang.imp]
x:72 [binder, in WiSE.lang.imp]
X:77 [binder, in WiSE.symbolic.symex]
x:8 [binder, in WiSE.symbolic.symex]
X:86 [binder, in WiSE.symbolic.symex]
x:9 [binder, in WiSE.relations]
x:96 [binder, in WiSE.streams]
Y
y:10 [binder, in WiSE.relations]y:15 [binder, in WiSE.relations]
y:18 [binder, in WiSE.relations]
y:5 [binder, in WiSE.symbolic.symex]
y:51 [binder, in WiSE.lang.imp]
y:6 [binder, in WiSE.utils]
y:7 [binder, in WiSE.relations]
Y:78 [binder, in WiSE.symbolic.symex]
Y:87 [binder, in WiSE.symbolic.symex]
Z
z:16 [binder, in WiSE.relations]z:8 [binder, in WiSE.relations]
other
_ @ _ ≃ _ [notation, in WiSE.symbolic.symex]_ ∘ _ [notation, in WiSE.symbolic.symex]
_ ≃ _ [notation, in WiSE.equalities]
_ ≡ _ [notation, in WiSE.equalities]
!! _ [notation, in WiSE.implem.bugfinder_proof]
! _ [notation, in WiSE.implem.bugfinder_proof]
π1:35 [binder, in WiSE.symbolic.symex]
π1:65 [binder, in WiSE.symbolic.symex]
π1:70 [binder, in WiSE.symbolic.symex]
π1:79 [binder, in WiSE.symbolic.symex]
π1:90 [binder, in WiSE.symbolic.symex]
π1:97 [binder, in WiSE.symbolic.symex]
π2:36 [binder, in WiSE.symbolic.symex]
π2:66 [binder, in WiSE.symbolic.symex]
π2:73 [binder, in WiSE.symbolic.symex]
π2:82 [binder, in WiSE.symbolic.symex]
π2:91 [binder, in WiSE.symbolic.symex]
π2:98 [binder, in WiSE.symbolic.symex]
π:101 [binder, in WiSE.symbolic.symex]
π:112 [binder, in WiSE.symbolic.symex]
π:134 [binder, in WiSE.symbolic.symex]
π:31 [binder, in WiSE.symbolic.symex]
π:44 [binder, in WiSE.symbolic.symex]
π:49 [binder, in WiSE.symbolic.symex]
π:54 [binder, in WiSE.symbolic.symex]
π:58 [binder, in WiSE.symbolic.symex]
σ':142 [binder, in WiSE.symbolic.symex]
σ':150 [binder, in WiSE.symbolic.symex]
σ':162 [binder, in WiSE.symbolic.symex]
σ':71 [binder, in WiSE.implem.bugfinder_proof]
σ:139 [binder, in WiSE.symbolic.symex]
σ:140 [binder, in WiSE.symbolic.symex]
σ:144 [binder, in WiSE.symbolic.symex]
σ:146 [binder, in WiSE.symbolic.symex]
σ:149 [binder, in WiSE.symbolic.symex]
σ:152 [binder, in WiSE.symbolic.symex]
σ:154 [binder, in WiSE.symbolic.symex]
σ:157 [binder, in WiSE.symbolic.symex]
σ:160 [binder, in WiSE.symbolic.symex]
σ:161 [binder, in WiSE.symbolic.symex]
σ:183 [binder, in WiSE.lang.imp]
σ:186 [binder, in WiSE.lang.imp]
σ:187 [binder, in WiSE.lang.imp]
σ:190 [binder, in WiSE.lang.imp]
σ:192 [binder, in WiSE.lang.imp]
σ:195 [binder, in WiSE.lang.imp]
σ:72 [binder, in WiSE.implem.bugfinder_proof]
σ:76 [binder, in WiSE.implem.bugfinder_proof]
σ:80 [binder, in WiSE.implem.bugfinder_proof]
Notation Index
E
Bug _ [in WiSE.implem.bugfinder]L
_ ⊨ _ [in WiSE.streams]_ ∧ _ [in WiSE.streams]
_ ∨ _ [in WiSE.streams]
_ → _ [in WiSE.streams]
!! _ [in WiSE.streams]
! _ [in WiSE.streams]
¬ _ [in WiSE.streams]
□ _ [in WiSE.streams]
◊ _ [in WiSE.streams]
◯ _ [in WiSE.streams]
other
_ @ _ ≃ _ [in WiSE.symbolic.symex]_ ∘ _ [in WiSE.symbolic.symex]
_ ≃ _ [in WiSE.equalities]
_ ≡ _ [in WiSE.equalities]
!! _ [in WiSE.implem.bugfinder_proof]
! _ [in WiSE.implem.bugfinder_proof]
Binder Index
A
a1:1 [in WiSE.symbolic.solver]a1:13 [in WiSE.symbolic.solver]
a1:16 [in WiSE.symbolic.solver]
a1:24 [in WiSE.relations]
a1:3 [in WiSE.lang.imp]
a1:5 [in WiSE.symbolic.solver]
a2:14 [in WiSE.symbolic.solver]
a2:17 [in WiSE.symbolic.solver]
a2:2 [in WiSE.symbolic.solver]
a2:25 [in WiSE.relations]
a2:4 [in WiSE.lang.imp]
a2:6 [in WiSE.symbolic.solver]
A:1 [in WiSE.streams]
A:1 [in WiSE.equalities]
A:1 [in WiSE.utils]
A:1 [in WiSE.implem.bugfinder_proof]
a:10 [in WiSE.equalities]
A:103 [in WiSE.streams]
A:106 [in WiSE.streams]
A:109 [in WiSE.streams]
A:11 [in WiSE.streams]
A:113 [in WiSE.streams]
A:117 [in WiSE.streams]
A:12 [in WiSE.equalities]
A:123 [in WiSE.streams]
A:124 [in WiSE.streams]
A:128 [in WiSE.streams]
A:132 [in WiSE.streams]
A:133 [in WiSE.streams]
A:134 [in WiSE.streams]
A:138 [in WiSE.streams]
A:14 [in WiSE.utils]
A:142 [in WiSE.streams]
A:17 [in WiSE.streams]
a:19 [in WiSE.symbolic.solver]
A:19 [in WiSE.utils]
A:19 [in WiSE.relations]
a:19 [in WiSE.lang.imp]
A:23 [in WiSE.streams]
A:27 [in WiSE.streams]
A:28 [in WiSE.relations]
A:31 [in WiSE.streams]
A:37 [in WiSE.streams]
A:4 [in WiSE.equalities]
A:43 [in WiSE.streams]
A:48 [in WiSE.streams]
A:53 [in WiSE.streams]
A:58 [in WiSE.streams]
A:6 [in WiSE.streams]
a:6 [in WiSE.implem.bugfinder_proof]
A:62 [in WiSE.streams]
A:66 [in WiSE.streams]
A:67 [in WiSE.streams]
A:7 [in WiSE.utils]
A:70 [in WiSE.streams]
A:74 [in WiSE.streams]
A:78 [in WiSE.streams]
a:8 [in WiSE.lang.imp]
A:82 [in WiSE.streams]
A:86 [in WiSE.streams]
a:9 [in WiSE.symbolic.solver]
A:9 [in WiSE.streams]
A:90 [in WiSE.streams]
A:93 [in WiSE.streams]
A:97 [in WiSE.streams]
B
b1:12 [in WiSE.lang.imp]b1:14 [in WiSE.lang.imp]
b1:20 [in WiSE.symbolic.solver]
b1:26 [in WiSE.relations]
b1:30 [in WiSE.symbolic.solver]
b1:9 [in WiSE.lang.imprec]
b2:10 [in WiSE.lang.imprec]
b2:13 [in WiSE.lang.imp]
b2:15 [in WiSE.lang.imp]
b2:21 [in WiSE.symbolic.solver]
b2:27 [in WiSE.relations]
b2:31 [in WiSE.symbolic.solver]
b:11 [in WiSE.equalities]
B:13 [in WiSE.equalities]
b:153 [in WiSE.lang.imp]
b:163 [in WiSE.lang.imp]
b:18 [in WiSE.lang.imprec]
B:2 [in WiSE.implem.bugfinder_proof]
B:20 [in WiSE.relations]
b:20 [in WiSE.lang.imp]
b:24 [in WiSE.symbolic.solver]
b:26 [in WiSE.symbolic.solver]
B:29 [in WiSE.relations]
b:33 [in WiSE.symbolic.solver]
b:35 [in WiSE.symbolic.solver]
b:38 [in WiSE.symbolic.solver]
B:38 [in WiSE.streams]
b:39 [in WiSE.symbolic.solver]
b:42 [in WiSE.symbolic.solver]
B:44 [in WiSE.streams]
B:5 [in WiSE.equalities]
b:5 [in WiSE.implem.bugfinder_proof]
B:59 [in WiSE.streams]
B:8 [in WiSE.utils]
b:9 [in WiSE.lang.imp]
B:98 [in WiSE.streams]
C
cond:29 [in WiSE.implem.bugfinder]cond:31 [in WiSE.implem.bugfinder]
c1:106 [in WiSE.lang.imp]
c1:113 [in WiSE.lang.imp]
c1:117 [in WiSE.lang.imp]
c1:131 [in WiSE.lang.imp]
c1:137 [in WiSE.lang.imp]
c1:39 [in WiSE.symbolic.symex]
c1:47 [in WiSE.symbolic.symex]
c1:52 [in WiSE.symbolic.symex]
c1:67 [in WiSE.symbolic.symex]
c1:72 [in WiSE.symbolic.symex]
c1:78 [in WiSE.lang.imp]
c1:81 [in WiSE.symbolic.symex]
c1:83 [in WiSE.lang.imp]
c1:88 [in WiSE.lang.imp]
c1:92 [in WiSE.symbolic.symex]
c1:99 [in WiSE.symbolic.symex]
c2:100 [in WiSE.symbolic.symex]
c2:107 [in WiSE.lang.imp]
c2:114 [in WiSE.lang.imp]
c2:118 [in WiSE.lang.imp]
c2:132 [in WiSE.lang.imp]
c2:138 [in WiSE.lang.imp]
c2:40 [in WiSE.symbolic.symex]
c2:48 [in WiSE.symbolic.symex]
c2:53 [in WiSE.symbolic.symex]
c2:68 [in WiSE.symbolic.symex]
c2:75 [in WiSE.symbolic.symex]
c2:79 [in WiSE.lang.imp]
c2:84 [in WiSE.symbolic.symex]
c2:84 [in WiSE.lang.imp]
c2:89 [in WiSE.lang.imp]
c2:93 [in WiSE.symbolic.symex]
c3:108 [in WiSE.lang.imp]
c3:133 [in WiSE.lang.imp]
c3:41 [in WiSE.symbolic.symex]
c:110 [in WiSE.lang.imp]
c:121 [in WiSE.lang.imp]
c:124 [in WiSE.lang.imp]
c:13 [in WiSE.lang.imprec]
c:23 [in WiSE.lang.imp]
c:43 [in WiSE.symbolic.symex]
c:57 [in WiSE.symbolic.symex]
c:57 [in WiSE.lang.imp]
c:61 [in WiSE.symbolic.symex]
c:65 [in WiSE.lang.imp]
c:94 [in WiSE.lang.imp]
c:97 [in WiSE.lang.imp]
E
env0:106 [in WiSE.symbolic.symex]env0:114 [in WiSE.symbolic.symex]
env0:117 [in WiSE.symbolic.symex]
env0:129 [in WiSE.symbolic.symex]
env0:130 [in WiSE.symbolic.symex]
env1:125 [in WiSE.lang.imp]
env1:132 [in WiSE.symbolic.symex]
env2:126 [in WiSE.lang.imp]
env:10 [in WiSE.implem.bugfinder]
env:102 [in WiSE.symbolic.symex]
env:108 [in WiSE.symbolic.symex]
env:115 [in WiSE.symbolic.symex]
env:118 [in WiSE.symbolic.symex]
env:12 [in WiSE.symbolic.solver]
env:12 [in WiSE.implem.bugfinder_proof]
env:15 [in WiSE.symbolic.solver]
env:151 [in WiSE.lang.imp]
env:152 [in WiSE.lang.imp]
env:156 [in WiSE.lang.imp]
env:159 [in WiSE.lang.imp]
env:16 [in WiSE.implem.bugfinder_proof]
env:162 [in WiSE.lang.imp]
env:18 [in WiSE.symbolic.symex]
env:18 [in WiSE.symbolic.solver]
env:21 [in WiSE.symbolic.symex]
env:23 [in WiSE.implem.bugfinder_proof]
env:24 [in WiSE.symbolic.symex]
env:29 [in WiSE.symbolic.solver]
env:32 [in WiSE.symbolic.solver]
env:34 [in WiSE.symbolic.solver]
env:35 [in WiSE.implem.bugfinder_proof]
env:40 [in WiSE.symbolic.solver]
env:41 [in WiSE.symbolic.solver]
env:6 [in WiSE.symbolic.symex]
env:6 [in WiSE.implem.bugfinder]
env:62 [in WiSE.symbolic.symex]
env:69 [in WiSE.symbolic.symex]
env:76 [in WiSE.symbolic.symex]
env:8 [in WiSE.implem.bugfinder_proof]
env:85 [in WiSE.symbolic.symex]
env:9 [in WiSE.symbolic.symex]
env:94 [in WiSE.symbolic.symex]
e':30 [in WiSE.lang.imp]
e':42 [in WiSE.lang.imp]
e':55 [in WiSE.lang.imp]
e:102 [in WiSE.lang.imp]
e:11 [in WiSE.symbolic.symex]
e:112 [in WiSE.lang.imp]
e:116 [in WiSE.lang.imp]
e:120 [in WiSE.lang.imp]
e:123 [in WiSE.lang.imp]
e:127 [in WiSE.lang.imp]
e:14 [in WiSE.lang.imprec]
e:15 [in WiSE.symbolic.symex]
e:158 [in WiSE.lang.imp]
e:20 [in WiSE.symbolic.symex]
e:23 [in WiSE.symbolic.symex]
e:25 [in WiSE.lang.imp]
e:26 [in WiSE.symbolic.symex]
e:28 [in WiSE.lang.imp]
e:33 [in WiSE.symbolic.symex]
e:33 [in WiSE.lang.imp]
e:36 [in WiSE.lang.imprec]
e:37 [in WiSE.lang.imp]
e:4 [in WiSE.symbolic.symex]
e:40 [in WiSE.lang.imp]
e:45 [in WiSE.lang.imp]
e:46 [in WiSE.symbolic.symex]
e:51 [in WiSE.symbolic.symex]
e:53 [in WiSE.lang.imp]
e:56 [in WiSE.symbolic.symex]
e:59 [in WiSE.lang.imp]
e:60 [in WiSE.symbolic.symex]
e:61 [in WiSE.lang.imp]
e:73 [in WiSE.lang.imp]
e:82 [in WiSE.lang.imp]
e:87 [in WiSE.lang.imp]
e:93 [in WiSE.lang.imp]
e:96 [in WiSE.lang.imp]
F
f1:129 [in WiSE.streams]f2:130 [in WiSE.streams]
f:105 [in WiSE.streams]
f:136 [in WiSE.streams]
f:140 [in WiSE.streams]
f:16 [in WiSE.equalities]
f:2 [in WiSE.utils]
f:3 [in WiSE.implem.bugfinder_proof]
f:39 [in WiSE.streams]
f:45 [in WiSE.streams]
f:49 [in WiSE.streams]
f:54 [in WiSE.streams]
f:60 [in WiSE.streams]
f:8 [in WiSE.equalities]
f:9 [in WiSE.utils]
f:99 [in WiSE.streams]
G
gs:34 [in WiSE.lang.imprec]g:17 [in WiSE.equalities]
g:9 [in WiSE.equalities]
H
H0:15 [in WiSE.equalities]H0:7 [in WiSE.equalities]
H:14 [in WiSE.equalities]
H:6 [in WiSE.equalities]
L
ls:35 [in WiSE.lang.imprec]l1:29 [in WiSE.implem.bugfinder_proof]
l1:32 [in WiSE.implem.bugfinder_proof]
l2:30 [in WiSE.implem.bugfinder_proof]
l2:33 [in WiSE.implem.bugfinder_proof]
l3:31 [in WiSE.implem.bugfinder_proof]
l3:37 [in WiSE.implem.bugfinder_proof]
l:10 [in WiSE.utils]
l:14 [in WiSE.implem.bugfinder]
l:15 [in WiSE.utils]
l:20 [in WiSE.utils]
l:21 [in WiSE.implem.bugfinder_proof]
l:27 [in WiSE.implem.bugfinder_proof]
l:3 [in WiSE.utils]
l:4 [in WiSE.implem.bugfinder_proof]
l:55 [in WiSE.implem.bugfinder_proof]
l:56 [in WiSE.implem.bugfinder_proof]
l:62 [in WiSE.implem.bugfinder_proof]
l:65 [in WiSE.implem.bugfinder_proof]
l:66 [in WiSE.implem.bugfinder_proof]
M
m:122 [in WiSE.streams]m:141 [in WiSE.streams]
m:26 [in WiSE.streams]
m:63 [in WiSE.streams]
N
next_next:23 [in WiSE.implem.bugfinder]next_next:17 [in WiSE.implem.bugfinder]
n:112 [in WiSE.streams]
n:116 [in WiSE.streams]
n:12 [in WiSE.streams]
n:121 [in WiSE.streams]
n:127 [in WiSE.streams]
n:131 [in WiSE.streams]
n:135 [in WiSE.streams]
n:139 [in WiSE.streams]
n:144 [in WiSE.streams]
n:146 [in WiSE.streams]
n:18 [in WiSE.streams]
n:18 [in WiSE.implem.bugfinder]
n:25 [in WiSE.streams]
n:25 [in WiSE.implem.bugfinder_proof]
n:26 [in WiSE.implem.bugfinder_proof]
n:28 [in WiSE.streams]
n:28 [in WiSE.implem.bugfinder_proof]
n:32 [in WiSE.streams]
n:56 [in WiSE.streams]
n:57 [in WiSE.streams]
n:64 [in WiSE.streams]
n:73 [in WiSE.streams]
n:77 [in WiSE.streams]
P
path:11 [in WiSE.implem.bugfinder_proof]path:126 [in WiSE.symbolic.symex]
path:15 [in WiSE.implem.bugfinder_proof]
path:22 [in WiSE.implem.bugfinder_proof]
path:34 [in WiSE.implem.bugfinder_proof]
path:7 [in WiSE.implem.bugfinder_proof]
path:7 [in WiSE.implem.bugfinder]
path:9 [in WiSE.implem.bugfinder]
pat:109 [in WiSE.symbolic.symex]
pat:113 [in WiSE.symbolic.symex]
pat:147 [in WiSE.lang.imp]
pat:8 [in WiSE.implem.bugfinder]
prog0:125 [in WiSE.symbolic.symex]
prog0:131 [in WiSE.symbolic.symex]
prog1:133 [in WiSE.symbolic.symex]
prog:11 [in WiSE.implem.bugfinder]
prog:128 [in WiSE.symbolic.symex]
prog:13 [in WiSE.implem.bugfinder_proof]
prog:136 [in WiSE.symbolic.symex]
prog:17 [in WiSE.implem.bugfinder_proof]
prog:24 [in WiSE.implem.bugfinder_proof]
prog:36 [in WiSE.implem.bugfinder_proof]
prog:9 [in WiSE.implem.bugfinder_proof]
p':107 [in WiSE.symbolic.symex]
p':149 [in WiSE.lang.imp]
p1:104 [in WiSE.symbolic.symex]
p1:154 [in WiSE.lang.imp]
p1:160 [in WiSE.lang.imp]
p1:166 [in WiSE.lang.imp]
p1:170 [in WiSE.lang.imp]
p2:105 [in WiSE.symbolic.symex]
p2:155 [in WiSE.lang.imp]
p2:161 [in WiSE.lang.imp]
p2:167 [in WiSE.lang.imp]
p2:171 [in WiSE.lang.imp]
P:100 [in WiSE.streams]
P:108 [in WiSE.streams]
p:110 [in WiSE.symbolic.symex]
P:111 [in WiSE.streams]
P:115 [in WiSE.streams]
p:116 [in WiSE.symbolic.symex]
p:119 [in WiSE.symbolic.symex]
P:119 [in WiSE.streams]
p:134 [in WiSE.lang.imp]
p:137 [in WiSE.symbolic.symex]
p:138 [in WiSE.symbolic.symex]
p:142 [in WiSE.lang.imp]
p:143 [in WiSE.symbolic.symex]
p:145 [in WiSE.symbolic.symex]
p:145 [in WiSE.lang.imp]
p:147 [in WiSE.symbolic.symex]
p:151 [in WiSE.symbolic.symex]
p:153 [in WiSE.symbolic.symex]
p:155 [in WiSE.symbolic.symex]
p:156 [in WiSE.symbolic.symex]
p:158 [in WiSE.symbolic.symex]
p:164 [in WiSE.lang.imp]
p:173 [in WiSE.lang.imp]
p:174 [in WiSE.lang.imp]
p:177 [in WiSE.lang.imp]
p:178 [in WiSE.lang.imp]
p:184 [in WiSE.lang.imp]
p:185 [in WiSE.lang.imp]
p:189 [in WiSE.lang.imp]
p:191 [in WiSE.lang.imp]
p:193 [in WiSE.lang.imp]
p:197 [in WiSE.lang.imp]
p:26 [in WiSE.implem.bugfinder]
p:27 [in WiSE.implem.bugfinder]
p:28 [in WiSE.implem.bugfinder]
p:30 [in WiSE.implem.bugfinder]
p:48 [in WiSE.implem.bugfinder_proof]
p:5 [in WiSE.implem.bugfinder]
p:67 [in WiSE.implem.bugfinder_proof]
P:68 [in WiSE.streams]
p:68 [in WiSE.implem.bugfinder_proof]
p:70 [in WiSE.implem.bugfinder_proof]
P:71 [in WiSE.streams]
p:73 [in WiSE.implem.bugfinder_proof]
P:75 [in WiSE.streams]
P:79 [in WiSE.streams]
p:79 [in WiSE.implem.bugfinder_proof]
p:81 [in WiSE.implem.bugfinder_proof]
p:82 [in WiSE.implem.bugfinder_proof]
P:83 [in WiSE.streams]
P:87 [in WiSE.streams]
P:91 [in WiSE.streams]
P:94 [in WiSE.streams]
Q
Q:120 [in WiSE.streams]q:4 [in WiSE.implem.bugfinder]
Q:80 [in WiSE.streams]
Q:84 [in WiSE.streams]
Q:88 [in WiSE.streams]
R
RA:21 [in WiSE.relations]RA:30 [in WiSE.relations]
RB:22 [in WiSE.relations]
RB:31 [in WiSE.relations]
S
senv1:63 [in WiSE.symbolic.symex]senv1:71 [in WiSE.symbolic.symex]
senv1:80 [in WiSE.symbolic.symex]
senv1:88 [in WiSE.symbolic.symex]
senv1:95 [in WiSE.symbolic.symex]
senv2:64 [in WiSE.symbolic.symex]
senv2:74 [in WiSE.symbolic.symex]
senv2:83 [in WiSE.symbolic.symex]
senv2:89 [in WiSE.symbolic.symex]
senv2:96 [in WiSE.symbolic.symex]
senv:103 [in WiSE.symbolic.symex]
senv:111 [in WiSE.symbolic.symex]
senv:127 [in WiSE.symbolic.symex]
senv:135 [in WiSE.symbolic.symex]
senv:19 [in WiSE.symbolic.symex]
senv:22 [in WiSE.symbolic.symex]
senv:25 [in WiSE.symbolic.symex]
sim:23 [in WiSE.relations]
sim:32 [in WiSE.relations]
str:101 [in WiSE.streams]
str:65 [in WiSE.streams]
st:150 [in WiSE.lang.imp]
st:24 [in WiSE.implem.bugfinder]
st:43 [in WiSE.implem.bugfinder_proof]
st:46 [in WiSE.implem.bugfinder_proof]
st:49 [in WiSE.implem.bugfinder_proof]
st:51 [in WiSE.implem.bugfinder_proof]
st:53 [in WiSE.implem.bugfinder_proof]
st:74 [in WiSE.implem.bugfinder_proof]
st:77 [in WiSE.implem.bugfinder_proof]
s'':77 [in WiSE.lang.imp]
s'':92 [in WiSE.lang.imp]
s':121 [in WiSE.symbolic.symex]
s':123 [in WiSE.symbolic.symex]
s':136 [in WiSE.lang.imp]
s':144 [in WiSE.lang.imp]
s':148 [in WiSE.lang.imp]
s':181 [in WiSE.lang.imp]
s':58 [in WiSE.implem.bugfinder_proof]
s':61 [in WiSE.implem.bugfinder_proof]
s':64 [in WiSE.implem.bugfinder_proof]
s':69 [in WiSE.implem.bugfinder_proof]
s':76 [in WiSE.lang.imp]
s':81 [in WiSE.lang.imp]
s':86 [in WiSE.lang.imp]
s':91 [in WiSE.lang.imp]
s0:41 [in WiSE.implem.bugfinder_proof]
s1:104 [in WiSE.lang.imp]
s1:125 [in WiSE.streams]
s1:129 [in WiSE.lang.imp]
s1:139 [in WiSE.lang.imp]
s1:19 [in WiSE.implem.bugfinder_proof]
s1:37 [in WiSE.symbolic.symex]
s2:105 [in WiSE.lang.imp]
s2:126 [in WiSE.streams]
s2:130 [in WiSE.lang.imp]
s2:140 [in WiSE.lang.imp]
s2:20 [in WiSE.implem.bugfinder_proof]
s2:38 [in WiSE.symbolic.symex]
s3:141 [in WiSE.lang.imp]
s:10 [in WiSE.symbolic.symex]
s:10 [in WiSE.streams]
s:100 [in WiSE.lang.imp]
s:104 [in WiSE.streams]
s:107 [in WiSE.streams]
s:109 [in WiSE.lang.imp]
s:110 [in WiSE.streams]
s:111 [in WiSE.lang.imp]
s:114 [in WiSE.streams]
s:115 [in WiSE.lang.imp]
s:118 [in WiSE.streams]
s:119 [in WiSE.lang.imp]
s:120 [in WiSE.symbolic.symex]
s:122 [in WiSE.symbolic.symex]
s:122 [in WiSE.lang.imp]
s:13 [in WiSE.streams]
s:135 [in WiSE.lang.imp]
s:14 [in WiSE.symbolic.symex]
s:143 [in WiSE.lang.imp]
s:146 [in WiSE.lang.imp]
s:165 [in WiSE.lang.imp]
s:172 [in WiSE.lang.imp]
s:18 [in WiSE.implem.bugfinder_proof]
s:180 [in WiSE.lang.imp]
s:19 [in WiSE.streams]
s:2 [in WiSE.symbolic.symex]
s:22 [in WiSE.lang.imprec]
s:24 [in WiSE.streams]
s:24 [in WiSE.lang.imp]
s:3 [in WiSE.implem.bugfinder]
s:30 [in WiSE.symbolic.symex]
s:33 [in WiSE.streams]
s:36 [in WiSE.implem.bugfinder]
s:36 [in WiSE.lang.imp]
s:39 [in WiSE.implem.bugfinder_proof]
s:40 [in WiSE.streams]
s:42 [in WiSE.symbolic.symex]
s:42 [in WiSE.implem.bugfinder_proof]
s:45 [in WiSE.symbolic.symex]
s:45 [in WiSE.implem.bugfinder_proof]
s:48 [in WiSE.lang.imp]
s:50 [in WiSE.symbolic.symex]
s:50 [in WiSE.streams]
s:52 [in WiSE.lang.imp]
s:55 [in WiSE.symbolic.symex]
s:55 [in WiSE.streams]
s:56 [in WiSE.lang.imp]
s:57 [in WiSE.implem.bugfinder_proof]
s:59 [in WiSE.symbolic.symex]
s:59 [in WiSE.implem.bugfinder_proof]
s:60 [in WiSE.implem.bugfinder_proof]
s:60 [in WiSE.lang.imp]
s:61 [in WiSE.streams]
s:63 [in WiSE.implem.bugfinder_proof]
s:64 [in WiSE.lang.imp]
s:69 [in WiSE.streams]
s:7 [in WiSE.symbolic.symex]
s:7 [in WiSE.streams]
s:70 [in WiSE.lang.imp]
s:71 [in WiSE.lang.imp]
s:72 [in WiSE.streams]
s:75 [in WiSE.lang.imp]
s:76 [in WiSE.streams]
s:80 [in WiSE.lang.imp]
s:81 [in WiSE.streams]
s:85 [in WiSE.streams]
s:85 [in WiSE.lang.imp]
s:89 [in WiSE.streams]
s:90 [in WiSE.lang.imp]
s:92 [in WiSE.streams]
s:95 [in WiSE.streams]
s:95 [in WiSE.lang.imp]
T
tasks:19 [in WiSE.implem.bugfinder]tasks:38 [in WiSE.implem.bugfinder_proof]
t:10 [in WiSE.implem.bugfinder_proof]
t:14 [in WiSE.implem.bugfinder_proof]
V
ve:103 [in WiSE.lang.imp]ve:34 [in WiSE.symbolic.symex]
ve:74 [in WiSE.lang.imp]
vx:35 [in WiSE.lang.imp]
vx:47 [in WiSE.lang.imp]
vx:63 [in WiSE.lang.imp]
vx:67 [in WiSE.lang.imp]
V0:141 [in WiSE.symbolic.symex]
V0:148 [in WiSE.symbolic.symex]
V0:159 [in WiSE.symbolic.symex]
V0:163 [in WiSE.symbolic.symex]
V0:188 [in WiSE.lang.imp]
V0:194 [in WiSE.lang.imp]
V:196 [in WiSE.lang.imp]
v:50 [in WiSE.lang.imp]
X
xs:13 [in WiSE.utils]xs:18 [in WiSE.utils]
xs:30 [in WiSE.streams]
xs:47 [in WiSE.streams]
xs:5 [in WiSE.streams]
x:1 [in WiSE.symbolic.symex]
x:101 [in WiSE.lang.imp]
x:102 [in WiSE.streams]
x:128 [in WiSE.lang.imp]
x:13 [in WiSE.relations]
x:14 [in WiSE.relations]
x:143 [in WiSE.streams]
x:145 [in WiSE.streams]
x:15 [in WiSE.lang.imprec]
x:157 [in WiSE.lang.imp]
x:17 [in WiSE.relations]
x:19 [in WiSE.lang.imprec]
x:23 [in WiSE.lang.imprec]
x:27 [in WiSE.symbolic.symex]
x:29 [in WiSE.lang.imprec]
x:29 [in WiSE.streams]
x:29 [in WiSE.lang.imp]
x:3 [in WiSE.lang.imprec]
x:3 [in WiSE.symbolic.symex]
x:32 [in WiSE.symbolic.symex]
x:32 [in WiSE.implem.bugfinder]
x:34 [in WiSE.implem.bugfinder]
x:34 [in WiSE.lang.imp]
x:4 [in WiSE.lang.imprec]
x:4 [in WiSE.streams]
x:41 [in WiSE.lang.imp]
x:46 [in WiSE.streams]
x:46 [in WiSE.lang.imp]
x:49 [in WiSE.lang.imp]
x:5 [in WiSE.relations]
x:54 [in WiSE.lang.imp]
x:58 [in WiSE.lang.imp]
x:6 [in WiSE.relations]
x:62 [in WiSE.lang.imp]
x:66 [in WiSE.lang.imp]
x:72 [in WiSE.lang.imp]
X:77 [in WiSE.symbolic.symex]
x:8 [in WiSE.symbolic.symex]
X:86 [in WiSE.symbolic.symex]
x:9 [in WiSE.relations]
x:96 [in WiSE.streams]
Y
y:10 [in WiSE.relations]y:15 [in WiSE.relations]
y:18 [in WiSE.relations]
y:5 [in WiSE.symbolic.symex]
y:51 [in WiSE.lang.imp]
y:6 [in WiSE.utils]
y:7 [in WiSE.relations]
Y:78 [in WiSE.symbolic.symex]
Y:87 [in WiSE.symbolic.symex]
Z
z:16 [in WiSE.relations]z:8 [in WiSE.relations]
other
π1:35 [in WiSE.symbolic.symex]π1:65 [in WiSE.symbolic.symex]
π1:70 [in WiSE.symbolic.symex]
π1:79 [in WiSE.symbolic.symex]
π1:90 [in WiSE.symbolic.symex]
π1:97 [in WiSE.symbolic.symex]
π2:36 [in WiSE.symbolic.symex]
π2:66 [in WiSE.symbolic.symex]
π2:73 [in WiSE.symbolic.symex]
π2:82 [in WiSE.symbolic.symex]
π2:91 [in WiSE.symbolic.symex]
π2:98 [in WiSE.symbolic.symex]
π:101 [in WiSE.symbolic.symex]
π:112 [in WiSE.symbolic.symex]
π:134 [in WiSE.symbolic.symex]
π:31 [in WiSE.symbolic.symex]
π:44 [in WiSE.symbolic.symex]
π:49 [in WiSE.symbolic.symex]
π:54 [in WiSE.symbolic.symex]
π:58 [in WiSE.symbolic.symex]
σ':142 [in WiSE.symbolic.symex]
σ':150 [in WiSE.symbolic.symex]
σ':162 [in WiSE.symbolic.symex]
σ':71 [in WiSE.implem.bugfinder_proof]
σ:139 [in WiSE.symbolic.symex]
σ:140 [in WiSE.symbolic.symex]
σ:144 [in WiSE.symbolic.symex]
σ:146 [in WiSE.symbolic.symex]
σ:149 [in WiSE.symbolic.symex]
σ:152 [in WiSE.symbolic.symex]
σ:154 [in WiSE.symbolic.symex]
σ:157 [in WiSE.symbolic.symex]
σ:160 [in WiSE.symbolic.symex]
σ:161 [in WiSE.symbolic.symex]
σ:183 [in WiSE.lang.imp]
σ:186 [in WiSE.lang.imp]
σ:187 [in WiSE.lang.imp]
σ:190 [in WiSE.lang.imp]
σ:192 [in WiSE.lang.imp]
σ:195 [in WiSE.lang.imp]
σ:72 [in WiSE.implem.bugfinder_proof]
σ:76 [in WiSE.implem.bugfinder_proof]
σ:80 [in WiSE.implem.bugfinder_proof]
Module Index
L
LTL [in WiSE.streams]Variable Index
S
Sequences.A [in WiSE.relations]Sequences.R [in WiSE.relations]
Library Index
B
bugfinderbugfinder_proof
E
equalitiesextract
I
impimprec
R
relationsS
solverstreams
symex
U
utilsConstructor Index
A
Add [in WiSE.lang.imprec]Add [in WiSE.lang.imp]
Aff [in WiSE.lang.imprec]
Aff [in WiSE.lang.imp]
B
Band [in WiSE.lang.imprec]Band [in WiSE.lang.imp]
Bcst [in WiSE.lang.imprec]
Bcst [in WiSE.lang.imp]
Beq [in WiSE.lang.imprec]
Beq [in WiSE.lang.imp]
Ble [in WiSE.lang.imprec]
Ble [in WiSE.lang.imp]
Bnot [in WiSE.lang.imprec]
Bnot [in WiSE.lang.imp]
BugFound [in WiSE.implem.bugfinder]
C
Cst [in WiSE.lang.imprec]Cst [in WiSE.lang.imp]
E
EQ [in WiSE.equalities]Err [in WiSE.lang.imprec]
Err [in WiSE.lang.imp]
error_Seq [in WiSE.lang.imp]
error_Err [in WiSE.lang.imp]
exec_loop_false [in WiSE.lang.imp]
exec_loop_true [in WiSE.lang.imp]
exec_Ite_false [in WiSE.lang.imp]
exec_Ite_true [in WiSE.lang.imp]
exec_Seq [in WiSE.lang.imp]
exec_Aff [in WiSE.lang.imp]
exec_Skip [in WiSE.lang.imp]
F
Finished [in WiSE.implem.bugfinder]G
Global [in WiSE.lang.imprec]I
Ite [in WiSE.lang.imprec]Ite [in WiSE.lang.imp]
L
Local [in WiSE.lang.imprec]Loop [in WiSE.lang.imprec]
Loop [in WiSE.lang.imp]
M
MAYBE [in WiSE.symbolic.solver]P
Pending [in WiSE.implem.bugfinder]S
SAT [in WiSE.symbolic.solver]scons [in WiSE.streams]
Seq [in WiSE.lang.imprec]
Seq [in WiSE.lang.imp]
Skip [in WiSE.lang.imprec]
Skip [in WiSE.lang.imp]
starr_step [in WiSE.relations]
starr_refl [in WiSE.relations]
star_step [in WiSE.relations]
star_refl [in WiSE.relations]
step_Loop_false [in WiSE.lang.imp]
step_Loop_true [in WiSE.lang.imp]
step_Ite_false [in WiSE.lang.imp]
step_Ite_true [in WiSE.lang.imp]
step_Seq_Skip [in WiSE.lang.imp]
step_Seq [in WiSE.lang.imp]
step_Aff [in WiSE.lang.imp]
Sub [in WiSE.lang.imprec]
Sub [in WiSE.lang.imp]
sym_step_Loop_false [in WiSE.symbolic.symex]
sym_step_Loop_true [in WiSE.symbolic.symex]
sym_step_Ite_false [in WiSE.symbolic.symex]
sym_step_Ite_true [in WiSE.symbolic.symex]
sym_step_Seq_Skip [in WiSE.symbolic.symex]
sym_step_Seq [in WiSE.symbolic.symex]
sym_step_Aff [in WiSE.symbolic.symex]
U
UNSAT [in WiSE.symbolic.solver]V
Var [in WiSE.lang.imprec]Var [in WiSE.lang.imp]
Lemma Index
A
aeq_spec [in WiSE.lang.imp]aeval_comp [in WiSE.symbolic.symex]
aeval_stable [in WiSE.lang.imp]
aeval_inst [in WiSE.lang.imp]
aeval_asubst [in WiSE.lang.imp]
asimp_correct [in WiSE.symbolic.solver]
B
BadInput_correct [in WiSE.symbolic.symex]beq_spec [in WiSE.lang.imp]
beval_comp [in WiSE.symbolic.symex]
beval_inst [in WiSE.lang.imp]
beval_bsubst [in WiSE.lang.imp]
bsimp_correct [in WiSE.symbolic.solver]
C
comp_update [in WiSE.symbolic.symex]comp_id [in WiSE.symbolic.symex]
E
error_state_error [in WiSE.lang.imp]error_state_seq [in WiSE.lang.imp]
exec_steps [in WiSE.lang.imp]
expand_inv [in WiSE.implem.bugfinder_proof]
expand_complete [in WiSE.implem.bugfinder_proof]
expand_sound [in WiSE.implem.bugfinder_proof]
F
find_bugs_complete [in WiSE.implem.bugfinder_proof]find_bugs_sound [in WiSE.implem.bugfinder_proof]
force_id [in WiSE.streams]
func_to_stream_correct [in WiSE.streams]
G
get_map [in WiSE.streams]get_filter [in WiSE.streams]
get_shift [in WiSE.streams]
H
HasBug_correct [in WiSE.symbolic.symex]I
IsBug_correct [in WiSE.symbolic.symex]is_error_Stuck [in WiSE.lang.imp]
is_error_correct [in WiSE.lang.imp]
L
LTL.globally_map [in WiSE.streams]LTL.shift_shift [in WiSE.streams]
M
map_eq [in WiSE.streams]map_in [in WiSE.implem.bugfinder_proof]
mk_not_correct [in WiSE.symbolic.solver]
mk_and_correct [in WiSE.symbolic.solver]
mk_sub_correct [in WiSE.symbolic.solver]
mk_add_correct [in WiSE.symbolic.solver]
P
progress_Loop [in WiSE.lang.imp]progress_Seq [in WiSE.lang.imp]
progress_Aff [in WiSE.lang.imp]
progress_Ite [in WiSE.lang.imp]
progress_Skip [in WiSE.lang.imp]
R
Reach_complete [in WiSE.symbolic.symex]Reach_sound [in WiSE.symbolic.symex]
relative_soundness [in WiSE.implem.bugfinder_proof]
relative_completeness [in WiSE.implem.bugfinder_proof]
run_finished [in WiSE.implem.bugfinder_proof]
run_finished_nil [in WiSE.implem.bugfinder_proof]
run_complete [in WiSE.implem.bugfinder_proof]
run_steps_complete [in WiSE.implem.bugfinder_proof]
run_here [in WiSE.implem.bugfinder_proof]
run_step_complete [in WiSE.implem.bugfinder_proof]
run_sound [in WiSE.implem.bugfinder_proof]
run_n_S_length [in WiSE.implem.bugfinder_proof]
run_n_length [in WiSE.implem.bugfinder_proof]
run_n_nil [in WiSE.implem.bugfinder_proof]
run_run_n [in WiSE.implem.bugfinder_proof]
run_nil [in WiSE.implem.bugfinder_proof]
run_eq [in WiSE.implem.bugfinder_proof]
S
shift_eq [in WiSE.streams]sim_init [in WiSE.symbolic.symex]
solver_correct [in WiSE.symbolic.solver]
sound_termination [in WiSE.implem.bugfinder_proof]
starr_star [in WiSE.relations]
star_simulation [in WiSE.relations]
star_one [in WiSE.relations]
steps_simulation_diagram [in WiSE.symbolic.symex]
steps_exec [in WiSE.lang.imp]
steps_seq [in WiSE.lang.imp]
step_simulation_diagram [in WiSE.symbolic.symex]
step_exec_exec [in WiSE.lang.imp]
stream_func_iso [in WiSE.streams]
symex_complete [in WiSE.symbolic.symex]
symex_sound [in WiSE.symbolic.symex]
sym_steps_steps [in WiSE.symbolic.symex]
sym_steps_steps_aux [in WiSE.symbolic.symex]
sym_steps_path [in WiSE.symbolic.symex]
sym_step_path [in WiSE.symbolic.symex]
sym_step_step [in WiSE.symbolic.symex]
Projection Index
B
body [in WiSE.lang.imprec]D
decls [in WiSE.lang.imprec]E
eq_op [in WiSE.equalities]H
Hlocals [in WiSE.lang.imprec]M
main [in WiSE.lang.imprec]P
params [in WiSE.lang.imprec]Inductive Index
A
aexpr [in WiSE.lang.imprec]aexpr [in WiSE.lang.imp]
B
bexpr [in WiSE.lang.imprec]bexpr [in WiSE.lang.imp]
E
error [in WiSE.lang.imp]exec [in WiSE.lang.imp]
I
IMP [in WiSE.lang.imp]S
sat [in WiSE.symbolic.solver]star [in WiSE.relations]
starr [in WiSE.relations]
status [in WiSE.implem.bugfinder]
step [in WiSE.lang.imp]
stmt [in WiSE.lang.imprec]
stream [in WiSE.streams]
sym_step [in WiSE.symbolic.symex]
V
variable [in WiSE.lang.imprec]Instance Index
F
fun_Eq [in WiSE.streams]S
starr_reflexive [in WiSE.relations]starr_trans [in WiSE.relations]
star_trans [in WiSE.relations]
star_reflexive [in WiSE.relations]
stream_Eq [in WiSE.streams]
Section Index
E
Examples [in WiSE.implem.bugfinder]Examples.Gcd [in WiSE.implem.bugfinder]
Examples.Simple [in WiSE.implem.bugfinder]
S
Sequences [in WiSE.relations]Simulation [in WiSE.relations]
Definition Index
A
a [in WiSE.implem.bugfinder]aeq [in WiSE.lang.imp]
aeval [in WiSE.lang.imprec]
aeval [in WiSE.lang.imp]
ainst [in WiSE.lang.imp]
all_some [in WiSE.utils]
alocals [in WiSE.lang.imprec]
asimp [in WiSE.symbolic.solver]
Assert [in WiSE.lang.imprec]
Assert [in WiSE.lang.imp]
asubst [in WiSE.lang.imp]
a0 [in WiSE.implem.bugfinder]
B
b [in WiSE.implem.bugfinder]BadInput [in WiSE.symbolic.symex]
BadInput [in WiSE.lang.imp]
beq [in WiSE.lang.imp]
beval [in WiSE.lang.imp]
bijection [in WiSE.equalities]
binst [in WiSE.lang.imp]
blocals [in WiSE.lang.imprec]
Bor [in WiSE.lang.imprec]
Bor [in WiSE.lang.imp]
bsimp [in WiSE.symbolic.solver]
bsubst [in WiSE.lang.imp]
bug [in WiSE.lang.imp]
bug_found [in WiSE.implem.bugfinder_proof]
b0 [in WiSE.implem.bugfinder]
C
comp [in WiSE.symbolic.symex]complete_bug_finding [in WiSE.symbolic.symex]
Concrete [in WiSE.symbolic.symex]
D
display [in WiSE.implem.bugfinder]done [in WiSE.implem.bugfinder_proof]
E
enum [in WiSE.streams]enum_equ [in WiSE.streams]
error_state [in WiSE.lang.imp]
eventually [in WiSE.streams]
execute_gcd_err [in WiSE.implem.bugfinder]
execute_gcd_noerr [in WiSE.implem.bugfinder]
execute_gcd [in WiSE.implem.bugfinder]
expand [in WiSE.implem.bugfinder]
F
filter [in WiSE.streams]find_bugs_assuming [in WiSE.implem.bugfinder]
find_bugs [in WiSE.implem.bugfinder]
first [in WiSE.utils]
force [in WiSE.streams]
func_to_stream [in WiSE.streams]
G
gcd [in WiSE.implem.bugfinder]gcd_buggy [in WiSE.implem.bugfinder]
gcd_assertions [in WiSE.implem.bugfinder]
get [in WiSE.streams]
globally [in WiSE.streams]
global_store [in WiSE.lang.imprec]
H
HasBug [in WiSE.symbolic.symex]HasBug [in WiSE.lang.imp]
here [in WiSE.implem.bugfinder_proof]
I
id [in WiSE.symbolic.symex]ident [in WiSE.lang.imprec]
ident [in WiSE.lang.imp]
init [in WiSE.implem.bugfinder]
init_store' [in WiSE.implem.bugfinder]
init_store [in WiSE.implem.bugfinder]
init_assuming [in WiSE.implem.bugfinder]
IsBug [in WiSE.symbolic.symex]
IsBug [in WiSE.lang.imp]
isomorph [in WiSE.equalities]
is_sat [in WiSE.symbolic.solver]
is_skip [in WiSE.lang.imp]
is_error [in WiSE.lang.imp]
L
locals [in WiSE.lang.imprec]local_store [in WiSE.lang.imprec]
LTL.and [in WiSE.streams]
LTL.eventually [in WiSE.streams]
LTL.globally [in WiSE.streams]
LTL.imp [in WiSE.streams]
LTL.model [in WiSE.streams]
LTL.next [in WiSE.streams]
LTL.not [in WiSE.streams]
LTL.now [in WiSE.streams]
LTL.or [in WiSE.streams]
LTL.t [in WiSE.streams]
M
map [in WiSE.streams]map_opt [in WiSE.utils]
mk_not [in WiSE.symbolic.solver]
mk_and [in WiSE.symbolic.solver]
mk_sub [in WiSE.symbolic.solver]
mk_add [in WiSE.symbolic.solver]
my_prog [in WiSE.implem.bugfinder]
N
none [in WiSE.implem.bugfinder_proof]now [in WiSE.streams]
P
peek [in WiSE.streams]potential_bug [in WiSE.symbolic.symex]
potential_bug [in WiSE.implem.bugfinder_proof]
progress [in WiSE.lang.imp]
R
Reach [in WiSE.symbolic.symex]Reach [in WiSE.lang.imp]
reachable_from [in WiSE.implem.bugfinder_proof]
reduce [in WiSE.utils]
relatively_sound_bug_finding [in WiSE.symbolic.symex]
run [in WiSE.implem.bugfinder]
run_n [in WiSE.implem.bugfinder]
S
shift [in WiSE.streams]sim [in WiSE.symbolic.symex]
simulation [in WiSE.relations]
solver [in WiSE.symbolic.solver]
steps [in WiSE.lang.imp]
store [in WiSE.lang.imp]
stream_equ [in WiSE.streams]
Stuck [in WiSE.lang.imp]
Symbolic [in WiSE.implem.bugfinder_proof]
sym_steps [in WiSE.symbolic.symex]
sym_state [in WiSE.symbolic.symex]
sym_beval [in WiSE.symbolic.symex]
sym_aeval [in WiSE.symbolic.symex]
sym_update [in WiSE.symbolic.symex]
sym_store [in WiSE.symbolic.symex]
T
tasks [in WiSE.implem.bugfinder]then_do [in WiSE.implem.bugfinder]
trivial_assertion [in WiSE.implem.bugfinder]
U
untill [in WiSE.streams]update [in WiSE.lang.imp]
V
ValidBug [in WiSE.implem.bugfinder_proof]ValidStatus [in WiSE.implem.bugfinder_proof]
Record Index
D
declaration [in WiSE.lang.imprec]E
Eq [in WiSE.equalities]I
IMPREC [in WiSE.lang.imprec]| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (986 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (17 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (649 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (11 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (67 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (81 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (16 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (122 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |