Przemysław Andrzej Wałęga (Queen Mary University of London, University of Oxford)

Logic Programming With Time: DatalogMTL

The area of logic programming provides us with declarative languages, such as Datalog, which are widely used for query answering and deductive databases. During the talk, I will introduce an extension of Datalog called DatalogMTL, design for complex reasoning about data that evolves over continuous time. I will discuss the challenges introduced by the temporal dimension and show how to address them, enabling efficient reasoning mechanisms 

Break

Jinhe Ye (University of Oxford)

Some model theory of large and non-large fields

The notion of a large field was introduced by Pop in the 90s for questions such as the regular inverse Galois problems. It has been proven to be the “right class” of fields over which one can do a lot of interesting mathematics. From the model-theoretic point of view, essentially all key examples of model theoretically tame fields are large. On the other hand, key examples of non-large fields are number fields and function fields, whose model theory are not tame in general. In this talk, we will survey the concept of large fields and some of the classical results in model theory of fields. We will also talk about some recent progress in the model theory of large and non-large fields.

Amir Goharshady (University of Oxford)

The Witness-Template Approach to Program Verification

It has been well-known since the early days of computing that most problems in program verification are undecidable. The quintessential example is the termination/halting undecidability theorem of Turing, which was later extended to all non-trivial semantic properties by Rice.

To sidestep this difficulty, a prominent method is to define a notion of "witness" or "certificate" for the verification task at hand. For example, ranking functions are sound and complete witnesses for termination. In other words, a program terminates if and only if it has a ranking function. Thus, instead of trying to prove termination we can focus on the equivalent task of synthesizing a ranking function. At the first glance, this does not seem promising since the problem remains undecidable. However, having a witness concept, we can focus on synthesis of witnesses of special forms. For example, we can find linear or polynomial ranking functions. These special cases are no longer undecidable and can cover many real-world programs, such as cyber-physical systems, Blockchain smart contracts, and programs with polynomial runtime.

Based on the intuition above, this talk covers the witness-template method to verification. In the first part of the talk, we will see many examples of sound and complete witnesses for a wide variety of problems such as termination, safety, reachability, syntax-guided synthesis, quantitative probability bounds on termination/safety-violation, and LTL model-checking.

In the second part, we turn our focus to template-based synthesis of such witnesses and provide sound and semi-complete algorithms using theorems in polyhedral and real algebraic geometry.