Static Analysis Via Abstract Interpretation of the Happens-Before Memory Model

DOI10.1007/978-3-540-79124-9_9MaRDI QIDQ5458814zbMATH OpenOpenAlexFDO

Authors Pietro Ferrara

Publication date 24 April 2008

Published in Tests and Proofs (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-79124-9_9

zbMATH Keywords

Abstract InterpretationMemory ModelMultithreaded ProgramsStatic Analysis

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 1951189
• Effective abstractions for verification under relaxed memory models
• An operational happens-before memory model
• The Java memory model
• scientific article; zbMATH DE number 1949622

Cites work

• Causal Dataflow Analysis for Concurrent Programs
• scientific article; zbMATH DE number 1834570 (Why is no real title available?)
• The Java memory model
• The Java Memory Model: Operationally, Denotationally, Axiomatically
• The octagon abstract domain
• Time, clocks, and the ordering of events in a distributed system

Cited in

(4)

• Hybrid analysis: Static \& dynamic memory reference analysis
• Improving thread-modular abstract interpretation
• Static analysis of run-time errors in embedded critical parallel C programs
• Calculating statically maximum log memory used by multi-threaded transactional programs

Describes a project that uses

Uses Software

• Octagon

This page was built for publication: Static Analysis Via Abstract Interpretation of the Happens-Before Memory Model

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