diff options
Diffstat (limited to 'content/zettel/3a7.md')
| -rw-r--r-- | content/zettel/3a7.md | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/content/zettel/3a7.md b/content/zettel/3a7.md new file mode 100644 index 0000000..9752273 --- /dev/null +++ b/content/zettel/3a7.md @@ -0,0 +1,27 @@ ++++ +title = "Translation validation" +author = "Yann Herklotz" +tags = [] +categories = [] +backlinks = ["3c3", "3a6", "2e1d2", "2e1c6", "1f4a"] +forwardlinks = ["2e1c1", "3a8", "3a7a"] +zettelid = "3a7" ++++ + +Translation validation is a proof technique whereby one can perform an +unverified translation and verify that the results match after the +translation using a verified validator. This gives exactly the same +guarantees as normal verification for a verified compiler, for example, +because the compiler is allowed to fail. The correctness proofs only +need to hold if the compiler succeeds. + +This means that a proven validator which errors out if it cannot prove +the equivalence between the input and output of the verified pass also +allows for a verified pass. One therefore has to show that if the +verified validator says that the input and output are equivalent, that +the semantics of the input and output are as well. + +Translation validation is often performed by using symbolic execution +([\#2e1c1]). + + [\#2e1c1]: /zettel/2e1c1 |