Multi-threading is a methodology that has been extremely used. Modern software depends essentially on multi-threading. Operating systems, famous examples, are based on multi-threading; a user can write his document, play an audio file, and downloading a file from internet at the same time. Each of these tasks called a thread. A common problem occurs when implementing multi-threaded programs is a data-race. Data race occurs when two threads try to access a shared variable at the same time without a proper synchronization. A detector is software that determines if the program contains a data-race problem or not. In this paper, we develop a detector that has the form of a type system. We present a type system which discovers the data-race problems. We also prove the soundness of our type system.

The most common form of computers today is the hand held form and
specially smart phones and tablets. The platform for the majority of
smart phones is the Android operating system. Therefore analyzing
and verifying the Android applications become an issue of extreme
importance. However classical techniques of static analysis are not
applicable directly to Android applications. This is so because
typically Android applications are developed using Java code that is
translated into Java bytecode and executed using Dalvik virtual
machine. Also developing new techniques for static analysis of
Android applications is an involved problem due to many facts such
as the concept of gestures used in Android interaction with users.

One of the main tools of analyzing and verifying programs is types
systems~\cite{el2012heap}. This paper presents a new type system,
Android$\mathcal{T}$, which is specific to Android applications. The
proposed type system ensures the absence of errors like "method is
undefined". Also the type system is applicable to check the
soundness of static analyses of Android applications.