Michael J. Butler

From Wikipedia, the free encyclopedia

This article or section needs sources or references that appear in reliable, third-party publications.
Primary sources and sources affiliated with the subject of the article are generally not sufficient for a Wikipedia article. Please include more appropriate citations from reliable sources, or discuss the issue on the talk page.
This article has been tagged since May 2008.

This article may not meet the general notability guideline or one of the following specific guidelines for inclusion on Wikipedia: Biographies, Books, Companies, Fiction, Music, Neologisms, Numbers, Web content, or several proposals for new guidelines. If you are familiar with the subject matter, please expand or rewrite the article to establish its notability. The best way to address this concern is to reference published, third-party sources about the subject. If notability cannot be established, the article is more likely to be considered for redirection, merge or ultimately deletion, per Wikipedia:Guide to deletion.
This article has been tagged since June 2008.

Michael J. Butler is Professor of Computer Science at the University of Southampton, UK.

Butler was originally from Ireland and received his Bachelors degree in Computer Science from Trinity College, Dublin in 1988. He then undertook and MSc and DPhil at the Programming Research Group in Oxford (1989 and 1992 respectively), working in the area of Communicating Sequential Processes (CSP). Subsequently he worked for Broadcom in Dublin and at Åbo Akademi University in Turku, Finland with Ralph-Johan Back on Refinement Calculus. He joined the University of Southampton in 1995 as a lecturer, rising to Reader in 2000 and then Professor in the same year.

He leads the Dependable Systems & Software Engineering group in the School of Electronics and Computer Science at Southampton. His main research is in the area of the B-Method, especially tool support such as ProB (model checking for B), U2B (UML and B), csp2B (CSP and B), and the RODIN toolset for Event-B.