# Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation)

- 198 Downloads
- 1 Citations

## 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 of multi-threaded programs. Specifically, we develop a proof-rule whose premise requires only to verify equivalence between *sequential functions*, whereas their consequents are equivalence of *concurrent programs*. This ability to avoid composing threads altogether when discharging premises, in a fully automatic way and for general programs, uniquely distinguishes our proof rule from others used for classical verification of concurrent programs. We also consider the effect of dynamic thread creation and synchronization primitives.

## Keywords

Regression verification Proving equivalence of programs Multi-threaded programs## Notes

### Acknowledgments

This material is based upon work funded and supported by the Department of Defense under Contract No. FA8721-05-C-0003 with Carnegie Mellon University for the operation of the Software Engineering Institute, a federally funded research and development center. This material has been approved for public release and unlimited distribution. DM-0001970.

## References

- 1.Chaki S, Gurfinkel A, Strichman O (2011) Time-bounded analysis of real-time systems. In: FMCAD’11Google Scholar
- 2.Chaki S, Gurfinkel A, Strichman O (2012) Regression verification for multi-threaded programs. In: Kuncak V, Rybalchenko A (eds) VMCAI, vol 7148 of Lecture Notes in computer science, Springer, pp 119–135Google Scholar
- 3.Clarke EM, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: TACAS, pp 168–176Google Scholar
- 4.Cobleigh JM, Giannakopoulou D, Pasareanu CS (2003) Learning assumptions for compositional verification. In: 9th International conference on tools and algorithms for the construction and analysis of systems (TACAS’03), pp 331–346Google Scholar
- 5.de Moura L, Bjorner N (2008) Z3: an efficient smt solver. In: International conference on tools and algorithms for the construction and analysis of systems (TACAS)Google Scholar
- 6.Felsing D, Grebing S, Klebanov V, Rmmer P, Ulbrich M (2014) Automating regression verification. In: Automated software engineering (ASE),
**(to be published)**Google Scholar - 7.Godlin B (2008) Regression verification: theoretical and implementation aspects. Master’s thesis, Technion, Israel Institute of TechnologyGoogle Scholar
- 8.Godlin B, Strichman O (2008) Inference rules for proving the equivalence of recursive procedures. Acta Inform 45(6):403–439MATHMathSciNetCrossRefGoogle Scholar
- 9.Godlin B, Strichman O (2009) Regression verification. In: \(46^{th}\) Design automation conference (DAC)Google Scholar
- 10.Gupta A, Popeea C, Rybalchenko A (2011) Threader: a constraint-based verifier for multi-threaded programs. In: CAV, pp 412–417Google Scholar
- 11.Jones CB (1983) Tentative steps toward a development method for interfering programs. ACM Trans Program Lang Syst 5(4):596–619MATHCrossRefGoogle Scholar
- 12.Kaser O, Ramakrishnan CR, Pawagi S (1993) On the conversion of indirect to direct recursion. LOPLAS 2(1–4):151–164CrossRefGoogle Scholar
- 13.Kawaguchi M, Lahiri SK, Rebelo H (2010) Conditional equivalence. Technical Report MSR-TR-2010-119, Microsoft ResearchGoogle Scholar
- 14.Lee EA (2006) The problem with threads. IEEE. Computer 39(5):33–42CrossRefGoogle Scholar
- 15.Owicki S, Gries D (1976) An axiomatic proof technique for parallel programs. Acta Inform 6:319–340MATHMathSciNetCrossRefGoogle Scholar