An overview of formal languages and algorithms used for verification of (abstractions) of hardwarre, software and communication protocols with particular attention for concurrent and distributed systems (finite and infinite-state specifications): FOL and Modal Logic. Temporal Logic: LTL and CTL. Model checking algorithms, Existential/Universal Abstractions, Abstraction Refinement, Abstract Interpretation, Fixpoint Computation, Widening. Abstract domains: Intervals, Octagons, Polyhedra. Infinite-state and Parameterized systems