Ciclo di seminari
System Verification via Substructural Logics
Programma
Nell'ambito del ciclo LAAG:IT - Logica, Algebra, Analisi, Geometria, Informatica Teorica e loro applicazioni, i Proff. Marco Bernardo e Giovanni Molica Bisci sono lieti di invitarvi al seminario intitolato "System Verification via Substructural Logics" che sarà tenuto dal Dott. Ludovico Fusco dell'Università di Urbino.
Trace-based modeling is a well-known approach to the behavioral analysis of reactive systems. In this framework, a system is identified with the set of its execution traces and the policies it complies with are modeled set-theoretically as either trace properties or hyperproperties. While the former (e.g., reachability, fairness, etc.) describe features of individual computations, the latter (e.g., noninterference, observational determinism, etc.) specify conditions under which the behavior of a system in certain runs does or does not depend on the characteristics of certain alternative executions. Thus, while trace properties are sets of traces, hyperproperties are sets of trace properties. This provides a framework for a policy classification based on the safety/liveness and hypersafety/hyperliveness dichotomies. Inextricably linked to the dynamics of system evolution, behavioral properties admit very natural formalizations in linear- and branching-time temporal logics (and related formalisms). Consequently, model checking is the paradigm of choice for their verification.
However, a well-known definition of safety in terms of Kuratowski closure operators on residuated lattices suggests a strong connection between substructural logics and system verification. In this talk, starting from the main results in the literature on the topological counterparts of safety and liveness, I present a work in progress where I try to develop this idea in a systematic way. In particular, I argue that some key concepts in the verification of trace properties can be expressed in an appropriate extension of the Full Lambek calculus, on which I present some preliminary results. Finally, I discuss some research avenues on how to extend this approach to hyperproperty verification. The theoretical discussion is complemented by practical examples on hyperproperties for RFID systems.
Il seminario si svolgerà in presenza, ma sarà anche possibile seguirlo a distanza collegandosi ad https://meet.google.com/ewf-nabf-zbe
Dettagli sull'evento
Data e luogo
Inizio: 08/05/2024
alle ore 17:00
Fine: 08/05/2024
alle ore 18:00
Collegio Raffaello (Urbino, Piazza della Repubblica, 13) Aula Olivetti
Organizzato e promosso da:
LAAG:IT - Logica, Algebra, Analisi, Geometria, Informatica Teorica e loro applicazioni.
