Browse our site
About
People
Research Areas
Projects
Publications
Seminars
Future
Past
News
You are here:
Home
Seminars
Past
Synthesising Correct Concurrent Runtime Monit...
Synthesising Correct Concurrent Runtime Monitors
Main information
By:
Adrian Francalanza (University of Malta)
Date:
Wednesday, 5th of February 2014, 14h00
Location:
FCT/UNL, Seminar Room (Ed. II)
Abstract
Runtime verification of programs is often carried out by monitors, software entities running along side the program being verified, observing its behaviour and flagging whenever a satisfaction or violation is detected. A fundamental tenet underlying such a setup is the correctness of the monitor itself. In this talk I shall discuss recent work on synthesising correct concurrent monitors for runtime verification. In particular I shall focus on an adaptation of the mu-calculus that allows one to specify safety properties for Erlang programs. I outline issues relating to automated synthesis from formulas in this logic to Erlang monitors that detect formula violations at runtime. I present a formalisation of monitor correctness for this concurrent setting and describe a technique that can be used to prove monitor correctness in stages; this technique is used to prove the correctness of the monitor synthesis presented.
Short-bio
Adrian Francalanza obtained his PhD from Sussex University, working on co-inductive theories for partial-failure and fault tolerance in a distributed pi-calculus. During his post-doctorate, he worked on ownership types for object-oriented languages at Imperial College, and then on separation-based logics for message-passing languages at Southampton University. He is currently a senior lecturer at the University of Malta. Adrian's main reasearch interests focus on the formal aspects of message-passing concurrent programs, ranging from semantic theories for program equivalence, to program correctness through type systems and program logics.
Departamento de Informática, FCT/UNL
Quinta da Torre 2829-516 CAPARICA - Portugal
Tel. (+351) 21 294 8536 FAX (+351) 21 294 8541