  Event-driven architectures are broadly used for systems that must respond to
events in the real world. Event-driven applications are prone to concurrency
bugs that involve subtle errors in reasoning about the ordering of events.
Unfortunately, there are several challenges in using existing model-checking
techniques on these systems. Event-driven applications often loop indefinitely
and thus pose a challenge for stateless model checking techniques. On the other
hand, deploying purely stateful model checking can explore large sets of
equivalent executions.
  In this work, we explore a new technique that combines dynamic partial order
reduction with stateful model checking to support non-terminating applications.
Our work is (1) the first dynamic partial order reduction algorithm for
stateful model checking that is sound for non-terminating applications and (2)
the first dynamic partial reduction algorithm for stateful model checking of
event-driven applications. We experimented with the IoTCheck dataset: a study
of interactions in smart home app pairs. This dataset consists of app pairs
originated from 198 real-world smart home apps. Overall, our DPOR algorithm
successfully reduced the search space for the app pairs, enabling 69 pairs of
apps that did not finish without DPOR to finish and providing a 7X average
speedup.
