×

zbMATH — the first resource for mathematics

Regression verification for multi-threaded programs. (English) Zbl 1325.68060
Kuncak, Viktor (ed.) et al., Verification, model checking, and abstract interpretation. 13th international conference, VMCAI 2012, Philadelphia, PA, USA, January 22–24, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-27939-3/pbk). Lecture Notes in Computer Science 7148, 119-135 (2012).
Summary: 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.
For the entire collection see [Zbl 1236.68007].

MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
Threader
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Full version at ie.technion.ac.il/ ofers/publications/vmcai12_full.pdf
[2] 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) · Zbl 1031.68545 · doi:10.1007/3-540-36577-X_24
[3] Godlin, B.: Regression verification: Theoretical and implementation aspects. Master’s thesis, Technion, Israel Institute of Technology (2008)
[4] Godlin, B., Strichman, O.: Inference rules for proving the equivalence of recursive procedures. Acta Informatica 45(6), 403–439 (2008) · Zbl 1161.68013 · doi:10.1007/s00236-008-0075-2
[5] Godlin, B., Strichman, O.: Regression verification. In: 46th Design Automation Conference, DAC (2009) · doi:10.1145/1629911.1630034
[6] 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) · Zbl 05940730 · doi:10.1007/978-3-642-22110-1_32
[7] Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596–619 (1983) · Zbl 0517.68032 · doi:10.1145/69575.69577
[8] Kaser, O., Ramakrishnan, C.R., Pawagi, S.: On the conversion of indirect to direct recursion. LOPLAS 2(1-4), 151–164 (1993) · doi:10.1145/176454.176510
[9] Kawaguchi, M., Lahiri, S.K., Rebelo, H.: Conditional equivalence. Technical Report MSR-TR-2010-119, Microsoft Research (2010)
[10] Lee, E.A.: The problem with threads. IEEE Computer 39(5), 33–42 (2006) · Zbl 05088711 · doi:10.1109/MC.2006.180
[11] Owicki, S.S., Gries, D.: An Axiomatic Proof Technique for Parallel Programs I. Acta Inf. 6, 319–340 (1976) · Zbl 0312.68011 · doi:10.1007/BF00268134
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.