The project will focus on developing symbolic computation algorithms for the analysis of program loops with numeric and unbounded data structures, as well as probabilistic features. For doing so, computer algebra techniques in combination with statistical method will be designed to analyze safety and liveness properties of emerging applications of programming languages, such as synthesizing probabilistic loops from the value distributions of program variables and inferring tight bounds on the expected runtimes of probabilistic programs.

Preferences are a crucial element in formalisations of argumentation scenarios. In this project, we aim to incorporate a recently proposed general framework for preference handling [1] to argumentation formalisms. Such preferences can be applied at different points in the evaluation process: one approach would be to rank outcomes of argumentation frameworks; another app roach is to rank possible completions of incomplete argumentation frameworks [2].

[1] Michael Bernreiter, Jan Maly, Stefan Woltran: Choice Logics and Their Computational Properties. Accepted for IJCAI’21.
[2] Dorothea Baumeister, Matti Järvisalo, Daniel Neugebauer, Andreas Niskanen, Jörg Rothe: Acceptance in incomplete argumentation frameworks. Artif. Intell. 295: 103470 (2021).

Notions of equivalence between logic programs constitute central a theoretical tool to understand concepts like program simplification. While several such notions have been studied in the literature (e.g., [1]), recent developments like forgetting [2] or abstraction call for refined notions of equivalence. The overall goal in this project to define such notions and explore suitable logical characterisations.

[1] Stefan Woltran: A common view on strong, uniform, and other notions of equivalence in answer-set programming. Theory Pract. Log. Program. 8(2): 217-234 (2008)
[2] Ricardo Gonçalves, Matthias Knorr, João Leite, Stefan Woltran: On the limits of forgetting in Answer Set Programming. Artif. Intell. 286: 103307 (2020)

The project will focus on obtaining an in-depth understanding of the parameterized complexity of prominent problems that arise in artificial intelligence research and in related areas. The pursued topics and general approaches may, for instance, follow a similar direction as the following recent publications:

[1] Robert Ganian, Sebastian Ordyniak: The complexity landscape of decompositional parameters for ILP. Artif. Intell. 257: 61-71 (2018).
[2] Robert Ganian, Thekla Hamm, Guillaume Mescoff: The Complexity Landscape of Resource-Constrained Scheduling. IJCAI 2020: 1741-1747.

The project will target new fixed-parameter algorithms and algorithmic lower bounds for fundamental problems in theoretical computer science. The focus will lie on techniques that utilize structural parameters of an input graph.

Example papers:
[1] Robert Ganian, Fabian Klute, Sebastian Ordyniak: On Structural Parameterizations of the Bounded-Degree Vertex Deletion Problem. Algorithmica 83(1): 297-336 (2021)
[2] Eduard Eiben, Robert Ganian, Thekla Hamm, Fabian Klute, Martin Nöllenburg: Extending Partial 1-Planar Drawings. ICALP 2020: 43:1-43:19

Probabilistic programs (PPs) are now gaining momentum due to the several emerging applications in the areas of machine learning and artificial intelligence. High-tech giants, such as Google, Microsoft and Uber, have started to develop their own probabilistic programming languages that include native constructs for sampling distributions, enabling the programmer to freely mix deterministic and stochastic elements. This programming paradigm offers a unifying framework for encoding probabilistic machine learning models, such as Bayesian networks, with decision making routines used, for example, in autonomous parking. One of the main problems that arise from introducing randomness into the program is that we can no longer view variables as single values, but as distributions of values. Dealing with distributions is far more complex and some simplifications and approximations are necessary. The resulting flexible framework comes at the price of programs with behaviors hard to analyze, leading to unpredictable consequences in safety-critical applications, such as in autonomous driving. This research project consists in developing new automated techniques to analyse probabilistic programs (e.g. proving termination, learning invariants, verifying safety condition) or to automatically synthesize probabilistic programs satisfying certain properties.

