×

zbMATH — the first resource for mathematics

Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation). (English) Zbl 1331.68048
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 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.

MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Software:
CBMC; Threader; z3
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Chaki S, Gurfinkel A, Strichman O (2011) Time-bounded analysis of real-time systems. In: FMCAD’11
[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-135 · Zbl 1325.68060
[3] Clarke EM, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: TACAS, pp 168-176 · Zbl 1126.68470
[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-346 · Zbl 1161.68013
[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)
[6] Felsing D, Grebing S, Klebanov V, Rmmer P, Ulbrich M (2014) Automating regression verification. In: Automated software engineering (ASE), (to be published)
[7] Godlin B (2008) Regression verification: theoretical and implementation aspects. Master’s thesis, Technion, Israel Institute of Technology
[8] Godlin, B; Strichman, O, Inference rules for proving the equivalence of recursive procedures, Acta Inform, 45, 403-439, (2008) · Zbl 1161.68013
[9] Godlin B, Strichman O (2009) Regression verification. In: \(46^{th}\) Design automation conference (DAC) · Zbl 0517.68032
[10] Gupta A, Popeea C, Rybalchenko A (2011) Threader: a constraint-based verifier for multi-threaded programs. In: CAV, pp 412-417
[11] Jones, CB, Tentative steps toward a development method for interfering programs, ACM Trans Program Lang Syst, 5, 596-619, (1983) · Zbl 0517.68032
[12] Kaser, O; Ramakrishnan, CR; Pawagi, S, On the conversion of indirect to direct recursion, LOPLAS, 2, 151-164, (1993)
[13] Kawaguchi M, Lahiri SK, Rebelo H (2010) Conditional equivalence. Technical Report MSR-TR-2010-119, Microsoft Research · Zbl 0517.68032
[14] Lee, EA, The problem with threads. IEEE, Computer, 39, 33-42, (2006)
[15] Owicki, S; Gries, D, An axiomatic proof technique for parallel programs, Acta Inform, 6, 319-340, (1976) · Zbl 0312.68011
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.