[P4] Fwd: [P4-design] P4 Formal semantics?

[Sándor Laki]

FYI



-------- Forwarded Message --------
Subject: 	[P4-design] P4 Formal semantics?
Date: 	Mon, 17 Oct 2016 21:30:05 +0000
From: 	Rosu, Grigore <grosu at illinois.edu>
To: 	p4-design at lists.p4.org <p4-design at lists.p4.org>



Dear P4 Designers,

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 (http://kframework.org), 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: http://fsl.cs.illinois.edu/index.php/Programming_Language_Design_and_Semantics.

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.

Best,
Grigore



---
Ezt az e-mailt az Avast víruskereső szoftver átvizsgálta.
https://www.avast.com/antivirus
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://plc.inf.elte.hu/pipermail/p4/attachments/20161018/c26fab09/attachment.html>
-------------- next part --------------
_______________________________________________
P4-design mailing list
P4-design at lists.p4.org
http://lists.p4.org/mailman/listinfo/p4-design_lists.p4.org