From 583e1c9f5cb043ef093cdd255396706161a9e30b Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 17 Nov 2020 16:40:48 +0000 Subject: Add more proof section --- archive/introduction.tex | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'archive') diff --git a/archive/introduction.tex b/archive/introduction.tex index 4b041f2..172309d 100644 --- a/archive/introduction.tex +++ b/archive/introduction.tex @@ -1 +1,5 @@ + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + First of all, most of the compiler passes in \compcert{} have been proven correct, meaning that once the compiler is built, the proofs can be erased as the algorithm has been shown to be correct independent of the input. However, some optimisation passes such as software pipelining require translation validation~\cite{tristan08_formal_verif_trans_valid}, in which case the correctness of the compiler pass needs to be checked at runtime. However, even in this case the verifier itself is proven to only verify code correct that does indeed behave in the same way. -- cgit