<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
</head>
<body bgcolor="#FFFFFF" text="#000000">
<p>FYI<br>
</p>
<div class="moz-forward-container"><br>
<br>
-------- Forwarded Message --------
<table class="moz-email-headers-table" border="0" cellpadding="0"
cellspacing="0">
<tbody>
<tr>
<th align="RIGHT" nowrap="nowrap" valign="BASELINE">Subject:
</th>
<td>[P4-design] P4 Formal semantics?</td>
</tr>
<tr>
<th align="RIGHT" nowrap="nowrap" valign="BASELINE">Date: </th>
<td>Mon, 17 Oct 2016 21:30:05 +0000</td>
</tr>
<tr>
<th align="RIGHT" nowrap="nowrap" valign="BASELINE">From: </th>
<td>Rosu, Grigore <a class="moz-txt-link-rfc2396E" href="mailto:grosu@illinois.edu"><grosu@illinois.edu></a></td>
</tr>
<tr>
<th align="RIGHT" nowrap="nowrap" valign="BASELINE">To: </th>
<td><a class="moz-txt-link-abbreviated" href="mailto:p4-design@lists.p4.org">p4-design@lists.p4.org</a> <a class="moz-txt-link-rfc2396E" href="mailto:p4-design@lists.p4.org"><p4-design@lists.p4.org></a></td>
</tr>
</tbody>
</table>
<br>
<br>
<meta http-equiv="Content-Type" content="text/html;
charset=windows-1252">
<style type="text/css" id="owaParaStyle"></style>
<div style="direction: ltr;font-family: Times New Roman;color:
#000000;font-size: 12pt;">
Dear P4 Designers,
<div><br>
</div>
<div>I have a PhD student who is looking for a topic and, after
some discussion with Nikolaj Bjorner, we think that defining a
formal semantics to P4 could be a timely and useful project.
Note that we would do it using the K framework
(<a class="moz-txt-link-freetext" href="http://kframework.org">http://kframework.org</a>), so the semantics would immediately
yield a series of formal analysis tools for P4, such as
simulator/interpreter, symbolic execution, bounded model
checking, symbolic model checking, and even a deductive
verifier. Our overall paradigm is explained on this
wikipage: <a class="moz-txt-link-freetext" href="http://fsl.cs.illinois.edu/index.php/Programming_Language_Design_and_Semantics">http://fsl.cs.illinois.edu/index.php/Programming_Language_Design_and_Semantics</a>.<br>
<div><br>
</div>
<div>The main question right now is whether you think this is
a worthwhile thing to do right now, or we should better wait
a bit longer until things stabilize. On the other hand,
note that giving a formal semantics in K is a rather
lightweight process, nothing comparable with doing the same
thing in Coq or Isabelle (for example, it took only 4 months
to define the K semantics of JavaScript ES5), so it can be
used as an active means to even design P4 itself. So in
case we go ahead with it, it would be great if some of you
would like to get involved as well, to make sure we stay on
the right track. My student would do most of the K
"coding", but you and I would supervise him to make sure he
is doing the right thing right.</div>
<div><br>
</div>
<div>Best,<br>
<div style="font-family:Tahoma; font-size:13px">
<div><font face="Times New Roman" size="3">Grigore</font></div>
<div><br>
</div>
</div>
</div>
<div style="font-family: Times New Roman; color: #000000;
font-size: 16px">
<div>
<div>
</div>
</div>
</div>
</div>
<style type="text/css" style="">
<!--
p
{margin-top:0;
margin-bottom:0}
-->
</style></div>
</div>
<br /><br />
<hr style='border:none; color:#909090; background-color:#B0B0B0; height: 1px; width: 99%;' />
<table style='border-collapse:collapse;border:none;'>
<tr>
<td style='border:none;padding:0px 15px 0px 8px'>
<a href="https://www.avast.com/antivirus">
<img border=0 src="http://static.avast.com/emails/avast-mail-stamp.png" alt="Avast logo" />
</a>
</td>
<td>
<p style='color:#3d4d5a; font-family:"Calibri","Verdana","Arial","Helvetica"; font-size:12pt;'>
Ezt az e-mailt az Avast víruskereső szoftver átvizsgálta.
<br><a href="https://www.avast.com/antivirus">www.avast.com</a>
</p>
</td>
</tr>
</table>
<br />
</body>
</html>