Regression Verification for Multi-Threaded Programs
Sagar
Chaki, Arie Gurfinkel, Ofer Strichman,
Proceedings of the 13th International Conference on
Verification, Model Checking and Abstract Interpretation (VMCAI), page
119-135, January 22--24, 2012.
Abstract:
Regression verification is the problem of deciding whether two similar
programs are equivalent under an arbitrary yet equal context, given
some definition of equivalence. So far this problem has only been
studied for the case of single-threaded deterministic programs. We
present a method for regression verification to establish partial
equivalence (i.e., input/output equivalence of terminating executions)
of multi-threaded programs. Specifically, we develop two proof-rules
that decompose the regression verification between concurrent
programs to that of regression verification between \emph{sequential}
functions, a more tractable problem. This ability to avoid composing
threads altogether when discharging premises, in a fully automatic way
and for general programs, uniquely distinguishes our proof rules from
others used for classical verification of concurrent programs.
Online