informal Formal Methods Meetings

iFM2 is a series of informal talks held at the University of Udine on everything about Formal Methods. The series has seen a great number of talks from people all around Italy and beyond. Here you find the slides for almost all the talks held so far.

The current health crysis has forced iFM2 to stop, but it will resume very soon (virtually). Stay tuned!


Friday September 18th - 9:30 CEST (UTC+2)
Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions
Emanuele D'Osualdo
Click HERE to join!
(Microsoft Teams)

We develop a theory of decidable inductive invariants for an infinite-state variant of the Applied pi-calculus, with applications to automatic verification of stateful cryptographic protocols with unbounded sessions/nonces. Since the problem is undecidable in general, we introduce depth-bounded protocols, a strict generalisation of a class from the literature, for which our decidable analysis is sound and complete. Our core contribution is a procedure to check that an invariant is inductive, which implies that every reachable configuration satisfies it. Our invariants can capture security properties like secrecy, can be inferred automatically, and represent an independently checkable certificate of correctness. We provide a prototype implementation and we report on its performance on some textbook examples.

Past talks

7 Feb 2020
Synthesis with Binary Predicates
Pietro Sala
22 Gen 2020
Solving Infinite Games on Graphs via Quasi-Dominions
Fabio Mogavero
10 Dic 2019
An On-Line Algorithm for Reorientation of Graphs
Marta Fiori Carones
5 Nov 2019
Indexing sets of strings: Wheeler languages (part II)
Giovanna D'Agostino
29 Oct 2019
Indexing sets of strings: Wheeler languages (part I)
Alberto Policriti
5 Jul 2019
Rigorous continuous evolution of uncertain systems
Davide Bresolin
11 Jun 2019
Non-well-founded set based multi-agent epistemic action language
Francesco Fabiano
10 May 2019
Assumption-based Runtime Verification with Partial Observability and Resets
Alessandro Cimatti
12 Apr 2019
Incremental inductive verification
Luca Geatti
5 Apr 2019
Deciding weak weighted bisimulations
Marino Miculan
15 Mar 2019
On Ehrenfeucht conjecture and its applications to transducer equivalence
Gabriele Puppis
27 Feb 2019
Modal Separation Logics and Friends
Stephán Demri
15 Feb 2019
Parity-energy ATL for Qualitative and Quantitative Reasoning in MAS
Dario Della Monica
25 Gen 2019
Model checking: The interval way
Angelo Montanari