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

DOI10.1007/S10703-015-0237-0zbMATH Open1331.68048OpenAlexW2214640391MaRDI QIDQ5962972FDOQ5962972

Authors Sagar Chaki, Arie Gurfinkel, Ofer Strichman

Publication date 25 February 2016

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10703-015-0237-0

zbMATH Keywords

proving equivalence of programsregression verificationmulti-threaded programs

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Regression verification for multi-threaded programs
• Automating regression verification of pointer programs by predicate abstraction
• Causality-based verification of multi-threaded programs
• Proof spaces for unbounded parallelism
• A dynamic logic for deductive verification of multi-threaded programs

Cites work

• scientific article; zbMATH DE number 1956591 (Why is no real title available?)
• An axiomatic proof technique for parallel programs
• Inference rules for proving the equivalence of recursive procedures
• Regression verification for multi-threaded programs
• Tentative steps toward a development method for interfering programs
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(6)

• Precise Fixpoint-Based Analysis of Programs with Thread-Creation and Procedures
• Abstract semantic diffing of evolving concurrent programs
• Automating regression verification of pointer programs by predicate abstraction
• Operationally-based program equivalence proofs using LCTRSs
• Regression verification for multi-threaded programs
• Regression verification for unbalanced recursive functions

Describes a project that uses

Uses Software

• z3
• CBMC
• Threader

This page was built for publication: Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5962972)