Viðburðir eftir árum


ICE-TCS seminar: Karoliina Lehtinen

Runtime Verification of Fixpoint Logic: Synthesis of Optimal Monitors

  • 22.1.2018, 12:10 - 13:00

ICE-TCS-logo-200px

Date and time: Monday, 22 January 2018 from 12:10 till 13:00
Place: Room M111 at Reykjavik University

Title: Runtime Verification of Fixpoint Logic: Synthesis of Optimal Monitors

Speaker: Karoliina Lehtinen (Christian-Albrechts University of Kiel, Germany)

Abstract:
Runtime monitoring is a verification technique that evades the state explosion problem by only analysing execution traces. Accordingly, it is more restricted than model-checking in the kind of specifications it can verify: only safety and co-safety specifications enjoy sound and complete
monitors.

I will argue that arbitrary specifications can still have meaningful incomplete monitors. I will define what it means for a monitor to be optimal, and prove that all muHML formulas have an optimal deterministic monitor that can be synthesized in 2-Exptime.