An assertion is a condition that must hold true in every possible execution of the program. Assertions in SMV are written in a ``linear time'' temporal logic, that makes it possible to succinctly state propositions about the relation of events in time.