I will present an approach for the verification of programmer-specified safety properties, such as method preconditions and postconditions, as well as the absence of data races and deadlocks in multithreaded Java-like programs. Under the approach, the programmer first specifies the safety properties of interest in special comments in the program source code. A tool then translates the annotated source program to a set of first-order logic verification conditions, which are then passed to an automatic theorem prover. The approach verifies absence of data races by associating with each thread an access set, which is a set of objects. A thread's access set starts out empty and grows and shrinks as the thread creates, locks, and unlocks objects. A thread may only read or write the fields of the objects in its access set. Access sets of different threads never intersect.