Our research focuses on formal methods, which are based on concepts and theories from discrete mathematics and logic.

They are applied to enhance the reliability of computer systems and computer software, and also to further the understanding of the possibilities of computing in general. The following themes are studied:

• Our research in formal methods for concurrent systems is led by Prof. Dr. Jorge A. Perez. In this theme, the main issues are specification and analysis of message-passing programs. The research in specification focuses on process calculi, formal languages that express the interaction of concurrent processes, while the research for analysis focuses on type systems for process calculi, often referred to as behavioral type systems. Behavioral types codify the protocols that channels in concurrent processes should implement. Coupling process calculi with behavioral types defines a compositional approach to verify safety and liveness properties for message-passing systems. A well-studied class of behavioral types is session types; this way, session-typed concurrency refers to a model in which interacting processes follow protocols specified as session types.
• Our research in mathematical logic is led by Prof. Dr. Gerard R. 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_1 \wedge \dots \wedge A_n \rightarrow 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?).