blob: 9752273958807e1ac9d51b03aeef2829d13d3271 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
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
|
