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 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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Full version at ie.technion.ac.il/~ofers/publications/vmcai12_full.pdf
Cobleigh, J.M., Giannakopoulou, D., Păsăreanu, C.S.: Learning Assumptions for Compositional Verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 331–346. Springer, Heidelberg (2003)
Godlin, B.: Regression verification: Theoretical and implementation aspects. Master’s thesis, Technion, Israel Institute of Technology (2008)
Godlin, B., Strichman, O.: Inference rules for proving the equivalence of recursive procedures. Acta Informatica 45(6), 403–439 (2008)
Godlin, B., Strichman, O.: Regression verification. In: 46th Design Automation Conference, DAC (2009)
Gupta, A., Popeea, C., Rybalchenko, A.: Threader: A Constraint-Based Verifier for Multi-threaded Programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 412–417. Springer, Heidelberg (2011)
Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596–619 (1983)
Kaser, O., Ramakrishnan, C.R., Pawagi, S.: On the conversion of indirect to direct recursion. LOPLAS 2(1-4), 151–164 (1993)
Kawaguchi, M., Lahiri, S.K., Rebelo, H.: Conditional equivalence. Technical Report MSR-TR-2010-119, Microsoft Research (2010)
Lee, E.A.: The problem with threads. IEEE Computer 39(5), 33–42 (2006)
Owicki, S.S., Gries, D.: An Axiomatic Proof Technique for Parallel Programs I. Acta Inf. 6, 319–340 (1976)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chaki, S., Gurfinkel, A., Strichman, O. (2012). Regression Verification for Multi-threaded Programs. In: Kuncak, V., Rybalchenko, A. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2012. Lecture Notes in Computer Science, vol 7148. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-27940-9_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-27940-9_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-27939-3
Online ISBN: 978-3-642-27940-9
eBook Packages: Computer ScienceComputer Science (R0)