islet-project
diff --git a/‎doc/islet-model-checking.md
Lines changed: 442 additions & 0 deletions b/‎doc/islet-model-checking.md
Lines changed: 442 additions & 0 deletions
diff --git a/‎doc/res/model-checking/delegate_results.png
111 KB b/‎doc/res/model-checking/delegate_results.png
111 KB
diff --git a/‎doc/res/model-checking/el3_modeling1.png
70.9 KB b/‎doc/res/model-checking/el3_modeling1.png
70.9 KB
diff --git a/‎doc/res/model-checking/el3_modeling2.png
112 KB b/‎doc/res/model-checking/el3_modeling2.png
112 KB
diff --git a/‎doc/res/model-checking/features_code.png
60.6 KB b/‎doc/res/model-checking/features_code.png
60.6 KB
diff --git a/‎doc/res/model-checking/features_results.png
116 KB b/‎doc/res/model-checking/features_results.png
116 KB
diff --git a/‎doc/res/model-checking/features_spec_failure.png
22.7 KB b/‎doc/res/model-checking/features_spec_failure.png
22.7 KB
diff --git a/‎doc/res/model-checking/granule_invariant.png
54.8 KB b/‎doc/res/model-checking/granule_invariant.png
54.8 KB
diff --git a/‎doc/res/model-checking/host_mem_modeling1.png
120 KB b/‎doc/res/model-checking/host_mem_modeling1.png
120 KB
diff --git a/‎doc/res/model-checking/host_mem_modeling2.png
120 KB b/‎doc/res/model-checking/host_mem_modeling2.png
120 KB
diff --git a/‎doc/res/model-checking/islet-features-harness.png
108 KB b/‎doc/res/model-checking/islet-features-harness.png
108 KB
diff --git a/‎doc/res/model-checking/tf-rmm-features-harness.png
130 KB b/‎doc/res/model-checking/tf-rmm-features-harness.png
130 KB
diff --git a/‎doc/res/model-checking/tfrmm_undelegate_harness.png
124 KB b/‎doc/res/model-checking/tfrmm_undelegate_harness.png
124 KB
diff --git a/‎doc/res/model-checking/undelegate_code.png
44.4 KB b/‎doc/res/model-checking/undelegate_code.png
44.4 KB
diff --git a/‎doc/res/model-checking/undelegate_harness.png
113 KB b/‎doc/res/model-checking/undelegate_harness.png
113 KB
diff --git a/‎doc/res/model-checking/undelegate_results.png
103 KB b/‎doc/res/model-checking/undelegate_results.png
103 KB
diff --git a/‎doc/res/model-checking/undelegate_spec_success.png
27.4 KB b/‎doc/res/model-checking/undelegate_spec_success.png
27.4 KB