Parallel assertions for architectures with weak memory models

DOI10.1007/978-3-642-33386-6_21MaRDI QIDQ4649301zbMATH OpenOpenAlexWikidataFDO

Authors Daniel Schwartz-Narbonne, Georg Weissenbacher, Sharad Malik

Publication date 21 November 2012

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-33386-6_21

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Semantics in the theory of computing (68Q55)

Recommendations

• Program verification under weak memory consistency using separation logic
• Loop invariant symbolic execution for parallel programs
• scientific article; zbMATH DE number 2090570
• Model checking concurrent programs
• Parallel assignments in software model checking

Cited in

(2)

• Underspecified harnesses and interleaved bugs
• The impact of memory models on software reliability in multiprocessors

Describes a project that uses

Uses Software

• PARSEC
• LLVM

This page was built for publication: Parallel assertions for architectures with weak memory models

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