Title: An LTL Proof System for Runtime Verification
By: Adrian Francalanza (Univ. Malta)
Abstract:
We propose a local proof system for Linear Temporal Logic (LTL) that formalised deductions within the constraints of Runtime Verification (RV), and show how such a system can be used as a basis for constructing online runtime monitors. Soundness and partial completeness results are proven for the proof system. We also prove decidability and incrementality properties for a monitoring algorithm constructed from our deductive system. Finally, we relate the expressivity of our framework to existing symbolic analysis techniques for LTL used for online monitoring. (Joint work with Clare Cini)
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.
More info: http://citi.di.fct.unl.pt/seminar/seminar.php?id=239