Strand: A logic combining heap structures and data


Program
 Verification
condition
 Structural solving (MONA)
 Data-constraint solving (Z3 with QF-LIA)
finitely-many
minimal models ?
 #States
 Final
BDD size
 Time (s)
 Graph model
exists?
 Bound
(#Nodes)
 Formula size
(KB)
 Satisfiable?
 Time (s)
sorted-list-search
 before-loop
 Yes
 67
 264
 0.34
 No
 -
 -
 -
 -
in-loop
 Yes
 131
 585
 0.59
 No
 -
 -
 -
 -
after-loop
 Yes
 67
 264
 0.18
 No
 -
 -
 -
 -
sorted-list-insert
 before-head
 Yes
 73
 298
 1.66
 Yes
 5
 6.2
 No
 0.02
before-loop
 Yes
 259
 1290
 0.38
 No
 -
 -
 -
 -
in-loop
 Yes
 1027
 6156
 4.46
 No
 -
 -
 -
 -
after-loop
 Yes
 146
 680
 13.93
 Yes
 7
 14.5
 No
 0.02
sorted-list-insert-error
 before-loop
 Yes
 298
 1519
 0.34
 Yes
 7
 9.5
 Yes
 0.02
sorted-list-reverse before-loop
 Yes
 35
 119
 0.24
 No
 -
 -
 -
 -
in-loop
 Yes
 513
 2816
 2.79
 No
 -
 -
 -
 -
after-loop
 Yes
 129
 576
 0.35
 No
 -
 -
 -
 -
bst-search before-loop
 Yes
 52
 276
 5.03
 No
 -
 -
 -
 -
in-loop
 Yes
 160
 1132
 32.80
 Yes
 9
 7.7
 No
 0.02
after-loop
 Yes
 52
 276
 3.27
 No
 -
 -
 -
 -
bst-insert
 before-loop
 Yes
 36
 196
 1.34
 No
 -
 -
 -
 -
in-loop
 Yes
 68
 452
 9.84
 No
 -
 -
 -
 -
after-loop
 Yes
 20
 84
 1.76
 No
 -
 -
 -
 -