ABSTRACT. Since the early days of the termination competition, there have always been wrong answers produced by termination analysis tools. One way to increase the reliability of the generated analyses is by certification, an approach where the answers of the termination tools are checked by some verified certifier.

This talk will cover an overview of the CeTA certifier, whose soundness has been proven in Isabelle/HOL. CeTA initially only supported termination proofs of term rewrite systems. The benefit was that no theory-reasoning was required, and therefore progress was made quickly. This situation dramatically changed when adding support for integer transition systems, i.e., a backend that is often used for termination analysis of imperative programs. Here, certification of termination proofs requires to prove the validity of quantifier-free formulas over the integers. After the development of such a verified reasoning engine, we also utilize it to further extend the support for term rewriting, where we recently added support for the weighted-path order with max-polynomial interpretations.

ABSTRACT. Uniqueness of normal forms w.r.t. conversion (UNC) of term rewriting systems (TRSs) guarantees that there are no distinct convertible normal forms. It was recently shown that the UNC property of TRSs is decidable for shallow TRSs (Radcliffe et al., 2017). The existing procedure mainly consists of testing whether there exists a counterexample in a finite set of candidates; however, the procedure suffers a bottleneck of having a sheer number of such candidates. In this paper, we propose a new procedure which consists of checking a smaller number of such candidates and enumerating such candidates more efficiently. Correctness of the proposed procedure is proved and its complexity is analyzed. Furthermore, these two procedures have been implemented and it is experimentally confirmed that the proposed procedure runs much faster than the existing procedure.

ABSTRACT. Language-integrated query is a popular and powerful programming construct, which allows database queries and ordinary program code to interoperate seamlessly and safely. Language-integrated query techniques rely on classical results about monadic comprehension calculi, including the conservativity theorem for nested relational calculus. Conservativity implies that query expressions can freely use nesting and unnesting, yet as long as the query result type is a flat relation, these capabilities do not lead to an increase in expressiveness over flat relational queries. Moreover, Wong showed how such queries can be translated to SQL via a constructive rewriting algorithm, and subsequently Cooper and others advocated higher-order nested relational calculi as a basis for language-integrated queries in languages such as Links and F#. However, as we explain, there is no published proof of the central strong normalization property for higher-order nested relational queries: a previous proof attempt does not deal correctly with rewrite rules that duplicate subterms. This paper fills the gap in the literature, explaining the difficulty with a previous proof attempt, and showing how to extend the TT-lifting approach of Lindley and Stark to accommodate duplicating rewrites.

ABSTRACT. Wanda is a fully automatic termination analysis tool for higher-order term rewriting. In this paper, we will discuss the methodology used in Wanda. Most pertinently, this includes a higher-order dependency pair framework and a variation of the higher-order recursive path ordering, as well as some non-termination analysis techniques and delegation to a first-order tool. Additionally, we will discuss how to use Wanda in practice for systems in two different formalisms and present experimental results

ABSTRACT. We present a framework for symbolically executing and model checking higher-order programs with external (open) methods. We focus on the client-library paradigm and in particular we aim to check libraries with respect to any definable client. We combine traditional symbolic execution techniques with operational game semantics to build a symbolic execution semantics that captures arbitrary external behaviour. We prove the symbolic semantics to be sound and complete. This yields a bounded technique by imposing bounds on the depth of recursion and callbacks. We provide an implementation of our technique in the K framework and showcase its performance on a custom benchmark based on higher-order coding errors such as reentrancy bugs.

ABSTRACT. We introduce PHFL, a probabilistic extension of higher-order fixpoint logic. PHFL may also be regarded as a higher-order extension of probabilistic temporal logics such as PCTL and \(\mu^p\)-calculus. We show that PHFL is strictly more expressive than \(\mu^p\)-calculus, and that the PHFL model checking problem for finite Markov chains is undecidable even for the \(\mu\)-only, order-\(1\) fragment of PHFL. Furthermore, we show a translation from Lubarsky's MuArithmetic to PHFL, which implies that PHFL model checking is \(\Pi^1_1\)-hard. As a positive result, we characterize a decidable fragment of the PHFL model checking problems using a novel type system.

ABSTRACT. We extend the constructive differential game logic (\CdGL) of hybrid games with a refinement connective that relates two hybrid games. We use this connective to prove a folk theorem relating hybrid games to hybrid systems.

ABSTRACT. We study a mixture between the average case and worst case complexities of higher-order model checking, the problem of deciding whether the tree generated by a given λY-term (or equivalently, a higher-order recursion scheme) satisfies the property expressed by a given tree automaton. Higher-order model checking has recently been studied extensively in the context of higher-order program verification. Although the worst-case complexity of the problem is k-EXPTIME complete for order-k terms, various higher-order model checkers have been developed that run efficiently for typical inputs, and program verification tools have been constructed on top of them. One may, therefore, hope that higher-order model checking can be solved efficiently in the average case, despite the worst-case complexity. We provide a negative result, by showing that, under certain assumptions, for almost every term, the higher-order model checking problem specialized for the term is k-EXPTIME hard with respect to the size of automata. The proof is based on a novel intersection type system that characterizes terms that do not contain any useless subterms.

ABSTRACT. I have focused a lot of the applied side of my work over the last 20 years on formal verification of arithmetic in some sense.  Originally my main focus was on verification of floating-point algorithms for division, square root, transcendental functions etc. More recently my interests have shifted to discrete arithmetical primitives, large integer arithmetic, and elliptic curve operations. As well as many contrasts and special problems, there are a number of common themes running through all this work: the challenges of verification at the unstructured machine- code level or indeed even getting adequate specifications for machine instruction sets, the countervailing benefit of generally having clear and incontrovertible specifications of the functions themselves, and the value of special customized decision procedures in making verifications of this kind practical. I will give an overview of some of the highlights of this work, as well as talking in more detail about my current project.