The Colloquium of Logic is organized by the Portuguese Logic Society and aims to promote the research and knowledge in this field, from mathematical logic to philosophical logic as well as logic for artificial intelligence and theoretical computer science. The talks of the Colloquium of Logic will be held in a hybrid way. The talks will take place at the Mathematics Department of Técnico ULisboa, room 3.10, and virtually on Zoom. The next speakers are:
- Alessandro Gianola (Department of Computer Science and Engineering and INESC, Técnico ULisboa), “Uniform Interpolation in Formal Verification”, 16th May 2024, 17:00
Talk on line
Abstract: In the last two decades, Craig interpolation has emerged as an essential tool in formal verification, where first-order theories are used to express constraints on the system, such as on the datatypes manipulated by programs. Interpolants for such theories are largely exploited as an efficient method to approximate the reachable states of the system and for invariant synthesis. In this talk, we report recent results on a stronger form of interpolation, called uniform interpolation, and its connection with the notion of model completion from model-theoretic algebra. We discuss how uniform interpolants can be used in the context of formal verification of infinite-state systems to develop effective techniques for computing the reachable states in an exact way. Finally, we present some results about the transfer of uniform interpolants to theory combinations. We argue that methods based on uniform interpolation are particularly effective and computationally efficient when applied to verification of the so-called data-aware processes: these are systems where the control flow of a process can interact with a data storage.