[P4-design] P4 Formal semantics?
grosu at illinois.edu
Tue Oct 18 19:53:02 EDT 2016
Many thanks for the positive feedback, Nick (and others who responded privately). I am not familiar enough with P4 myself, but my student started looking into and I will learn it by following his progress. Basically all we needed to know was that if ask questions like "what is the meaning of this?" or "is this well-defined or not?" then we get some answers relatively quickly, so we can move on. Now we know there is interest, so we will go ahead with it. If anybody else is interested to stay in the loop, please let us know in private, to minimize spam.
From: Nick McKeown [nickm at stanford.edu]
Sent: Monday, October 17, 2016 10:52 PM
To: Rosu, Grigore; p4-design at lists.p4.org
Subject: Re: [P4-design] P4 Formal semantics?
Grigore - this is a really awesome proposal :) Personally, I'd love to see this happen. Let's explore to see how this would work. Are you familiar enough with P4 already to feel comfortable this is doable? What kind of support will you need from this group (or the community at large)?
On 10/17/16 2:30 PM, Rosu, Grigore wrote:
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.
P4-design mailing list
P4-design at lists.p4.org<mailto:P4-design at lists.p4.org>
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the P4-design