We survey principles of model checking techniques for the automatic analysis of reactive systems. The use of model checking is exemplified by an analysis of the Needham-Schroeder p...
d Abstract) Luboˇs Brim and Jiˇr´ı Barnat Faculty of Informatics, Masaryk University, Brno, Czech Republic With the increase in the complexity of computer systems, it becomes e...