Concurrent programs and concurrent systems are usually highly efficient and are widely used in practice. However, concurrent programs and systems are often prone to error, which could bring fatal consequences in real world applications. Moreover, the non-determinism brought by concurrency is a major difficulty in the verification of concurrent programs. But with formal verification, people could use interactive theorem provers to rigorously prove the correctness of a concurrent program. We present several correctness criteria for concurrent programs, which can be verified using interactive theorem proof techniques. They include Hoare triple, linearizability, contextual refinement, and logical atomicity. Researchers usually use program logics to verify programs in an interactive theorem prover. We summarize the usage of concurrent separation logic, rely-guarantee based logic, and relational Hoare logic in concurrent program verifications. We also surveyed existing foundational verification tools and verification results using these techniques.