Preliminary work of the supervisors:
[1] M. Moosbrugger, E. Bartocci, J.-P. Katoen, L. Kovacs: Automated Termination Analysis of Polynomial Probabilistic Programs. In Proc. of ESOP 2021: the 30th European Symposium on Programming, vol. 12648, pp. 491–518, 2021, doi: 10.1007/978-3-030-72019-3_18
[2] E. Bartocci, L. Kovacs, M. Stankovic: Analysis of Bayesian Networks via Prob-Solvable Loops. In Proc. of ICTAC 2020: International Colloquium on Theoretical Aspects of Computing, vol. 12545, pp. 221–241, 2020, doi: 10.1007/978-3-030-64276-1_12
[3] E. Bartocci, L. Kovacs, M. Stankovic: MORA – Automatic Generation of Moment-Based Invariant, In Proc. of TACAS 2020: the 26th Intern. Conference on Tools and Algorithms for the Construction and Analysis of Systems, vol. 12078, pp. 492–498, 2020, doi: 10.1007/978-3-030-45190-5_28
[4] E. Bartocci, L. Kovacs, M. Stankovic: Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops, In Proc. of ATVA 2019: the 17th Intern. Conference on Automated Technology for Verification and Analysis, vol. 11724, pp. 69–86, 2019, doi: 10.1007/978-3-030-59152-6

Debugging Cyber-Physical Systems (CPS) is a cumbersome and costly activity. CPS models combine continuous and discrete dynamics. A fault in a physical component manifests itself in a very different way than a fault in a state machine. Furthermore, faults can propagate both in time and space before they can be detected at the observable interface of the model. In recent work we have investigated fault localization [1] and failure explanation techniques [2] for Simulink/Stateflow diagrams of cyber-physical systems. The main idea of our approach is to combine testing [3], specification mining [4,5], and failure analysis to automatically explain failures supporting the debugging activities. This research project aims at further developing these techniques and going beyond them by automatically proposing possible repair solutions to the engineer.

