Computing Logic and Reasoning

Logic

Logic is the study of statements of facts: how they can be combined, translated, derived and analysed. It includes what the mathematical properties of logics are, and what forms of reasoning are needed to model different kinds of systems.

Our experts study substructural and categorical logics, probabilistic systems, nominal systems and specialised systems for reasoning in particular application domains. We have particular expertise in understanding logics as mathematical structures, and in their use in verification. A key concern is logics that can be used in practice for automated reasoning, for example monadic second-order logic and logics with probability can become too complex, and one needs to identify feasible fragments.

Probabilistic Reasoning

Probabilistic analyses are core to understanding modern systems at many levels. Useful analysis requires working computationally with classes of distributions and not simply the likelihoods of individual events. Our researchers are working on probabilistic programming languages and algorithms, using probabilistic tools to analyse the behaviour of conventional systems.  We use stochastic games on graphs to model process controllers, entropy and information theory to quantify the information leakage from and hence security of programs, and innovative probabilistic AI-linked methods to generate the pseudo-random number generators used in cryptography.

Verification

The foremost concern in the design and implementation of any software system is correctness: does it actually do what you intend it to do? Verification addresses two problems:

• How can we formally describe the properties we want the system to have?
• How can we prove that our system has them?

And for practical use there is also a third:

• How can this be seamlessly integrated into the code development process?

Our researchers study a range of formal methods of software development and their application to real-world systems. These include:

• Session types: the specification and verification of communication protocols for concurrent and distributed computing based on type systems.
• Separation logic: this was the first logic to be used regularly on the entire code-bases of major companies to locate and eliminate memory violations.
• Game semantics: the use of game semantics as a verification framework for higher-order programming with effects.

Logic-translations - author Paulo Oliva (with permission)

Stochastic-games - author Kelmendi with permission