Automatic verification of determinism for structured parallel programs

DOI10.1007/978-3-642-15769-1_28MaRDI QIDQ4930747zbMATH OpenOpenAlexFDO

Authors Martin Vechev, Eran Yahav, Raghavan Raman, Vivek Sarkar

Publication date 1 October 2010

Published in Static Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-15769-1_28

Mathematics Subject Classification ID

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

Recommendations

• SingleTrack: A Dynamic Determinism Checker for Multithreaded Programs
• A type and effect system for determinism in multithreaded programs
• Efficient detection of determinacy races in cilk programs
• Refinement for structured concurrent programs
• Automated Verification of Concurrent Search Structures

Cited in

(9)

• Mostly automated formal verification of loop dependencies with applications to distributed stencil algorithms
• Verifying parallel programs with dynamic communication structures
• Denotational fixed-point semantics for constructive scheduling of synchronous concurrency
• Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms
• Toward a formal semantic framework for deterministic parallel programming
• Automated Verification of Concurrent Search Structures
• Modular reasoning for deterministic parallelism
• Safe nondeterminism in a deterministic-by-default parallel language
• From non-preemptive to preemptive scheduling using synchronization synthesis

Describes a project that uses

Uses Software

• SingleTrack
• Apron
• Eraser
• Interproc
• Soot
• Octagon

This page was built for publication: Automatic verification of determinism for structured parallel programs

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