zbMATH — the first resource for mathematics

Type inference against races. (English) Zbl 1104.68399
Giacobazzi, Roberto (ed.), Static analysis. 11th international symposium, SAS 2004, Verona, Italy, August 26–28, 2004. Proceedings. Berlin: Springer (ISBN 3-540-22791-1/pbk). Lecture Notes in Computer Science 3148, 116-132 (2004).
Summary: The race condition checker rccjava uses a formal type system to statically identify potential race conditions in concurrent Java programs, but it requires programmer-supplied type annotations. This paper describes a type inference algorithm for rccjava. Due to the interaction of parameterized classes and dependent types, this type inference problem is NP-complete. This complexity result motivates our new approach to type inference, which is via reduction to propositional satisfiability. This paper describes our type inference algorithm and its performance on programs of up to 30,000 lines of code.
For the entire collection see [Zbl 1056.68010].

68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Full Text: DOI