Doctoral College on Automated Reasoning
The doctoral program on Automated Reasoning (funded by the FWF) offers positions for 13 doctoral students who will work on exciting projects at the intersection of security and artificial intelligence with Automated Reasoning at the core.
The doctoral program is designed to educate the next generation of experts on Automated Reasoning. It targets foundational questions such as rigorously defining the notion of safety and security across domains and applications, the development of automated techniques and analyses to ensure safety and security of electronic systems, and explores synergies between the fields of security and artificial intelligence (see our list of potential research topics).
Doctoral students receive solid foundations spanning several of the sub-disciplines that make up the program. The interdisciplinarity of their research is ensured via close co-supervision by faculty members with complementary expertise and frequent exchange and collaboration with their colleagues (in retreats, seminars, and social events).
Program and Curriculum
The doctoral program on Automated Reasoning is a 4-year structured doctoral college in the TU Wien Informatics Doctoral School. The program is part of the doctoral college on Secure and Intelligent Human-Centric Digital Technologies (SecInt), but with a strong focus on automated reasoning and formal methods. Our list of potential research topics provides some ideas for research projects for prospective PhD students. However, the research is in no way limited to these topics.
In the following, we present the corner stones of the curriculum. More details on the structure and procedures of the doctoral school can be found on the webpage of the Doctoral School of the Faculty of Informatics and the webpage of the SecInt doctoral program.
Student Progress
- All students have to pass a proficiency evaluation within the first 18 months of their doctoral studies
- Students have to submit yearly reports, which are evaluated by two faculty members (excluding the supervisor and co-supervisor)
Coursework
- a 3 ECTS seminar on Ethics of Security and Artificial Intelligence
- 9 ECTS area courses on topics relevant to Automated Reasoning and complementing students' background
- 6 ECTS fundamental courses from the areas philosophy of science and methodologies, career planning, and research methods
Events and Workshops
During their studies, regular Colloquia and Workshops with international participation will take place, allowing students to present their research, get feedback from other students and professors, and seek for new research collaborations.
The Cybersecurity Center, the Center for Artificial Intelligence and Machine Learning, and the Vienna Cybersecurity and Privacy Research Cluster provide exciting lecture series and opportunities for scientific collaboration.
Internships
Doctoral students will be offered the opportunity of international secondments or internships with our research partners in industry and academia, exposing the students to novel ideas, different working cultures, and opening up new career perspectives. Throughout the program, students are offered mentoring and support for career planning, and workshops on innovation and entrepreneurship.
Supervisors
|
Research Topics
|
Runtime Enforcement of Hyperproperties This topic aims at synthesizing so-called enforcers that guarantee at run- time that a system satisfies a given hyperproperty. This involves designing novel formalisms to represent the properties and novel algorithms to synthesize enforcing strategies. |
|
Synthesis of Probabilistic Programs This topic combines algebraic and logical reasoning to synthesize probabilistic code fragments in order to fill “holes” in program sketches. The desired properties of the synthetic fragments will be specified using a novel formalism involving statistical moments |
|
Model Checking Algorithms for Maximum Satisfaction This research aims at novel model checking algorithms to determine an optimal valuation of system parameters such that the given system satisfies a given specification. Novel formalisms based on hyperproperties will enable us to express properties such as causality |
|
Reachability-Preserving Reasoning This research leverages contemporary decision procedures for satisfiability to reasoning over reachability. A novel notion of reachability-preserving invariants—derived from proof certificates—enables us to exploit redundancy in systems, hence increasing scalability. |
|
Dichotomy between Proofs and Solutions of SAT The goal is to investigate novel ways of model construction and proof generation in inprocessing incremental SAT solvers to enable more advanced reasoning techniques in SAT-based formal methods. |
|
Algebraic Loop Synthesis This project aims at synthesizing program loops that satisfy polynomial properties as well as given optimality criteria (such as runtime), which involves developing novel efficient techniques to reason about non-linear arithmetic constraints. |
|
Tractable Equational Reasoning The goal is to develop new automated proving procedures for first-order theories with equality, such as arithmetic. Our reasoning engines will replace ad hoc certification of safety and security properties by fast and extensible proving procedures. |
|
Program Analysis for Zero-Knowledge Protocols This research concerns the development of automated testing, program analysis, and fault localization techniques for the verification of zero-knowledge protocols (widely used in authentication, voting, and crypto-currencies). |
|
Effective Testing and Repair Techniques for Machine-Learning Models This project targets effectively testing general functional-correctness properties of machine-learning models and repairing the models under test such that they exhibit fewer property violations. |
|
Automated Cryptographic Protocol Analysis in the Complete Symbolic Attacker Model This research aims at verifying cryptographic protocols by means of a novel encoding of symbolic attacker models in first-order logic as well as dedicated first-order reasoning algorithms to solve the resulting problems. |
|
Static Analysis of Hyperproperties in DNNs This research aims at verifying cryptographic protocols by means of a novel encoding of symbolic attacker models in first-order logic as well as dedicated first-order reasoning algorithms to solve the resulting problems. |
|
Learning Theory-based Formal Verification This project investigates probabilistic testing, verification, and certification theoretically as well as in real-world practical contexts. Probably Approximately Correct bounds from learning theory based for instance on epsilon-nets will be used to derive bounds on the number of sampes needed. Practially, techniques from active search, self-supervised learning, and generative models will be trained when that number of samples is not sufficient. |
|
Knowledge Informed Certified Robustness The goal is to devise machine learning algorithms such as a novel type of or training algorithm for deep neural networks which are able to interactively incorporate automatically derived or human given domain rules. |