<div dir="ltr">On Fri, Mar 18, 2016 at 12:18 AM, Jonathan Thornburg <span dir="ltr"><<a href="mailto:jthorn@astro.indiana.edu" target="_blank">jthorn@astro.indiana.edu</a>></span> wrote:<br><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Indeed, it would seem to provide an interesting vehicle for producing<br>
a formally-verified TCP/IP stack.  Has anyone tried this?<br>
<div class="HOEnZb"><div class="h5"></div></div></blockquote></div><div class="gmail_signature"><div dir="ltr"><br></div><div>To do a DSL for producing a formally-verified TCP/IP stack might be a bit of overkill. For example, "a friend of mine" have done this with severely ACSL-annotated C code and Frama-C couple years ago.</div><div><br></div><div>Ilya </div><div dir="ltr"><br></div></div>
</div></div>