Verification of Data in Space and Time
Abstract: Research data can take very many forms, but in many cases there are interesting relations between elements of data. Such relations could be of various nature, for example causal relations, temporal relations, spatial relations or any combination thereof, to mention a few. Reasoning about time and space and their combination has a long history. Only more recently, reasoning about spatial aspects of systems, that is, the properties of entities that relate to their position, distance, connectivity and reachability in space, have received increasing attention in computer science. We present recent results in spatial and spatio-temporal logic, that have their origin in Modal logic and early work dating back to McKinsey and Tarksi, and their evolution into efficient spatial and spatio-temporal model checking methods. We illustrate these methods by their application to various domains ranging from smart public transportation to medical imaging. In the latter domain, data-analysis techniques, such as machine learning, provide a popular new area of research too, opening the way for an interesting discussion on how various methods could be used profitable in a complementary way.
Short Bio: Mieke Massink received her master’s degree in computer science from the University of Nijmegen, The Netherlands in 1988; she received her Laurea in Computer Science from the University of Pisa in 1995 and her PhD degree in computer science from the University of Nijmegen in 1996. In 1992 she received the “Dr. I.B.M. Frye Stipend” of the University of Nijmegen for the most promising female PhD researcher. She is currently a researcher in the Formal Methods and Tools lab at CNR-ISTI (Institute of Information Science and Technology “A. Faedo”), a computer science research institute of the National Research Council of Italy (CNR).
Prior to this she held positions at the University of Nijmegen, The University of Twente, both in the Netherlands, and in the context of several European projects, the CNR-CNUCE institute, Italy, and the University of York, United Kingdom. She has been lecturing at the University of Pisa from 1996 to 1998 and from 2006 to 2009 and at the University of Florence from 2005 to 2017. She is lecturing in the Tuscan PhD program in Smart Computing from 2015; in Feb. 2011 she was Visiting Professor at the MT-Lab, DTU, Copenhagen, DK. She has served as PC member/chair of numerous conferences and workshops in the area of Formal Methods. Her research interests include the development and application of formal languages for specification and verification of concurrent, safety critical and software intensive systems, including collective adaptive systems which may exhibit emergent behaviour, and human interaction related aspects of such systems. In particular her interest is in semantic models and scalable verification techniques for process algebras and automata, and their extension with aspects of mobility, time, space e/o probability, with a focus on temporal and modal logics for the specification and verification of related properties through logic-based model checking.