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

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

Ofer Strichman, Arie Gurfinkel, Sagar Chaki

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

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

zbMATH Keywords

proving equivalence of programsregression verificationmulti-threaded programs

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• An axiomatic proof technique for parallel programs
• Tentative steps toward a development method for interfering programs
• Tools and Algorithms for the Construction and Analysis of Systems
• Regression Verification for Multi-threaded Programs
• Inference rules for proving the equivalence of recursive procedures

Cited In (3)

• Abstract semantic diffing of evolving concurrent programs
• Operationally-based program equivalence proofs using LCTRSs
• Precise Fixpoint-Based Analysis of Programs with Thread-Creation and Procedures

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)