P 1.1.4

P is a state machine based programming language for modeling and specifying complex distributed systems. P allows programmers to model their system as a collection of communicating state machines. P supports several backend analysis engines (based on automated reasoning techniques like model checking and symbolic execution) to check that the distributed system modeled in P satisfy the desired correctness specifications. Not only can a P program be systematically tested (e.g., model checking), but it can also be compiled into executable code. Essentially, P unifies modeling, specifying, implementing, and testing into one activity for the programmer.

P is currently being used extensively inside Amazon (AWS) for analysis of complex distributed systems. P is also being used for programming safe robotics systems. P was first used to implement and validate the USB device driver stack that ships with Microsoft Windows 8 and Windows Phone.

✨ Programming concurrent, distributed systems is fun but challenging, however, a pinch of programming language design with a dash of automated reasoning can go a long way in addressing the challenge and amplify the fun!. ✨

Let the fun begin!

You can find most of the information about the P framework on: http://p-org.github.io/P/.

What is P?, Getting Started, Tutorials, Case Studies and related Research Publications. If you have any further questions, please feel free to create an issue, ask on discussions, or email us

P has always been a collaborative project between industry and academia (since 2013) 🥁. The P team welcomes contributions and suggestions from all of you!! 👊. See CONTRIBUTING for more information.