2014 Theoretical Aspects of Software Engineering Conference (TASE) (2014)
Sept. 1, 2014 to Sept. 3, 2014
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TASE.2014.23
This paper extends our behavioural type and effect system for detecting deadlocks by polymorphism and formalizing type inference (with respect to lock types). Our inference is defined for a simple concurrent, first-order language. From the inferred effects, after suitable abstractions to keep the state space finite, we either obtain the verdict that the program will not deadlock, or that it may deadlock. We show soundness and completeness of the type inference.
System recovery, Abstracts, Inference algorithms, Standards, Context, Calculus, Syntactics
K. I. Pun, M. Steffen and V. Stolz, "Behaviour Inference for Deadlock Checking," 2014 Theoretical Aspects of Software Engineering Conference (TASE), Changsha, China, 2014, pp. 106-113.