seminars
Detail
Publication date: 1 de June, 2021An LTL Proof System for Runtime Verification
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.
| Date | 04/02/2015 |
|---|---|
| State | Concluded |
| Host 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. |