Formal Methods in System Design

, Volume 47, Issue 3, pp 287–301 | Cite as

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



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.


Regression verification Proving equivalence of programs Multi-threaded programs 



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.


  1. 1.
    Chaki S, Gurfinkel A, Strichman O (2011) Time-bounded analysis of real-time systems. In: FMCAD’11Google Scholar
  2. 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. 3.
    Clarke EM, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: TACAS, pp 168–176Google Scholar
  4. 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. 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. 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. 7.
    Godlin B (2008) Regression verification: theoretical and implementation aspects. Master’s thesis, Technion, Israel Institute of TechnologyGoogle Scholar
  8. 8.
    Godlin B, Strichman O (2008) Inference rules for proving the equivalence of recursive procedures. Acta Inform 45(6):403–439MATHMathSciNetCrossRefGoogle Scholar
  9. 9.
    Godlin B, Strichman O (2009) Regression verification. In: \(46^{th}\) Design automation conference (DAC)Google Scholar
  10. 10.
    Gupta A, Popeea C, Rybalchenko A (2011) Threader: a constraint-based verifier for multi-threaded programs. In: CAV, pp 412–417Google Scholar
  11. 11.
    Jones CB (1983) Tentative steps toward a development method for interfering programs. ACM Trans Program Lang Syst 5(4):596–619MATHCrossRefGoogle Scholar
  12. 12.
    Kaser O, Ramakrishnan CR, Pawagi S (1993) On the conversion of indirect to direct recursion. LOPLAS 2(1–4):151–164CrossRefGoogle Scholar
  13. 13.
    Kawaguchi M, Lahiri SK, Rebelo H (2010) Conditional equivalence. Technical Report MSR-TR-2010-119, Microsoft ResearchGoogle Scholar
  14. 14.
    Lee EA (2006) The problem with threads. IEEE. Computer 39(5):33–42CrossRefGoogle Scholar
  15. 15.
    Owicki S, Gries D (1976) An axiomatic proof technique for parallel programs. Acta Inform 6:319–340MATHMathSciNetCrossRefGoogle Scholar

Copyright information

© Springer Science+Business Media New York 2015

Authors and Affiliations

  1. 1.SEI/CMUPittsburghUSA
  2. 2.TechnionHaifaIsrael

Personalised recommendations