[P4-design] P4 Formal semantics?
mbudiu at vmware.com
Mon Oct 17 18:42:51 EDT 2016
I think it's a great idea. I would encourage this effort for the P4-16 language version.
I personally don't have too many free cycles, but I hope that as the spec work (and associated reference compiler implementation) wind down I will be able to create more free cycles. I certainly could contribute a relatively small number of cycles.
From: P4-design [mailto:p4-design-bounces at lists.p4.org] On Behalf Of Rosu, Grigore
Sent: Monday, October 17, 2016 2:30 PM
To: p4-design at lists.p4.org
Subject: [P4-design] P4 Formal semantics?
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.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the P4-design