P is a state machine based programming language for formally modeling and specifying complex distributed systems. P allows programmers to model their system design 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. P is a programming language for asynchronous event-driven programming and the IoT that was developed by Microsoft and University of California, Berkeley The P language is carefully designed so that we can check if the systems being designed is responsive, i.e., it is able to handle every event in a timely manner. By default, a machine needs to handle every event that arrives in every state. The default safety checker looks for violations of this rule. Sometimes, handling every event at every state is impractical. The language provides a notion of deferred events where the programmer can annotate when she wants to delay processing an event. The language also provides default liveness checks that an event cannot be potentially deferred forever. Call transitions (which are like subroutines) are used to factor common event handling code, and allow programmers to write complicated state machines. P was used to implement and verify the core of the USB device driver stack that ships with Microsoft Windows 8. The resulting driver is more reliable and performs better than its prior incarnation (which did not use P), and we have more confidence in the robustness of its design due to the language abstractions and verification provided by P. P: a domain specific language for writing asynchronous event-driven programs. This asynchronous language promotes a discipline of programming where deferrals need to be declared explicitly, and consequently leads to responsive systems. The main technical contribution of this work is an asynchronous model which forces each event in the queue to be handled as soon as the machine associated with the queue is scheduled, and has a chance to de-queue the event. The system's verifier systematically explores the state space of machines and ensures that there are no unhandled events. In certain circumstances, such as processing a high priority event, or processing a sequence of event exchanges during a transaction, some other lower priority events may have to be queued temporarily. P has features such as deferred events for a programmer to explicitly specify such deferrals.