 | RADU IOSIF CNRS-VERIMAG Formal Verification in the Era of Self-Adapting Networks We introduce a formal model to reason about the behaviors of self-adapting (reconfigurable) networks. The second part of the talk introduces the Separation Logic of Relations (SLR), a resource logic used to specify infinite sets of network configurations and compares the expressivity of this logic to that of well-established hypergraph description logics, such as (Monadic) Second Order logic. If time allows, we present some recent advances in the definition of the most general fragment of SLR with decidable validity (universality) and entailment (inclusion) problems. Such a fragment is key to obtaining (push-button) verification algorithms for checking the correctness of self-adapting networks. |
 | ULRICH KOHLENBACH Technische Universität Darmstadt Proof Mining: Foundations and Applications In the Proof Mining paradigm one applies proof-theoretic transformations to extract new computational information (e.g. programs or effective bounds), as well as qualitative improvements (e.g. by weakening of assumptions) from given prima facie noneffective proofs in different areas of core mathematics. This logic-based methodology makes use of so-called proof interpretations which are modern extensions and adaptions of Gödel’s famous functional (‘Dialectica’) interpretation as well as embeddings of classical reasoning into approximately constructive (‘intuitionistic’) reasoning. By these methods, noneffective proofs get translated into functional programs together with a regime to control bounding data throughout higher types by logical relations (‘majorization’). We will discuss the proof-theoretic background of this methodology and survey a few recent applications to topics in optimization which are also relevant in connection with machine learning. |
 | EUGENIO OMODEO Università degli Studi di Trieste A proof verifier rooted in Set Theory and its bottleneck This talk illustrates proof technology based on Set Theory and reports on concrete experiments carried out with the proof-checker Ref (a.k.a. ÆtnaNova). It also addresses the crucial complexity issue regarding set-theoretic inference mechanisms. Jacob T. Schwartz had a multifaceted vision of the role that set theory could play in computer science. That vision encompassed both a programming language, itself rooted in a universe of finite sets, and a proof assistant, relying on a formal theory of infinite as well as finite sets, to which mathematicians and algorithm designers could comfortably submit their proofs in order to have their correctness automatically verified. That unifying vision led to SETL, an executable algorithm specification language much ahead of its time, and — decades later — to the said system Ref. The inferential armory of an automated proof assistant based on set theory must include algorithms which, inside specific fragments of the underlying symbolic language, can establish whether or not a given formula is satisfiable in the von Neumann universe. One such decision algorithm, regarding the fragment named Multi-Level Syllogistic (in short MLS), was devised in 1979 and proliferated many others; today, an enriched variant of it plays a key role in the proof-checker Ref. Since the satisfiability problem for MLS is NP-complete, in view of the pervasiveness of its decision mechanism in actual uses of Ref, an investigation was undertaken aimed at identifying useful sublanguages of MLS whose satisfiability tests have polynomial-time worst-case complexity. The present contribution, grounded on ongoing research, also reports on a comprehensive taxonomy of polynomial and NP-complete decidable fragments of the Zermelo-Fraenkel set theory. |
 | ALICIA VILLANUEVA Universitat Politècnica de València Symbolic reasoning for the inference of specifications Varied kinds of formal specifications have been proven to be practical artifacts to assist the process of system implementation and verification. We will present two examples of how symbolic reasoning can be used to synthesize specifications from programs automatically. We applied symbolic execution to synthesize specifications for C-like programs. In this approach, we used the symbolic engine of the 𝕂 Framework as the underlying engine to derive a contract of the system that developers can easily read, which can also be an input for other tools to assist software development and maintenance. We will also show how a different approach allows us to synthesize algebraic specifications for functional programs. |