A tableau-based procedure for model checking programs

When verifying applications that require a high level of reliability, testing fails to assure an adequate level of correctness. Thus we apply model checking, an automatic verification technique: the programs are written in a simple sequential language and properties are specified by a suitable temporal logic. We obtain a finite state representation of the system by applying abstraction techniques. The abstraction is derived from the logic formula representing the property to be checked. A tableau-based method is developed to prove satisfaction.