Agenda

04 Lug 2024 12:00

Model Checking a Temporal Logic via Program Verification

Laboratorio ACADIA, edificio ZETA - Campus Scientifico via Torino

Speaker: Diletta Rigo, Università di Padova

Abstract:
We explore the possibility of viewing Model Checking as an instance of program verification in order to allow for the reuse of the vast theory and toolset of Abstract Interpretation in the setting of Model Checking. We focus on ACTL, the universal fragment of the temporal logic CTL, which can describe properties of executions which are universally quantified over paths. We show how ACTL formulae can be mapped into programs written in a suitable programming language, whose execution generates counterexamples to the validity of that formula or proves there is none. Then we discuss how to analyse such programs by Abstract Interpretation over some abstract domain, exploiting the idea of local completeness as put forward in some recent work, combining over- and under-approximations.

Bio Sketch:
Diletta Rigo, master's graduate, University of Padua

Lingua

L'evento si terrà in italiano

Organizzatore

Sabina Rossi

Cerca in agenda