Research

The Fundamental Computing group conducts cutting-edge research on the foundations of computing with a focus on the development of rigorous methods for ensuring correct and reliable software. This is a scientific and societal challenge, which we address using logic, concurrency theory, discrete mathematics, and category theory.

For the list of publications from our group, check Pure.

Formal methods for concurrency and distribution (prof.dr. Jorge Pérez)

Message-passing programs are the backbone of most distributed software infrastructures today. This theme targets the rigorous specification and analysis of these communicating programs. We specialize in specification languages based on process calculi, formal languages that express the interaction of concurrent processes. For analysis, we focus on type systems, a well-established static analysis technique able to detect errors before programs are executed. In particular, we investigate behavioral type systems, which codify the protocols that interacting processes should implement. The combination of process calculi with behavioral types results in a compositional approach to verify safety and liveness properties for communicating programs. Our recent work investigates the logical foundations of behavioral type systems: how fundamental principles such as “propositions as types” can inform the principled verification of message-passing programs.

(Co)algebraic methods in logic and semantics (prof.dr. Helle Hansen)

Logic and semantics provide the foundations for the formal analysis of software systems. Due to the vast complexity of such systems, it is essential to have appropriate abstraction techniques and methods for compositional reasoning. To this end, in this theme, we study the fundamental relationships between logic, structure and program behaviours using the methods of modal logic, algebra and coalgebra. Modal logics are widely used as specification languages in formal verification due to their good balance between expressive power and computational complexity.  Algebra is a well-established theory of compositionality. Coalgebra is a branch of applied category theory that provides a unifying framework for reasoning about the behaviours of many different types of systems, including automata, transition systems and Markov decision processes. A main contribution in coalgebra has been to show that modal logics for specifying system behaviours can be developed at the abstract level of coalgebra. Much of our work falls in the rich area of coalgebraic modal logic.

Non-classical logics and their proof theory (prof.dr. Revantha Ramanayake)

While classical (boolean) logic is the logic of truth (and logic gates), non-classical logics model a much wider range of concepts: dynamic behaviour of software programs, proofs-as-programs, resource-awareness, fuzzy reasoning, multi-agent epistemic reasoning, language grammars, and more. Proof theory is the branch of Logic that studies a logic based on a formal (mathematical) notion of its proof system and its proofs. Our research centres on non-classical logics and their proof theory. We use proof systems to prove properties of the logics, e.g. computational properties like (un)decidability and complexity, drawing on ideas from theoretical computer science and discrete mathematics. This approach relies on refined proof systems with good mathematical properties, motivating our research into their development (structural proof theory). We are also interested in automated theorem provers and automated tools (software) for non-classical logics, and the computer-formalised proofs.

Mathematical logic (prof.dr. Gerard Renardel de Lavalette)

The focus is on the proof theory of equational logic and Horn logic, and on intuitionistic logic. Intuitionism was created by L.E.J. Brouwer; its logic, formalized by A. Heyting, reappeared as the foundation of type theory with applications in programming and theorem proving. Equational logic is the formalization of algebraic equational reasoning, used in tools like Mathematica. Horn logic is the logic of formulae of the form A₁ ∧⋯∧ A_n→B; it is the basis of the logic programming language Prolog. We focus on fundamental properties like completeness (is a given proof system strong enough to prove all true statements?) and exactness (does a certain model correspond to the structure of a logic?).

Parameterized algorithms and exact exponential algorithms (dr. Ivan Bliznets)

We live in a world full of computationally challenging problems. Often, we seek algorithms that consistently produce correct solutions. To address this issue, two approaches are commonly employed: constructing exact exponential algorithms and developing fixed-parameter tractable algorithms.

In the realm of exact exponential algorithms, the primary objective is to design algorithms that compute exact solutions while optimizing performance and minimizing the exponential blow-up in running time. Dynamic programming, branch-and-bound, and measure-and-conquer techniques are widely used in this area.

Parameterized algorithms constitute a captivating field within computational complexity theory. Unlike classical complexity theory, which typically analyzes algorithm running times solely based on input size (e.g., O(n²) or O(3ⁿ)), parameterized algorithms take additional parameters into account beyond input size. These parameters often correspond to specific structural properties or characteristics of problem instances. By incorporating them, we achieve a more fine-grained complexity analysis. Consequently, this approach sometimes enables the construction of practical algorithms for real-world instances of NP-hard problems.

Automated reasoning for software-intensive systems (dr. Rodrigo Otoni)

Over the last decades software systems have made their way into virtually every area of human activity. With time, these systems became increasingly complex, in order to cater to ever more intricate application scenarios. This complexity, already significant in systems that are fully sequential, is exacerbated by concurrency and distribution, reaching a point where manual development became infeasible. To overcome this issue, we can harness the power of the same software systems to enable automated reasoning. Fundamentally, automated reasoning revolves around providing solutions to computationally hard problems, which, depending on the use case, can be NP-complete or even harder. The difficulty of such problems can be tackled by the design of innovative heuristics and the clever use of domain-specific knowledge, with these activities being the core of our work. Our research focuses on automated reasoning through the lenses of verification, synthesis, and certification.