blob: 00f58163ab0ba6ef1d94f66f4fdb1c459177b43e (
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
28
29
30
31
32
33
|
+++
title = "How to solve this specification problem"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["1f2"]
forwardlinks = ["3a"]
zettelid = "1f2a"
+++
This specification problem can be solved informally, by basing the HLS
tool on the C semantics of existing compilers that have been well-tested
and are well-understood. One example of such a compiler is CompCert
([\#3a]), which has a formal specification of Clight \[1\] language,
which defines a subset of C that is formally verified.
<div id="refs" class="references csl-bib-body" markdown="1">
<div id="ref-blazy09_mechan_seman_cligh_subset_c_languag"
class="csl-entry" markdown="1">
<span class="csl-left-margin">\[1\]
</span><span class="csl-right-inline">S. Blazy and X. Leroy, “Mechanized
semantics for the Clight subset of the C language,” *Journal of
Automated Reasoning*, vol. 43, no. 3, pp. 263–288, Oct. 2009, doi:
[10.1007/s10817-009-9148-3].</span>
</div>
</div>
[\#3a]: /zettel/3a
[10.1007/s10817-009-9148-3]: https://doi.org/10.1007/s10817-009-9148-3
|
