Title Promoter Affiliations Abstract "Modular formal verification of expressive low-level object-oriented programming languages" "Bart Jacobs" "Distributed and Secure Software (DistriNet)" "In this PhD project, we perform research on the theory and tool-building aspects of performing modular formal verification of safety and security properties of programs written in industrially-relevant programming languages such as C++, with the goal of making modular formal verification technology more applicable to industrial practice. Challenges include supporting C++ templates and the C++ Standard Template Library, and adding full support for treating structs or classes as values, which is not yet well-supported by existing technologies." "Exploiting Symmetry in Model Expansion for Predicate and Propositional Logic" "Marc Denecker" "Informatics Section" "Many combinatorial problems exhibit symmetry, a transformational property that does not fundamentally alter the nature of a problem. For instance, renaming a set of identical trucks in a routing problem, mirroring or rotating a chessboard onto itself, or the automorphisms of an input graph give rise to symmetry. These symmetry properties often hinder an algorithm solving a combinatorial problem, as it wastefully investigates different configurations of essentially the same solution.In this thesis, we set out to explore symmetry properties in model expansion problems for both predicate and propositional logic. The goal is to equip automated systems with the necessary tools to adequately handle symmetry. By investigating both symmetry detection and symmetry exploitation, we present symmetry exploitation techniques that rely only on problem specifications as input, without additional symmetry information. Systems equipped with these techniques are able to tackle a wider range of problems with less human input – the eventual goal of any artificial intelligence.First, we present BreakID, a novel symmetry breaking preprocessor for propositional logic. BreakID’s core idea is to investigate structural properties of the symmetry group of a problem, and to adjust any generated symmetry breaking formulas accordingly. Furthermore, we also added usability features and technical optimizations that allow symmetry detection and subsequent breaking for a broader range of propositional formulas, both in a Boolean satisfiability and an answer set programming context. Experimental results show that BreakID improves on Shatter and sbass, the previous state-of- the-art static symmetry breaking preprocessors for propositional logic.Second, we investigate two new dynamic symmetry handling algorithms for propositional solvers, based on symmetrically deriving logical consequences.The first algorithm, SP, focuses on propagating literals that are symmetrical to already propagated literals. SP is based on the notion of weak activity, a generalization of the constraint programming notion of activity. Experiments show that this approach is effective, but can be improved by also performing symmetrical propagations not based on the weak activity status of a symmetry. This leads to the second algorithm, SEL, which derives symmetrical explanation clauses and, as such, is a form of symmetrical learning. Even though SEL is a straightforward form of symmetry handling, we provide experiments that indicate it is competitive to BreakID’s advanced symmetry breaking.However, working on a propositional level burdens the algorithms that detect symmetry and derive symmetry group information, as these properties are more readily available at the predicate level. Hence thirdly, we investigate how symmetry manifests itself in first-order logic. We propose the notion of local domain symmetry, a form of symmetry in predicate logic theories that captures a broad range of symmetry groups occurring in practical problems. Based on theoretical properties of local domain symmetry, we design efficient ways of both detecting and breaking it. Our implementation in IDP outperforms other approaches in symmetry detection time, and in symmetry breaking power for problems with large row interchangeability groups. Moreover, our approach is one of the few automated approaches that detects symmetry at the predicate level. The modest price to pay is that some forms of symmetry are not captured by the notion of local domain symmetry.Finally, we establish a promising link between local search algorithms and symmetries by noting that a local search neighborhood for a problem can be constructed from its quasisymmetry group. These quasisymmetries can be automatically detected with previously established techniques, leading to a novel automated local search approach with good initial performance.Summarized, our work provides new insights in how symmetry can be detected and exploited without human interaction. These ideas, rooted in propositional and predicate logic, are useful for anyone designing automated combinatorial problem solving systems, be they affiliated with constraint programming, operations research, Boolean satisfiability solving, answer set programming, or related fields." "ERC-Opvangproject: Low-level Object Capabilities, Formally" "Dominique Devriese" "Software Languages Lab, Informatics and Applied Informatics" "Object capabilities (ocaps) are a technique for fine-grained privilege separation in programming languages, with applications in security and software engineering. Ocaps are practically used in high-level programming languages like JavaScript, but recently, there is also a renewed interest in capability machines: processors that apply ocaps at the low level of assembly languages (lowcaps). Security measures based on lowcaps offer the perspective of efficient but watertight defences against realistic attackers, that protect against arbitrary attacks, not just the ones we already know. Such measures promise to end the attack-defence arms race that plagues many current measures. In this research project, I aim to validate and demonstrate this potential, as well as deepen the scientific understanding of ocaps in general. To reach this objective, this project takes the perspective that a lowcap assembly language is just another programming language, that can be studied using powerful techniques that are developed for high-level programming languages, particularly logical relations and program logics. Using this methodology, I intend to propose, study and implement novel lowcap security measures and rigorously prove their effectiveness. On the other hand, I also intend to further study effect parametricity: a general property I proposed that formally captured the essence of ocaps. I intend to study and apply it in different contexts: for modular reasoning about ocap and lowcap code, but also in the context of functional and dependently typed programming languages, for a number of different purposes (elaborated below). This project’s results will range from novel, provably correct security measures built on lowcaps, novel methods for reasoning about such measures, but also novel insights about the nature of ocaps, the relation between object-oriented and functional code and the use of effect parametricity in dependently-typed proof assistants." "Higher Order Modelling for First Order Solvers" "Marc Denecker" "Informatics Section" "Many common computational problems can be posed as model expansion problems, where the task is to find a solution satisfying a set of constraints. Many different paradigms and approaches exist to solve these problems. Likewise, there are many languages to express these problems in. Some of these are standardized, such as Answer Set Programming (ASP) or Minizinc. For some languages there is only one system, like the FO(.) language. The language one chooses to express the problem in, has a high impact on both readability of the modelling and the efficiency of an automated solver.In this thesis we explore higher-order language constructs for modelling languages. These are generally considered very readable yet very inefficient, but in some cases this tradeoff is not so strict. This thesis is divided into three parts.The first part of the thesis focusses on the semantics of higher-order languages. Chapter 2 extends \fodot{} with templates as second-order definitions. Templates were already known as language constructs in other languages such as ASP, but their semantics were given through a rewriting process rather than giving a meaning to the templates themselves. Chapter 3 explores how logics are built and introduces infons as the basis for defining the semantics of an arbitrary language construct. Using this approach, we introduce a uniform way to extend languages with (higher-order) language constructs and define a higher-order logic with definitions.The second part of the thesis shows how existing ASP solvers can be used to solve model expansion problems posed in a higher-order language. Chapter 4 explains a translation from Programming Computable Functions (PCF) to Answer Set Programming. It then explains how this translation can handle extensions of PCF to obtain a higher-order modelling language which can be translated to ASP.Chapter 5 explains the workflow of the Functional Modelling System (FMS). This system is a prototype implementation of the language described in Chapter 4. It describes techniques for optimising modellings and how the translation phase fits in a larger system.Even the best languages are easier to use with good supportive software. In the last part of the thesis, we shift our focus away from higher-order features and introduce some tooling that was developed for the IDP3 system. Chapter 6 introduces a web-based IDE for IDP3. This IDE enables new users to easier write theories and get started with IDP.Chapter 7 introduces an interactive configuration tool which was developed to show how specifications written in Decision Model and Notation (DMN) can be used to do more than just draw conclusions from premises. It enables the user to interactively explore the solution space of a configuration problem." "New Language Constructs and Inferences for the Knowledge Base Paradigm: A Business and Multi-agent Perspective" "Marc Denecker" "Informatics Section" "In Artificial Intelligence, the scientific field of Knowledge Representation and Reasoning (KRR) is concerned with developing formal languages, to represent knowledge, and inference methods to solve tasks using that knowledge. Most of the existing approaches develop a formal language (a logic) together with an inference, to solve some type of computational task. The recently proposed Knowledge Base (KB) paradigm applies a strict separation of concerns to information and problem solving, based on the idea that knowledge is completely independent of the computational task it is used for. A KB system allows information to be stored in a knowledge base, and provides a range of inference methods, all using the same knowledge base. With these inference methods, various types of problems and tasks can be solved using the same knowledge base.In this text we study this paradigm in detail and we prove the hypothesis that this approach has many advantages over standard declarative paradigms. We use an implementation of a KB system: the IDP system with corresponding language FO(·) to model challenging and interesting applications. These applications show the need to provide extensions: we develop new language constructs and formalize new inferences.In the first part of this work, we study two applications from industry. We first look at interactive product configuration. In these interactive configuration problems, a configuration of interrelated objects under constraints is searched,where the system assists the user in reaching an intended configuration. We show that multiple functionalities in this domain can be achieved by applying different forms of inferences on a formal specification of the configuration domain.To this goal, a set of new, derived inferences are defined. A second application is the car-rental system, a prototypical example from the domain of Business Rules: rule-based systems that are used in industry for knowledge intensive applications. We investigate if all necessary knowledge can be represented in our knowledge Representation language FO(·). We propose an extension of the concept of inductive definitions in the form of a ”new“-operator to modelknowledge about situations where a new object is created, for which a good formalism was not available.In the second part, we focus on applying the ideas of the KB paradigm and the KB system IDP in a security context, by modelling Access Control applications. We use a KB system in a distributed way to verify if a certain agent has access, based on the policies of other agents. We develop a generalisation of autoepistemic logic to a distributed setting as a language for these distributed policies. Distributed autoepistemic logic (dAEL) is equipped with tools to express references to the knowledge of other agents. We study generalisations of well-known semantics of autoepistemic logic, using Approximation Fixpoint Theory (AFT). dAEL assumes complete mutual introspection between agents, every agent knows exactly what every other agent knows. This is a reasonable assumption when modelling public statements that an agent makes, but it is not reasonable for every multi-agent application.In the last part of this thesis we present another new logic: COLm , an extension of first order logic with constructs for a knowledge modality KA for each agent, a common knowledge modality C and an only knowing modality OA for each agent. We study how these modalities behave together and develop a new semantic structure that can resolve formulas of this language, without assuming any introspection." "Satisfiability and model generation in infinite space" "Gerda Janssens" "Informatics Section" "The goal of declarative programming is to represent the knowledge available in a problem domain and solve tasks using inference tools.  The FO(.)-Knowledge Base System IDP is a state-of-the-art declarative system that is unique as it comes with a multitude of inferences and allows developers to use the same information for solving very different kinds of tasks. Currently, the language and its inferences only allow for finite domains; it is not suited for computing with infinite types like unbounded numbers, lists, strings, trees, sets, etc. This limitation is currently prohibitive and the current proposal wants to rectify this.To do so, this proposal intends to bring together advantages of different logic based programming branches. SMT solvers in particular have been designed with infinite domains in mind. We will combine these techniques with the advantages of FO(.) to create a more powerful Knowledge Base System. This will require designing new language constructs and extending the inference methods to support these. As a result, the class of practical problems that can be satisfactorily tackled will be greatly extended. The results of this research are an interesting contribution to grounding based solvers in general."