Parameterized Complexity of Program Verification Tasks

Program verification is hard. Decision problems arising from verification tasks usually do not admit satisfying worst-case complexities. On the other hand, program verification can be efficient. Verification tools developed in recent years perform well even on large systems. To resolve this discrepancy between theory and practice, we picked up a recent trend in complexity theory: Parameterized Complexity. Unlike classical complexity theory that relates the complexity to the size of the instance, Parameterized Complexity measures the influence of several parameters on a problem’s complexity. This offers a more fine-grained view. We can separate those parameters of a problem that allow for the construction of efficient algorithms from those that cause the hardness. We conducted parameterized complexity analyses of typical verification tasks. The main findings are as follows. (1) A new algorithm (ESA’17) for Bounded Context Switching, non-polynomial only in the number of context switches and the size of the memory. (2) Two new algorithms (TACAS’18) for safety verification in the parameterized Leader-Contributor model (LCM). This includes an algorithm running in time single-exponential in the size of the contributors. (3) Two new algorithms (submitted) for liveness verification in LCM, showing that checking safety and liveness only differ by a polynomial factor. (4) A new polynomial-time algorithm (NETYS’19) for liveness in broadcast networks. To obtain these upper bounds, we employ techniques from both fields, Parameterized Complexity and verification. Further, we show that the given algorithms are optimal: the verification tasks cannot be solved more efficient unless the Exponential Time Hypothesis fails, a standard assumption in Parameterized Complexity.

Authors

• Peter Chini
• Roland Meyer
• Prakash Saivasan.

Keywords

No keywords are indexed for this paper.