Personal tools
You are here: Home Events Milner Lectures Milner Lecture 2012

Milner Lecture 2012

Milner Lecture 4pm Tuesday 25 September 2012

Informatics Forum, G.07

The University of Edinburgh

10 Crichton Street, Edinburgh, EH8 9AB

*Followed by a reception in Informatics Forum


Marta Kwiatkowska, University of Oxford

Sensing everywhere: on quantitative verification for ubiquitous computing / Seminar Video

Ubiquitous computing, as originally foreseen by Weiser in 1990s, is a vision of a world where computers are invisible and become pervasive, embedded in our environment, equipment we handle, or even our bodies. These computing devices are sensor-enabled, so that they can interface to the physical world, and autonomous, silently supporting our daily activities and making decisions on our behalf. The progress towards this vision has been relentless, giving rise to a multitude of applications of smart sensor technologies, from environmental monitoring to healthcare. Robin Milner was a great proponent of the science for ubiquitous computing, arguing the need for appropriate rigorous foundations and reasoning frameworks. In this lecture, I will describe recent progress concerning the role that quantitative verification can play towards improving the safety and reliability of sensor-enabled devices, focusing on the kinds of models, logics and tools needed for this purpose. The research will be illustrated with examples of smart energy management, implantable medical devices and, looking towards the future, sensing at the molecular level.


Marta Kwiatkowska is Professor of Computing Systems and Fellow of Trinity College, University of Oxford. She was elected to Academia Europea in 2011 and received a prestigious ERC Advanced Grant VERIWARE "From software verification to everyware verification", 2010-15.

Kwiatkowska's research is concerned with modelling and automated verification techniques for probabilistic systems, with application to engineered and biological systems. Her work was recognised by invitations to speak at the LICS 2003, ESEC/FSE 2007, FASE/ETAPS 2011 and SAFECOMP 2012 conferences. The PRISM model checker developed under her leadership is internationally leading in the area and widely used for research and teaching. Applications of probabilistic model checking have spanned communication and security protocols, nanotechnology designs, power management and systems biology. Her research is supported by £3m of grant funding from EPSRC, EU, Oxford Martin School and Microsoft Research.

Marta Kwiatkowska serves on numerous programme committees and editorial boards of several journals, including Formal Methods in System Design, IEEE Transactions on Software Engineering and Royal Society's Philosophical Transactions A. She was lead organiser of the Royal Society Discussion Meeting "From computers to ubiquitous computing, by 2020" and guest co-editor of the associated Proceedings in Phil. Trans. R. Soc. A vol 366 no 1881.

Document Actions