---
res:
  bibo_abstract:
  - We describe the design and implementation of P, a domain-specific language to
    write asynchronous event driven code. P allows the programmer to specify the system
    as a collection of interacting state machines, which communicate with each other
    using events. P unifies modeling and programming into one activity for the programmer.
    Not only can a P program be compiled into executable code, but it can also be
    tested using model checking techniques. P allows the programmer to specify the
    environment, used to "close" the system during testing, as nondeterministic
    ghost machines. Ghost machines are erased during compilation to executable code;
    a type system ensures that the erasure is semantics preserving. The P language
    is designed so that a P program can be checked for responsiveness-the ability
    to handle every event in a timely manner. By default, a machine needs to handle
    every event that arrives in every state. But handling every event in 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 default safety checker
    looks for presence of unhan-dled events. The language also provides default liveness
    checks that an event cannot be potentially deferred forever. 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); we have more confidence in the robustness of its design
    due to the language abstractions and verification provided by P.@eng
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Ankush
      foaf_name: Desai, Ankush
      foaf_surname: Desai
  - foaf_Person:
      foaf_givenName: Vivek
      foaf_name: Gupta, Vivek
      foaf_surname: Gupta
  - foaf_Person:
      foaf_givenName: Ethan
      foaf_name: Jackson, Ethan
      foaf_surname: Jackson
  - foaf_Person:
      foaf_givenName: Shaz
      foaf_name: Qadeer, Shaz
      foaf_surname: Qadeer
  - foaf_Person:
      foaf_givenName: Sriram
      foaf_name: Rajamani, Sriram
      foaf_surname: Rajamani
  - foaf_Person:
      foaf_givenName: Damien
      foaf_name: Zufferey, Damien
      foaf_surname: Zufferey
      foaf_workInfoHomepage: http://www.librecat.org/personId=4397AC76-F248-11E8-B48F-1D18A9856A87
    orcid: 0000-0002-3197-8736
  bibo_doi: 10.1145/2491956.2462184
  dct_date: 2013^xs_gYear
  dct_language: eng
  dct_publisher: ACM@
  dct_title: 'P: Safe asynchronous event-driven programming@'
...