Speaker: Professor Andrei Voronkov
Date: 2nd November 2011.
Schedule: | 17:00 Registration | 17:30 Lecture |
Location: Lecture Theatre 1.1, Kilburn Building, University of Manchester, Oxford Road, Manchester M13 9PL. (Campus Map No 39).

 

Synopsis

Formal methods are mathematical techniques for analysing computer systems to prove that they have been correctly designed and that they are safe and efficient. They also provide the means of designing the systems. The techniques are highly complex and are implemented as computer programs called ‘theorem provers’. The possibility of using computer programs to prove mathematical theorems attracted the attention of mathematicians long before the first computers became available. Theorem provers are now routinely used to design hardware and find bugs in software. Another emerging application is in text mining, where formal knowledge is extracted from text (e.g. from newspapers or the Web) and reasoning is used to answer queries and derive new knowledge. Research in building theorem provers has a long history and has resulted in several notable achievements that Andrei will discuss. The pure joy as well as the Science of automated reasoning will figure largely in his lecture.

Registration

 

This is a free event, but we ask that you register here to reserve your place.

 

 

About The Speaker

Andrei Voronkov is a Professor in the School of Computer Science at the University of Manchester. He is an international authority on Formal Methods. He was born in Russia, studied at the specialized Physics-Mathematics School in Novosibirsk and graduated from the Department of Mathematics of Novosibirsk State University in 1982. He was awarded a PhD scholarship in Mathematics largely for his athletic achievements in the ‘long jump’ but in 1987 he received his PhD degree with a thesis in constructive logic. Having realised that his real interest lay with Computer Science, he started research in automated theorem proving in 1984 and in 1991 he was invited to work at ECRC (European Computer Industry Research Centre in Munich). He joined Uppsala University as a lecturer in 1993 and the University of Manchester as Professor in 1999.

Although he was occasionally writing computer programs from 1981, it was not until 1993 that he completely overcame the theoretical nature of his education and realised that programming and the mathematics related to it are much more fun than pure maths. In 1994 he was already writing programs that generated and executed code at run time, but he missed the chance of becoming a real computer hacker since he did not realise at the time that such programs could be used to attack networks and other computers. Instead, he became increasingly interested in computer reasoning, which is now routinely used for proving that computer programs written in such a way that they cannot be attacked, are indeed secure.

With the help of his students, he implemented a series of theorem proving programs. The last of them, called Vampire, was entered into the 1999 ‘CADE Automatic Theorem Proving System Competition (CASC) World Championship held annually by the ‘Conference on Automated Deduction’ (CADE). To his great surprise, it won, and since then Vampire has won 25 World Championship titles in various divisions, often solving more problems than all the other theorem prover competitors put together.

Andrei has been an invited speaker and programme committee member for many international conferences. In 2002, having been the programme chair for two such conferences, he decided that the amount of work involved was too much for any busy human being, and that he needed an efficient system to help him to organize the paper submission and reviewing process over the Web. Of course the system he developed had to be proved to work, and he eventually called it ‘EasyChair’. People started to ask for copies of EasyChair, and by 2005 it had become an established Web service. EasyChair has now been used by over 13,000 conferences and 500,000 authors, reviewers and organisers.

Andrei has held visiting positions and acted as consultant for several companies, including Microsoft, Intel and Bull.