Effect-polymorphic behaviour inference for deadlock checking

DOI10.1016/j.jlamp.2016.05.003zbMath1392.68148OpenAlexW2394951157MaRDI QIDQ338624

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

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

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Deadlock checking by a behavioral effect system for lock handling
• A theory of type polymorphism in programming
• Dynamic inference of polymorphic lock types
• Type-based information flow analysis for the \(\pi\)-calculus
• A Deadlock-Free Semantics for Shared Memory Concurrency
• A Basis for Verifying Multi-threaded Programs
• Polymorphic type, region and effect inference
• Deadlock Detection in Linear Recursive Programs
• Type-base flow analysis
• The Principal Type-Scheme of an Object in Combinatory Logic
• A New Type System for Deadlock-Free Processes