+++
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