# Logic foundation for formal verification

What types of logic should one study as foundation before diving into the area of software verification? What I can think of are:

1. Hoare Logic (for proving correctness of imperative programs)
2. Linear Temporal Logic (to model-check programs)

What can be others?