How hard is it to verify the correctness of programs? This question is intrigues researchers who want to measure the complexity of proofs, find the fastest SAT-solver, and improve model checking tools for systems.
Satisfiability problems, SAT problems, are at the heart of many practical verification techniques. They are also a key to the famous P = NP problem. Dr Oliver Kullmann has developed theoretical underpinnings, new algorithms, and a software environment for experimentation and implementation. Regarding new theories, especially the fundamental methods for worst-case upper bounds, leading to the branch-and-conquer method, the theory of autarkies as a bridge to mathematics and combinatorics, the theory of minimal unsatisfiability as a structural theory for understanding of unsatisfiability, and, most recently, approaches for a theory of good SAT translations, are notable.
A new paradigm for SAT solving, "Cube and Conquer", has been developed and implemented by various groups. This new approach originated from interactions between SAT and Ramsey theory, especially van der Waerden numbers and the Green-Tao theorem.
The software platform, the OKlibrary, is under constant development, and provides the experimental platform, without which many discoveries wouldn't have been possible.
Bounded arithmetic and propositional proof complexity
Most of Dr Arnold Beckmann’s research is located at the interface between Mathematical Logic and Computational Complexity Theory, in particular logical descriptions of computational complexity problems via bounded arithmetic and propositional proof complexity. Dr Beckmann invented dynamic ordinal analysis by adapting ordinal analysis to bounded arithmetic. This forms the basis for his project "Abstract Measures of Low-Level Computational Complexity", which links dynamic ordinal analysis to the characterisation of total NP search problems of bounded arithmetic – part of these results have been achieved in collaboration with Dr Klaus T Aehlig (Google Munich) and Professor Sam Buss (University of California San Diego).
Dr Beckmann investigates the complexity of infinite two player games on finite graphs, by using bounded arithmetic (joint with Professor Faron Moller), and by reducing it to questions whether propositional proof systems are automatisable (in collaboration with Professor Pavel Pudlak and Neil Thapen, Czech Academy of Science, Prague). Dr Beckmann has also worked on independence results for bounded arithmetic theories with Dr Jan Johannsen (University of Munich) and lower bounds for constant depth propositional proof systems in collaboration with Professor Buss.
Computing with sets
A recent research topic on Dr Beckmann's agenda is the study of notions of feasible computation on general sets. In collaboration with Sy-David Friedman (University of Vienna) and Sam Buss (University of California San Diego) they have invented the notion of "Safe Recursive Set Functions". Safe Recursive Set Functions have an interesting behaviour on hereditarily finite sets and thus are interesting in various areas of theoretical computer science (e.g. descriptive complexity, linear logic); they exactly correspond to a notion of polynomial time for infinite time Turing machines computing on real numbers studied previously in the literature; and they also form a reasonable notion on arbitrary (infinite) sets.
Methodologically related to this are Dr Beckmann's investigations of reduction systems, in particular simple typed lambda calculus and Gödel's system T, with connections to implicit computational complexity, in collaboration with Andreas Weiermann (University of Ghent).
Infinite state automata theory
Verification tools for modelling systems typically rely on the models having finitely many states. The aim of Professor Moller’s research is to develop structural techniques that not only extend automated verification to infinite state systems (which, for instance, encode infinite data types), but also circumvent the so-called state explosion problem. Two important tools developed in this study are structural decomposition techniques and the exploitation of game-theoretic interpretations of the various verification problems.
Modal and temporal logics
Professor Moller studies various program logics for reasoning about reactive systems that have been implemented in a number of tools used effectively in the verification of practical systems. The aim of Professor Moller’s research is to characterise and interrelate the expressive power of the various logical frameworks, particularly involving fixed point logics. The main tool in this work is the use of Ehrenfeucht-Fraisse games, which characterise the semantic content of these logics.