Abstract: Reducing the likelihood of human error in human-computer interaction is increasingly important. Human errors could not only hinder the correct use and operation, they can also compromise the safety and security of interactive systems. Hence the need for formal methods to analyse and verify the correctness of interactive systems, particularly with regards to human interaction. This seminar will illustrate through examples how to incorporate human behaviour within a formal model of the system and how to use formal analysis techniques, in particular model-checking, to detect patterns of human behaviours that may lead to erroneous interactions. Finally, the seminar will describe how model-checking may be used as a supporting tool in cognitive psychology to formally verify the correctness and completeness of behavioural theories developed from empirical studies. Short bio: Antonio Cerone joined the International Institute for Software Technology (IIST) of the United Nations University (UNU) as a Research Fellow in February 2004. His research focuses on the use of formal methods in verification of software and hardware, and in modelling cognitive human behaviour. He is particularly interested in the verification of interactive systems, security systems, safety-critical systems, asynchronous hardware and concurrent and real-time systems. Antonio completed his PhD in 1993 and his Master's degree in 1989, both at the University of Pisa, Italy.