Tuesday, Sept.10th, 2019 – 11:00 am
Runtime Verification is a lightweight technique that complements other verification methods in a multi-pronged approach towards ensuring software correctness. The technique poses novel questions to software engineers: it is not easy to see which specifications are amenable to runtime monitoring, and it is not clear which monitors perform the required runtime analysis correctly.
In this talk, I will present a theoretical framework that can be used to provide answers to those questions. Our approach uses the classic Hennessy-Milner with recursion as a specification logic that is agnostic of the adopted verification method and is general enough to embed commonly used specification logics. I also present an operational semantics for an elemental framework that describes the runtime analysis carried out by monitors. This allows us to establish a correspondence between the property satisfactions in the logic and the verdicts reached by the monitors carrying out the analysis. I will show how this correspondence is used to identify which subsets of the logic can be adequately monitored for, to study the power of deterministic monitors and to define various notions of monitor correctness. In this talk, I will assume no prior knowledge of runtime verification.
The talk is based on joint work with my collaborators in the project Theoretical Foundations for Monitorability.
Luca Aceto has been a full professor of computer science at Reykjavik University since November 2004. From September 2017 he is also full professor at the Gran Sasso Science Institute, L’Aquila (Italy), where he is the scientific director of the computer science group and the coordinator of the international PhD programme in computer science. Before joining Reykjavik University, he was an associate professor at Aalborg University (1996-2006) and a lecturer at the University of Sussex (1992-1996) amongst other appointments.
Luca Aceto is an elected member of the Informatics Section of Academia Europaea (the Academy of Europe). He also serves as the chair of the editorial board of LIPIcs, Leibniz International Proceedings in Informatics, and is a member of the Executive Board of the journal Logical Methods in Computer Science, of the Advisory Board of Electronic Proceedings in Theoretical Computer Science, and of the editorial boards of the Journal of Logical and Algebraic Methods in Programming and of Electronic Proceedings in Theoretical Computer Science. He was the president of the European Association for Theoretical Computer Science in the period July 2012-July 2016. He was the founder and first chair of IFIP WG 1.8 on Concurrency Theory, and co-founded and co-directed the Icelandic Centre of Excellence in Theoretical Computer Science since 2005.
Luca Aceto’s main research interests are in concurrency theory, with emphasis on the study of algebraic process description languages and on the techniques they support to specify and reason about reactive systems, logic in computer science, structural operational semantics and applications of equational logic in computer science. To date, he has published two books, ten book chapters, 58 journal papers and 74 refereed conference/workshop papers. In addition, he has edited more than 30 volumes.
Luca Aceto received a Distinguished Dissertation Award of the British Computer Society in 1991 and the Reykjavik University Research Award in 2012. He was Teacher of the Year in Mathematics and Computer Science at Aalborg University in 1997 and 1999.
The presentation will be in English. Free entrance.