Article

Regression verification for multi-threaded programs

Authors:

Sagar Chaki,

Arie Gurfinkel,

Ofer StrichmanAuthors Info & Claims

VMCAI'12: Proceedings of the 13th international conference on Verification, Model Checking, and Abstract Interpretation

Pages 119 - 135

https://doi.org/10.1007/978-3-642-27940-9_9

Published: 22 January 2012 Publication History

Publisher Site

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 <em>concurrent</em> programs to that of regression verification between <em>sequential</em> 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.

References

[1]

Full version at ie.technion.ac.il/˜ofers/publications/vmcai12_full.pdf

Google Scholar

[2]

Cobleigh, J.M., Giannakopoulou, D., Pasareanu, C.S.: Learning Assumptions for Compositional Verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 331-346. Springer, Heidelberg (2003).

Digital Library

Google Scholar

[3]

Godlin, B.: Regression verification: Theoretical and implementation aspects. Master's thesis, Technion, Israel Institute of Technology (2008).

Google Scholar

[4]

Godlin, B., Strichman, O.: Inference rules for proving the equivalence of recursive procedures. Acta Informatica 45(6), 403-439 (2008).

Digital Library

Google Scholar

[5]

Godlin, B., Strichman, O.: Regression verification. In: 46th Design Automation Conference, DAC (2009).

Digital Library

Google Scholar

[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).

Digital Library

Google Scholar

[7]

Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596-619 (1983).

Digital Library

Google Scholar

[8]

Kaser, O., Ramakrishnan, C.R., Pawagi, S.: On the conversion of indirect to direct recursion. LOPLAS 2(1-4), 151-164 (1993).

Digital Library

Google Scholar

[9]

Kawaguchi, M., Lahiri, S.K., Rebelo, H.: Conditional equivalence. Technical Report MSR-TR-2010-119, Microsoft Research (2010).

Google Scholar

[10]

Lee, E.A.: The problem with threads. IEEE Computer 39(5), 33-42 (2006).

Digital Library

Google Scholar

[11]

Owicki, S.S., Gries, D.: An Axiomatic Proof Technique for Parallel Programs I. Acta Inf. 6, 319-340 (1976).

Google Scholar

Cited By

View all

Zhu CZhang MWu XXu XLi Y(2023)Client-Specific Upgrade Compatibility Checking via Knowledge-Guided DiscoveryACM Transactions on Software Engineering and Methodology10.1145/358256932:4(1-31)Online publication date: 26-May-2023
https://dl.acm.org/doi/10.1145/3582569
He FHan J(2020)Termination analysis for evolving programs: an incremental approach by reusing certified modulesProceedings of the ACM on Programming Languages10.1145/34282674:OOPSLA(1-27)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428267
Yu QHe FWang B(2020)Incremental predicate analysis for regression verificationProceedings of the ACM on Programming Languages10.1145/34282524:OOPSLA(1-25)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428252
Show More Cited By

Recommendations

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 ...
Reduction for Compositional Verification of Multi-Threaded Programs
FMCAD '14: Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design

Automated verification of multi-threaded programs requires keeping track of a very large number of possible interactions between the program threads. Different reasoning methods have been proposed that alleviate the explicit enumeration of all thread ...
Effective verification of confidentiality for multi-threaded programs
Foundational Aspects of Security

This paper studies how confidentiality properties of multi-threaded programs can be verified efficiently by a combination of newly developed and existing model checking algorithms. In particular, we study the verification of scheduler-specific ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

VMCAI'12: Proceedings of the 13th international conference on Verification, Model Checking, and Abstract Interpretation

January 2012

461 pages

ISBN:9783642279393

Editors:
Viktor Kuncak
Swiss Federal Institute of Technology Lausanne (EPFL), IC IIF LARA INR 318, Station 14, Lausanne, Switzerland
,
Andrey Rybalchenko
Institut für Informatik, Technische Universität München, Boltzmannstr. 3, Munich, Germany

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 22 January 2012

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 12 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Zhu CZhang MWu XXu XLi Y(2023)Client-Specific Upgrade Compatibility Checking via Knowledge-Guided DiscoveryACM Transactions on Software Engineering and Methodology10.1145/358256932:4(1-31)Online publication date: 26-May-2023
https://dl.acm.org/doi/10.1145/3582569
He FHan J(2020)Termination analysis for evolving programs: an incremental approach by reusing certified modulesProceedings of the ACM on Programming Languages10.1145/34282674:OOPSLA(1-27)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428267
Yu QHe FWang B(2020)Incremental predicate analysis for regression verificationProceedings of the ACM on Programming Languages10.1145/34282524:OOPSLA(1-25)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428252
Abadi MKeidar-Barner SPidan DVeksler T(2019)Verifying Parallel Code After Refactoring Using Equivalence CheckingInternational Journal of Parallel Programming10.1007/s10766-017-0548-447:1(59-73)Online publication date: 1-Feb-2019
https://dl.acm.org/doi/10.1007/s10766-017-0548-4
Murawski ATzevelekos N(2018)Algorithmic games for full ground referencesFormal Methods in System Design10.5555/3220753.322085452:3(277-314)Online publication date: 1-Jun-2018
https://dl.acm.org/doi/10.5555/3220753.3220854
Lopes NMonteiro J(2016)Automatic equivalence checking of programs with uninterpreted functions and integer arithmeticInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-015-0366-118:4(359-374)Online publication date: 1-Aug-2016
https://dl.acm.org/doi/10.1007/s10009-015-0366-1
Partush NYahav E(2014)Abstract semantic differencing via speculative correlationACM SIGPLAN Notices10.1145/2714064.266024549:10(811-828)Online publication date: 15-Oct-2014
https://dl.acm.org/doi/10.1145/2714064.2660245
Partush NYahav EBlack AMillstein T(2014)Abstract semantic differencing via speculative correlationProceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications10.1145/2660193.2660245(811-828)Online publication date: 15-Oct-2014
https://dl.acm.org/doi/10.1145/2660193.2660245
Böhme MOliveira BRoychoudhury ANotkin DCheng BPohl K(2013)Partition-based regression verificationProceedings of the 2013 International Conference on Software Engineering10.5555/2486788.2486829(302-311)Online publication date: 18-May-2013
https://dl.acm.org/doi/10.5555/2486788.2486829
Beyer DLöwe SNovikov EStahlbauer AWendler PMeyer BBaresi LMezini M(2013)Precision reuse for efficient regression verificationProceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering10.1145/2491411.2491429(389-399)Online publication date: 18-Aug-2013
https://dl.acm.org/doi/10.1145/2491411.2491429

Abstract

References

Cited By

Recommendations