blob: 06a4bd87d1e3a3d51d05a02fcbdea7de56b6097b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
+++
title = "Proof of CompCertGSA"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a8g4", "2e1c6a"]
forwardlinks = ["3a8g5a"]
zettelid = "3a8g5"
+++
The proof of CompCertGSA is quite complicated, especially the proof of
the correctness of the predicates. The predicates are generated using
path expressions, so the proof of correctness of the translation
requires a proof of correctness of the path expressions, of which there
can be various different forms.
|
