Cellular Automata (CA) are a simple computational model defined by a regular grid of cells, where each cell updates its own state by evaluating a local rule on its neighborhood. CA have long been investigated as a tool to simulate complex systems, particularly because of two distinctive properties: the manifestation of complex dynamical behaviors emerging from the local interactions among the cells, and the massive parallelism of the model, which lends itself to very efficient implementations. Indeed, since their inception in the 1950s by Ulam and Von Neumann, CA have been applied in the most disparate fields, including biology, physics, ecology and many others. The aim of this talk is to give a general introduction to CA, especially focusing on their connections to formal languages and model checking. In particular, we show how model checking approaches have been applied to classify dynamical properties of CA in terms of their decidability. Finally, we present a recent result where algebraic language theory naturally emerges to solve a counting problem related to a cryptographic application of CA.