[1] E. Bartocci, T. Ferrère, N. Manjunath, D. Nickovic: Localizing Faults in Simulink/Stateflow Models with STL. Proc. of HSCC 2018: 197-206, doi: 10.1145/3178126.3178131
[2] E. Bartocci, N. Manjunath, L. Mariani, et al. CPS Debug: Automatic failure explanation in CPS models. Int J Softw Tools Technol Transfer (2021), doi: 10.1007/s10009-020-00599-4
[3] E. Bartocci, R. Bloem, B. Maderbacher, N. Manjunath, D. Nickovic: Adaptive Testing for Specification Coverage in CPS Models, In Proc. of ADHS: the 7th IFAC Conference on Analysis and Design of Hybrid Systems, 2021 (preprint: https://arxiv.org/abs/2010.06674)
[4] E. Bartocci, J. Deshmukh, F. Gliger, C. Mateis, D. Nickovic, X. Qin: Mining Shape Expressions from Positive Examples, In IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 39(11), pp. 3809 -20, 2020, doi: 10.1109/TCAD.2020.3012240 [5] L. Nenzi, S. Silvetti, E. Bartocci, L. Bortolussi: A Robust Genetic Algorithm for Learning Temporal Specifications from Data, In Proc. of QEST 2018: the 15th International Conference on Quantitative Evaluation of SysTems, vol. 11024, pp. 323–338, 2018, doi: 10.1007/978-3-319-99154-2_20

Hyperproperties extend the conventional notion of trace properties from a set of traces to a set of sets of traces. Many interesting requirements in computing systems are hyperproperties and cannot be expressed by trace properties. Examples include (1) a wide range of information-flow security policies such as noninterference and observational determinism (2) sensitivity and robustness requirements in cyber-physical systems and consistency conditions such as linearizability in concurrent data structures. Hyperproperties can describe the requirements of probabilistic systems as well. They generally express probabilistic relations between multiple executions of a system. For example, in information-flow security, adding probabilities is motivated by establishing a connection between information theory and information flow across multiple traces. A prominent example is probabilistic schedulers that open up an opportunity for an attacker to set up a probabilistic covert channel. Or, probabilistic causation compares the probability of occurrence of an effect between scenarios where the cause is or is not present. This research project aims at developing new automated and possibly scalable exact or approximate techniques to verify probabilistic hyperproperties over different classes of probabilistic models ranging from Markov Decision Processes to Stochastic games.

Previous work of the supervisor:
[1] E. Ábrahám, E. Bartocci, B. Bonakdarpour, O. Dobe: Probabilistic Hyperproperties with Nondeterminism. ATVA 2020: 518-534, doi: 10.1007/978-3-030-59152-6
[2] E. Ábrahám, E. Bartocci, B. Bonakdarpour, O. Dobe: Parameter Synthesis for Probabilistic Hyperproperties. LPAR 2020: 12-31, doi: 10.1007/978-3-030-64276-1_12

Autonomous agents must  possess the ability to adapt to (potentially unpredictable) changes in their environment. Machine learning techniques such as reinforcement learning (RL) haven proven successful methods for teaching agents this behaviour. However, when supporting humans, AI agents should restrict their own action to the ethical standards recognized in fundamental right and ethical theories, introducing a requirement for ethical reasoning.  RL has been employed to enforce such standards as well; agents can be trained to act in line with further rewards/penalties assigned according to the performance of ethical/unethical behaviour through a reward function. However, this does not provide a guarantee of the desired behaviour. Moreover, such techniques are not well equipped to handle the complexities of ethical reasoning. In general, like other black-box machine learning methods, RL cannot transparently explain why a certain policy is compliant or not. Additionally, when the ethical values are embedded in the learning process, a small change in their definition would require us to retrain the policy from scratch. This project aims at investigating how to embed normative reasoning techniques with the machine learning components responsible for the decision making, thus combing symbolic and sub-symbolic AI.

[1] Emery Neufeld, Ezio Bartocci, Agata Ciabattoni, Guido Governatori: A Normative Supervisor for Reinforcement Learning Agents. CADE 2021: 565-576, doi: 10.1007/978-3-030-79876-5_32

There are many open problems in Discrete Mathematics, including Extremal Graph Theory, Ramsey Theory, and Design Theory, where one is interested in finding smallest examples or counterexamples to conjectures. Since the search space grows quickly with the size of the objects, advanced symmetry-breaking methods are essential. This project combines symmetry-breaking with SAT-based methods.

Relevant literature:
[1] Michael Codish, Alice Miller, Patrick Prosser, Peter J. Stuckey: Constraints for symmetry breaking in graph representation. Constraints, an Int. J. 24(1): 1-24 (2019).
[2] Tomás Peitl, Stefan Szeider: Finding the Hardest Formulas for Resolution. Journal Artificial Intelligence Research, volume 72, pages 69–97, 2021.

This project aims to utilize recent SAT-solving progress to tackle problems that arise in Computational Social Choice, such as the aggregation of preferences of multiple agents or the prevention of rigged elections. The work includes theoretical investigations combined with experimental evaluation on real-world data.

Relevant literature:
[1] Ulle Endriss: Analysis of One-to-One Matching Mechanisms via SAT Solving: Impossibilities for Universal Axioms. AAAI 2020: 1918-1925.
[2] André Schidler, Stefan Szeider: SAT-based Decision Tree Learning for Large Data Sets. AAAI 2021: 3904-3912.

This project analyzes subsymbolic machine learning models, such as neural networks, with symbolic tools like SAT solvers. The aim is to replace opaque models with explainable and verifiable models, easily checked for bias.

Relevant literature:
[1] Alexey Ignatiev, Nina Narodytska, João Marques-Silva: Abduction-Based Explanations for Machine Learning Models. AAAI 2019: 1511-1519.
[2] Christoph Molnar: Interpretable machine learning. A Guide for Making Black Box Models Explainable, 2019.
[3] André Schidler, Stefan Szeider: SAT-based Decision Tree Learning for Large Data Sets. AAAI 2021: 3904-3912.

Many computational problems that arise in Artificial Intelligence and Combinatorial Optimization are intractable. Nevertheless, efficient, practical algorithms have been developed that exploit the hidden structure of problem instances that arise from real-world applications. This project aims at utilizing recent progress in Machine Learning to speed up such solving algorithms.

Relevant literature:
[1] Yoshua Bengio, Andrea Lodi, Antoine Prouvost: Machine learning for combinatorial optimization: A methodological tour d’horizon. Eur. J. Oper. Res. 290(2): 405-421 (2021)
[2] Jia Hui Liang, Vijay Ganesh, Pascal Poupart, Krzysztof Czarnecki: Learning Rate Based Branching Heuristic for SAT Solvers. SAT 2016: 123-140
[3] Holger H. Hoos, Tomás Peitl, Friedrich Slivovsky, Stefan Szeider: Portfolio-Based Algorithm Selection for Circuit QBFs. CP 2018: 195-209

Proofs of security and privacy are extremely complex and error prone and the most popular protocols, applications, and services are regularly affected by bugs and vulnerabilities. This state of affairs calls for the design of formal methods for the enforcement of rigorous security and privacy properties in complex, large scale systems. A central challenge in this field is to strive for the sweet spot between automation and expressiveness. Target application domains include web applications, smart contracts, blockchain protocols, and learning-based systems.

[1] EThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts. Schneidewind, Grischchenko, Scherer, Maffei. ACM CCS’20: 621-640

Norms are enormously important in a variety of fields, including law, emergency management and AI. The application of norms inevitably leads to deontic conflicts and deciding which norms override which other norms is often controversial. This project investigates conflict resolution methods for normative reasoning and aims to develop effective tools usable in application domains. As our main source of inspiration, we look at ways of dealing with normative reasoning that diverge from the contemporary European and Anglo-American approaches, thereby questioning implicit cultural biases in dealing with deontic conflicts. The various legal and philosophica ltraditions we will examine will be applied to real-world reasoning scenarios coming from contemporary ethical debates and normative AI cases. 

https://mimamsa.logic.at 

Logics different from classical logics (Non classical logics) provide adequate formalisms for reasoning, e.g., about time, norms, knowledge, dynamic data structures, vague information and resources. As such, these logics have been increasingly applied in various disciplines including artificial intelligence, philosophy, and in computer science, where most of these logics originate.

Non classical logics are usually introduced or described in a declarative way in the proof framework due to Hilbert and Frege. However, the resulting systems are extremely cumbersome when it comes to finding or analyzing proofs and for proving properties of the formalized logics. These tasks call for algorithmic presentations of the logics especially in the form of analytic calculi. Analyticity is crucial here since proofs in such calculi proceed by a stepwise decomposition of the objects to be proved.

The aim of this project is to advance the methods for the automated introduction of analytic calculi for non-classical logics, and their exploitation. 

The interpretation and application of norms have traditionally been the reserve of law and morality. Both of these areas have developed a number of methods, which are often not formally specified. Recently, especially in connection with the growth of Artificial Intelligence (AI) which is making autonomous systems mainstream, norms have become of central interest also for formal disciplines such as Logic and Computer Science.

As the real word is not predictable and unforeseen situations might arise,AI systems should be equipped with the ability to reason with and about norms. The aim of this project is to provide novel methods to achieve that, i.e., methods that will enable AI systems to comply not only with precise legal rules and deal with explicit exceptions, but also to reflect upon rules, assessing the impact of the rulesʼ application on the relevant values and provide appropriate corrections. 

Software and hardware is widely acknowledged to be full of bugs. Despite decades-long efforts, formal verification hasn’t fufilled the promise of providing us with correct-by-construction or provenly correct systems. Hence, this project focuses on formal falsification: automated testing and the automated detection of bugs in software and hardware. We target a broad range of bugs, including bugs in concurrent and distributed systems, security bugs, but also bugs in machine learning-based systems. The goal is to provide automated techniques that provide formal guarantees.

Model Checking is a technique to automatically check whether a given system (model) satisfies a property. Model checking has been successfully applied to hardware as well as software. Many successful model checking algorithms are based on satisfiability solvers, taking advantage of the huge strides made in this field in the last two decades. This project focuses on the tight integration and similarities of contemporary model checking algorithms and satisfiability solvers, exploiting and lifting the latest and most promising advances in automated solving to model checking.

Determining the resource consumption of a program (e.g., runtime, heap usage) is an integral part during the design and analysis of a program. In this project we are interested in static analysis techniques that allow deriving upper bounds on the resource consumption of a program. Techniques of interest include ranking functions, potential functions, program invariants, Hoare logic, assume-garantuee reasoning, etc. Further we are interested in decidabilty results on the resource consumption of foundational computing models such as Petri nets and counter automata.

Data structures in imperative programs are typically manipulated via pointers. The verification of such programs requires adequate logics that allow describing the shape and the current state of the data structure. In order to automate reasoning we are intersted in logics with decidable satisfiability and entailment problems. In this project we will study suitable logics, such as separation logic, and develop automated decision procedures. Moreover, we are intersted in static analysis techniques that derive program invariants, expressed in the considered logics, fully-automatically.

Present day computing witnesses a swift change of view between a single program running on a computer to a complex system, such as a cloud, an autonomous car or a cryptocurrency. This project aims at providing logical tools for the design and verification of such systems, using the principle of local reasoning: a state change, either internal or a reconfiguration, involves a limited resource, the rest of the system remaining unchanged. We plan to design logics for reasoning about such reconfigurable systems and automate these logics by new (semi-)decision procedures integrated with compositional push-button verification methods, that guarantee behavioral correctness.

Description Logics (DLs) are a versatile family of languages for knowledge representation, with efficient automated reasoning engines and many succesful applications. However, state-of-the-art technologies have extremely limited capabilties to reason with numeric values. As the latter are crucial in many potential applciations, major research efforts have aimed at enriching DLs with the ability to associate numeric values to logical objects (e.g., by the so called concrete domains), and to express numeric constraints both on such values and on the sizes of the extensions of classes and relations. Many promising solutions are emerging, but so far research is dominated by techniques that are good for establishing decidablity and complexity results, but poorly suited as the basis of such implementations. The goal of this project is to develop novel algorithms that can underpin DL engines with numeric reasoning support, mostly by translations into formalisms with efficeint solvers like integer linear programming and satisfiability module theories.

The urgency of accurate yet interpretable ML classifiers has resulted in many techniques for approximating and explaning systems by means of decision rules, decision trees, and similar interpretables model classes. Some of these approximation techniques use ad-hoc domain ontologies and very simple ontological reasoning to guide the constrcution of these explainable models, for example, to prioritize more informative features over less informative ones. This project will contribute to understanding the limits and possibilities of extracting knowledge from existing ontologies and using it to improve explainable classifiers.

Stream reasoning is a topic of growing importance. It is in partciular challenging if multiple entities (agents) have to process and to exchange information resulting in streams, and if real-time settings play a role. While some proposals for semantics of systems of entities agents exist, there is room for improvement to take various features (numeric uncertainy, realibility, learning) etc. into account, in particular, if declarative methodes are used for describing the behaviour of the entities.

Answer Set Programming is a successful declarative problem solving paradigm that has been deployed to many application fields. In order to enlarge its applicability, Answer Set Programming has been extended and combined with other problem solving methods, among them SAT and SMT solving, imperative programming, constraint programming etc. Recently, there has been a strong interest in combining Answer Set Programming with Machine Learning, leading to neuro-symbolic computation models that integrate neural networks with rules, or apply reinfocement learning to rules and program evalution, or use Answer Set Programming to guide learning. In this project, the Hybrid ASP approach will be further extended, and novel integration, algorithms, and applications will be considered.

Symbolic formalisms, among them mixed integer programming, constraint solving, SAT solving and answer set programming, have been successfully used for describing and solving scheduling problems in different applications domains.
However, the (non)existence of solutions is not always clear, and in case of optimization aspects that may lead to (non-)optimality. Abduction is a well-known mechanism in order to find explanations of unexpected observations. In this project, the use of abduction for making scheduling results more explainable to users will be explored.

Drawing inferences and conclusions in general depends on the context in which a reasoner is situated; e.g., cheering to a goal of your team is natural in general, but may be inappropriate if you are in the stadium among hooligans favouring the opponents. Dealing with context often requires to deal with ambiguity and possibly overriding of information due to inheritance from more general to specific settings. Furthermore, contexts might come in different aspects, like time, space etc. (above, when we are watching a match, and where).
This project will explore challenges that come from such a setting, which leads to multi-objective optimisation problems. A possible starting point are context-knowledge repositories, which are a versatile formalisms based on description logics. In particular, providing semantics, studying complexity of inference (which besides classical query answering might also include what-if questions), developing efficient algorithms and addressing applications would be on the agenda.