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.

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

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

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.

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