Mon 17 Jan 2022 10:50 - 11:20 at Salon I - Model Checking Chair(s): Arie Gurfinkel

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.

Mon 17 Jan

Displayed time zone: Eastern Time (US & Canada) change

10:20 - 11:50
Model CheckingVMCAI at Salon I
Chair(s): Arie Gurfinkel University of Waterloo
10:20
30m
Paper
Automata-Driven Partial Order Reduction and Guided Search for LTL Model CheckingRemote
VMCAI
Peter Gjøl Jensen Aalborg University, Denmark, Jiri Srba Aalborg University, Nikolaj Jensen Ulrik Aalborg University, Simon Mejlby Virenfeldt Aalborg University
10:50
30m
Paper
Stateful Dynamic Partial Order Reduction for Model Checking Event-Driven Applications that Do Not TerminateRemote
VMCAI
Rahmadi Trimananda University of California at Irvine, USA, Weiyu Luo University of California, Irvine, Brian Demsky University of California at Irvine, Harry Xu University of California, Los Angeles (UCLA)
Link to publication DOI Pre-print Media Attached File Attached
11:20
30m
Paper
Scaling Up Livelock Verification for Network-on-Chip Routing AlgorithmsInPerson
VMCAI
Landon Taylor Utah State University, Zhen Zhang Utah State University