Effect-polymorphic behaviour inference for deadlock checking

DOI10.1016/J.JLAMP.2016.05.003MaRDI QIDQ338624zbMATH OpenOpenAlexFDO

Authors Martin Steffen, Volker Stolz, Ka I Pun

Publication date 7 November 2016

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jlamp.2016.05.003

zbMATH Keywords

simulationconcurrencydeadlock detectionformal methodtype and effect system

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Deadlock checking by a behavioral effect system for lock handling
• Deadlock checking by data race detection
• Deadlock checking by data race detection
• Verification, Model Checking, and Abstract Interpretation
• An automatic technique for static deadlock prevention

Cites work

• scientific article; zbMATH DE number 1670563 (Why is no real title available?)
• scientific article; zbMATH DE number 1670568 (Why is no real title available?)
• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 1130261 (Why is no real title available?)
• scientific article; zbMATH DE number 3359777 (Why is no real title available?)
• A Basis for Verifying Multi-threaded Programs
• A Deadlock-Free Semantics for Shared Memory Concurrency
• A New Type System for Deadlock-Free Processes
• A theory of type polymorphism in programming
• Deadlock checking by a behavioral effect system for lock handling
• Deadlock detection in linear recursive programs
• Dynamic inference of polymorphic lock types
• Goblint: path-sensitive data race analysis
• Polymorphic type, region and effect inference
• The Principal Type-Scheme of an Object in Combinatory Logic
• Type-base flow analysis
• Type-based information flow analysis for the \(\pi\)-calculus

Cited in

(3)

• Deadlock checking by data race detection
• Deadlock checking by data race detection
• Deadlock checking by a behavioral effect system for lock handling

Describes a project that uses

Uses Software

• LOCKSMITH
• Goblint
• Featherweight Java
• RacerX
• Eraser
• ML

This page was built for publication: Effect-polymorphic behaviour inference for deadlock checking

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