Combining static analysis and run -time analysis for verification and testing of multi-threaded programs

Multithreaded programs are becoming more and more widely used. Such programs are notorious for containing errors that are difficult to reproduce and diagnose at run-time. Common synchronization errors in multithreaded programs include data races, atomicity violations, and deadlocks. A data race occurs when two threads concurrently access a shared variable and at least one of the accesses is a write. Atomicity is a common higher-level correctness requirement that expresses non-interference between concurrently executed methods. A method is atomic if every execution of the program is equivalent to an execution in which that method is executed without being interleaved with other concurrently executed methods. An atomicity violation occurs when a method expected to be atomic is not. A deadlock occurs when some threads are permanently blocked.;Several static and dynamic (run-time) analysis techniques exist to detect such errors. Static analysis techniques usually provide stronger guarantees, though they can be overly conservative and hence report more false alarms. Precise static analysis is often computationally hard and hence less scalable. Run-time checking generally produces fewer false alarms than static analysis; this is a significant practical advantage, since diagnosing all of the warnings from static analysis of large codebases may be prohibitively expensive. However, run-time checks may miss errors in unexecuted code and often incur significant run-time overhead. This thesis explores how static and run-time analyses can be combined to assist each other and alleviate the shortcomings of both.;We developed expressive type systems for proving absence of data races, atomicity violations, and deadlocks. To save the programmer from writing type annotations, we developed type inference algorithms for these type systems. Complete type inference for race-free type systems is NP-hard. Our inference algorithm for race types, which we call type discovery, is a novel combination of run-time analysis and static analysis.;We also explored the use of static analysis to significantly decrease the overhead of run-time checking. Warnings from the typechecker are used to identify parts of the program from which run-time checking can safely be omitted. When the types are obtained by type discovery or type inference, the approach is completely automatic, scalable to very large programs, and significantly reduces the overhead of run-time checking for data races, atomicity violations, and deadlocks.