On the complexity of bidirected interleaved Dyck-reachability

Abstract

Many program analyses need to reason about pairs of matching actions, such as call/return, lock/unlock, or set-field/get-field. The family of Dyck languages { D k }, where D k has k kinds of parenthesis pairs, can be used to model matching actions as balanced parentheses. Consequently, many program-analysis problems can be formulated as Dyck-reachability problems on edge-labeled digraphs. Interleaved Dyck-reachability (InterDyck-reachability), denoted by D k ⊙ D k -reachability, is a natural extension of Dyck-reachability that allows one to formulate program-analysis problems that involve multiple kinds of matching-action pairs. Unfortunately, the general InterDyck-reachability problem is undecidable.

Document Details

Document Type
Pub Defense Publication
Publication Date
Jan 04, 2021
Source ID
10.1145/3434340

Entities

People

  • Qirun Zhang
  • Thomas Reps
  • Yuanbo Li

Organizations

  • Georgia Tech
  • National Science Foundation
  • Office of Naval Research
  • University of Wisconsin–Madison

Tags

Readers

  • Electrical Engineering
  • Mathematical Modeling and Probability Theory.