July 18, 2024: Seminar day with silvio ghilardi, stefan merz and marco montali at the Digital Industry Center 

18 July 2024 | Sala Stringa - Online | 13:30 | Silvio Ghilardi (Università degli Studi di Milano), Stefan Merz (Inria & LORIA, Nancy, France) and Marco Montali (Free University of Bozen-Bolzano)

Programme

13:30 | Silvio Ghilardi (Università degli Studi di Milano) on "Interpolation Properties for Array Theories: Positive and Negative Results"
14:30 | Stefan Merz (Inria & LORIA, Nancy, France)  on "The TLA+ Proof System"
15:30 | break
16:00 | Marco Montali (Free University of Bozen-Bolzano)  on "Data-Aware Processes: Modelling and Verification"

***
Silvio Ghilardi | Interpolation Properties for Array Theories: Positive and Negative Results

Abstract

In this talk, we shall first review basic correspondences [2] between syntactic interpolation properties of a first order theory (quantifier-free interpolation property, general quantifier-free interpolation property, uniform quantifier-free interpolation property) and semantic properties related to the class of its models (amalgamation, strong amalgamation, model completability). Then we shall analyze these notions for variants of McCarthy extensional theory of arrays [5].

Whereas the basic theory does not have quantifier-free interpolation property, such property can be restored by adding it an extra symbol diff skolemizing the extensionality axiom [1]. General quantifier-free interpolation property also holds for this theory but not uniform quantifier-free interpolation property, as it can be shown by a counterexample.

Since the semantic content of diff operation is rather underspecified, we strenghten the theory by asking diff(a, b) to return the maximum index where two arrays a,b differ [3] (diff returns 0 if they are equal). We also add to a unary ‘length’ operation. We so end up in a theory [4] still having quantifier-free interpolation, as witnessed by a hierarchic polynomial reduction to general interpolation for linear arithmetics. General quantifier free interpolation property may fail, but can be re-gained by introducing some constant arrays in the language.

The second part of this talk comes from joint work with A. Gianola, D. Kapur, C. Naso [4]. The first part of the talk reviews old joint work with R. Bruttomesso and S. Ranise [1, 2] and adds to such old work some recent achievements.

References 

[1] Roberto Bruttomesso, Silvio Ghilardi, and Silvio Ranise. Quantifier-free interpolation of a theory of arrays. Log. Methods Comput. Sci., 8(2), 2012.

[2] Roberto Bruttomesso, Silvio Ghilardi, and Silvio Ranise. Quantifier-free interpolation in combinations of equality interpolating theories. ACM Trans. Comput. Log., 15(1):5:1–5:34, 2014.

[3] Silvio Ghilardi, Alessandro Gianola, and Deepak Kapur. Interpolation and amalgamation for arrays with maxdiff. In Stefan Kiefer and Christine Tasson, editors, Foundations of Software Science and Computation Structures - 24th International Conference, FOSSACS 2021, volume 12650 of Lecture Notes in Computer Science, pages 268–288. Springer, 2021.

[4] Silvio Ghilardi, Alessandro Gianola, Deepak Kapur, and Chiara Naso. Interpolation results for arrays with length and maxdiff. ACM Trans. Comput. Log., 24(4):28:1–28:33, 2023.

[5] John McCarthy. Towards a Mathematical Science of Computation. In IFIP Congress, pages 21–28, 1962. 

Bio
Silvio Ghilardi  graduated in Philosophy and then got a PhD in Mathematics at the Università degli Studi di Milano. He was research assistant in Algebra and Geometry, then Associate Professor and currently Full Professor in Mathematical Logic; in his career he worked both at the Computer Science and  at the  Mathematics Department of the Università degli Studi di Milano. His research interests range from modal logic, to algebraic and categorical logic, to formal methods and automated reasoning  (with special emphasis on SMT-related topics).

***

Stephan Merz |  The TLA+ Proof System 

Abstract

TLA+ is a formalism based on Zermelo-Fraenkel set theory and linear-time temporal logic for specifying algorithms. Tools for verifying properties of TLA+ specifications include the TLC explicit-state model checker, the Apalache bounded model checker, and the TLAPS proof assistant. TLAPS relies on automatic backend provers, including SMT solvers and a decision procedure for propositional temporal logic. In this talk I will describe the design of TLAPS and illustrate how it can be used for proving correctness of distributed algorithms. 

Bio
Stephan Merz obtained his PhD degree at the University of Munich (LMU) in 1992. After post-doctoral research at IRIT Toulouse and DEC SRC in Palo Alto, he was an assistant professor at LMU. Since 2002, he has been a senior researcher at Inria Nancy where he heads the VeriDis project, a joint research group between University of Lorraine, CNRS, Inria, and Max Planck Institute for Informatics in Saarbrücken. Between 2016 and 2021 he was also Head of Science at Inria Nancy. His research interests are in the formal specification and verification of software-intensive systems, and in particular of distributed algorithms. He is a regular contributor to the TLA+ language and tools, and he has been a co-organizer of the VTSA summer school since 2008. 

***
Marco Montali | Data-Aware Processes: Modelling and Verification

Abstract

The need of combining static (i.e., data-related) and dynamic (i.e., process-related) aspects has been increasingly recognized as a key milestone towards the understanding, management, and analysis of business and work processes. This has led to the development of several conceptual and formal models, striving to find a suitable equilibrium between data- and process-related aspects. In this seminar, I will overview this challenging integration problem, introducing a list of key requirements that models for data-aware processes should address. I will then focus on formal modelling and static analysis, presenting a cookbook with different recipes that mix such ingredients with increasingly complex flavors, at the same time supporting verification tasks against (first-order) state and temporal properties modulo theories. 

Bio
Marco Montali is Full Professor in the Faculty of Engineering at the Free University of Bozen-Bolzano, Italy, where he also coordinates the BSc Program in Informatics and Management of Digital Business. The Leitmotiv of his research is to develop novel, foundational and applied techniques grounded in artificial intelligence, formal methods, business process management and process mining to create intelligent agents and information systems that combine processes and data. He has served as PC Chair of BPM 2018, RuleML+RR 2019, ICPM 2020, and CBI 2021, as General Chair of ICPM 2022 and EDOC 2022, and has been steering committee member of the IEEE task force on process mining. He is co-author of more than 250 papers and recipient of 10 best paper awards and 2 test-of-time awards. He received the 2015 “Marco Somalvico” award, given by the Italian Association of Artificial Intelligence to the best under 35 Italian researcher in artificial intelligence.