Logic and Computation (L+C)
We make machines reason correctly. Connecting formal logic, algorithms, and complexity theory to understand how computation works, verify that systems behave as intended, and push the boundaries of what computers can solve efficiently.
Committed to society.
Logic is the foundation of computer science. Every computation can be understood as a process of logical inference, making logic essential for designing algorithms, verifying software and hardware, securing digital systems, and advancing artificial intelligence. At the Logic and Computation (L+C) research focus, we develop the mathematical foundations and computational methods that ensure complex systems behave correctly while exploring the limits of what can be computed efficiently.
We are internationally recognized as one of the leading centres for logic and computation, combining fundamental research with world-class software and lasting scientific impact. Building one of Europe’s strongest research and graduate training environments, we’re educating more than 80 PhD graduates. Through collaborations our work shapes trustworthy computing in both academia and industry, among our partners are Amazon Web Services, Bosch, Frequentis, Honda Research Institute Europe, Honda Motor Co Ltd, Microsoft Research, MCP GmBH, Siemens, and Ximes.
Powered by community.
We turn the foundations of reasoning into powerful tools, advancing trustworthy AI and computation from theory to practice.
Professors
Uwe Egly U. Egly
Knowledge-Based Systems
Retired Professor
Alexander Leitsch A. Leitsch
Theory and Logic
Retired Professor
Katalin Fazekas K. Fazekas
Formal Methods in Systems Engineering
Assistant Professor
Scientific Staff
Martin Riener M. Riener
Theory and Logic
Senior Lecturer
Sebastian Skritek S. Skritek
Databases and Artificial Intelligence
Senior Lecturer
Henri Thölke H. Thölke
Theory and Logic
PreDoc Researcher
Sebastian Johannes Lüderssen S. Lüderssen
Machine Learning
PreDoc Researcher
Marlene Gründel M. Gründel
Algorithms and Complexity
PreDoc Researcher
Manuel Sorge M. Sorge
Algorithms and Complexity
PostDoc Researcher
Adrian Chroust A. Chroust
Knowledge-Based Systems
PreDoc Researcher
Geoffrey Charles Joseph Sutcliffe G. Sutcliffe
Formal Methods in Systems Engineering
PostDoc Researcher
Sandford Bessler S. Bessler
Compilers and Languages
Affiliated
Sara Di Bartolomeo S. Di Bartolomeo
Algorithms and Complexity
PostDoc Researcher
Markus Fleischmann M. Fleischmann
Software Engineering
PreDoc Researcher
Dedicated to excellence.
Big questions deserve high standards. Our award-winning research shows that we are pushing the limits. Here is what we have been working on.
Below is some of our recent work.
Want more?
Head over to our research unit pages!
Recent Projects
- 2027 – 2031 / European Commission
- 2026 – 2030 / Austrian Science Fund (FWF)
- 2025 – 2029 / Austrian Science Fund (FWF)
- 2024 – 2029 / Austrian Science Fund (FWF) / Publication
- 2026 – 2028 / LaCS
- 2025 – 2028 / Austrian Science Fund (FWF) / Publication
- 2024 – 2028 / Vienna Science and Technology Fund (WWTF) / Website / Publication
- 2024 – 2028 / Austrian Science Fund (FWF) / Publications (26)
- 2025 – 2027 / Austrian Science Fund (FWF) / Publications (2)
- 2024 – 2027 / Austrian Science Fund (FWF) / Website / Publications (8)
- 2023 – 2027 / Austrian Science Fund (FWF) / Website
- 2023 – 2027 / Honda Research Institute Europe Gmb / Publications (9)
- 2023 – 2027 / Vienna Science and Technology Fund (WWTF) / Publications (9)
- 2023 – 2027 / Vienna Science and Technology Fund (WWTF) / Website / Publications (7)
- 2019 – 2027 / Vienna Science and Technology Fund (WWTF) / Publications (4)
- 2025 – 2026 / SBA Research gemeinnützige GmbH / Publications (2)
- 2025 – 2026 / European Commission / Publications (5)
- 2025 – 2026 / Sui Foundation
- 2024 – 2026 / WWTF Wiener Wissenschafts-, Forschu und Technologiefonds
- 2022 – 2026 / Honda Research Institute Europe Gmb / Publications (7)
Recent Publications
- Fazekas, K., Heule, M. J. H., Iser, A. (Eds.). (2026). Proceedings of SAT Competition 2026 : Solver and Benchmark Descriptions.DOI: 10.34726/12919 / Download: PDF
- Aumayr, L., Avarikioti, Z., Karakostas, D., Kreder, K., Shastry, S. (2026). Optimal Reward Allocation via Proportional Splitting. In A. Kiayias M. Kyropoulou (Eds.), 8th Conference on Advances in Financial Technologies (AFT 2026). Schloss Dagstuhl – Leibniz-Zentrum für Informatik. Peer-reviewed.DOI: 10.4230/LIPIcs.AFT.2026.30 / Download: PDF
- Deligkas, A., Eiben, E., Ganian, R., Hamm, T., Ordyniak, S. (2026). The complexity of envy-free graph cutting. Artificial Intelligence, 358, Article 104585. Peer-reviewed.
- Kovacs, L. (2026). The Vampire Diary. In B. Dutertre B. Könighofer (Eds.), Proceedings of the 26th Conference on Formal Methods in Computer-Aided Design – FMCAD 2026 (pp. 4–4). TU Wien Academic Press. Peer-reviewed.DOI: 10.34727/2026/isbn.978-3-85448-093-8_4 / Download: PDF
- Kafshdar Goharshady, A., Hader, T., Kovacs, L., Motwani, H. J. (2026). Randomized Satisfiability Checking for Non-Linear Arithmetic over Finite Fields. In B. Dutertre B. Könighofer (Eds.), Proceedings of the 26th Conference on Formal Methods in Computer-Aided Design – FMCAD 2026 (pp. 84–93). TU Wien Academic Press. Peer-reviewed.DOI: 10.34727/2026/isbn.978-3-85448-093-8_14 / Download: PDF
- Saccomani, P., Mohamed, A., Pertseva, E., Kaufmann, D., Tinelli, C., Barrett, C., Barbosa, H. (2026). Proof Production for Satisfiability Modulo Finite Fields with Proof Checking in Pacheck and Lean. In B. Dutertre B. Könighofer (Eds.), Proceedings of the 26th Conference on Formal Methods in Computer-Aided Design – FMCAD 2026 (pp. 113–123). TU Wien Academic Press. Peer-reviewed.DOI: 10.34727/2026/isbn.978-3-85448-093-8_17 / Download: PDF
- Ferdowsi, A., Kovacs, L. (2026). Certificate-Aware Property-Directed Reachability. In B. Dutertre B. Könighofer (Eds.), Proceedings of the 26th Conference on Formal Methods in Computer-Aided Design – FMCAD 2026 (pp. 414–425). TU Wien Academic Press. Peer-reviewed.DOI: 10.34727/2026/isbn.978-3-85448-093-8_46 / Download: PDF
- Ceylan, E., Chen, J., Roy, S. (2026). Optimal seat arrangement: What are the hard and easy cases? Journal of Computer and System Sciences, 160, Article 103779. Peer-reviewed.
- Chen, J., Niedermeier, R., Skowron, P. (2026). Stable marriage with multi-modal preferences. Journal of Computer and System Sciences, 160, Article 103778. Peer-reviewed.
- Bresich, M., Peng, J., Raidl, G. R., Limmer, S. (2026). Determining Destroy Sets in Large Neighborhood Search by Generative Flow Networks. In G. Iacca, G. Nadizar, A. Yaman, D. Bucur, A. Della Cioppa, T. Hu, E. Medvet, S. L. Thomson (Eds.), Parallel Problem Solving from Nature – PPSN XIX : 19th International Conference, PPSN 2026, Trento, Italy, August 29 – September 2, 2026, Proceedings, Part I (pp. 265–281). Springer. Peer-reviewed.
- Iurlano, E., Raidl, G. R. (2026). SAT-Based Search for Minwise Independent Families. In G. Iacca, G. Nadizar, A. Yaman, D. Bucur, A. Della Cioppa, T. Hu, E. Medvet, S. L. Thomson (Eds.), Parallel Problem Solving from Nature – PPSN XIX : 19th International Conference, PPSN 2026, Trento, Italy, August 29 – September 2, 2026, Proceedings, Part I (pp. 433–449). Springer Cham. Peer-reviewed.
- Šimkus, M. (2026). A Definitional Fragment of Temporal Equilibrium Logic: from Temporal Programs to Compact Automata. In A. Ozaki N. Potyka (Eds.), Non-Monotonic Reasoning 2026 : Proceedings of the 24th International Workshop on Non-Monotonic Reasoning (NMR 2026) co-located with the 23rd International Conference on Principles of Knowledge Representation and Reasoning (KR 2026) at the Federated Logic Conference 2026 (FLoC 2026). CEUR-WS.org. Peer-reviewed.
- Haldimann, J., Šimkus, M., Meyer, T. (2026). Towards Defeasible Reasoning about Actions and Their Effects. In A. Ozaki N. Potyka (Eds.), Non-Monotonic Reasoning 2026 : Proceedings of the 24th International Workshop on Non-Monotonic Reasoning (NMR 2026) co-located with the 23rd International Conference on Principles of Knowledge Representation and Reasoning (KR 2026) at the Federated Logic Conference 2026 (FLoC 2026). CEUR-WS.org. Peer-reviewed.
- Buraglio, G., Di Stefano, F., Šimkus, M. (2026). Semantics for Description Logics via Assumption-Based Argumentation: Preliminary Results. In A. Ozaki N. Potyka (Eds.), Non-Monotonic Reasoning 2026 : Proceedings of the 24th International Workshop on Non-Monotonic Reasoning (NMR 2026) co-located with the 23rd International Conference on Principles of Knowledge Representation and Reasoning (KR 2026) at the Federated Logic Conference 2026 (FLoC 2026). CEUR-WS.org. Peer-reviewed.
- Almeida, J., Limmer, S., Soares, J., Bresich, M., Raidl, G., Vale, Z. (2026). Dataset of electric autonomous dial-a-ride instances with local energy communities and electricity tariffs. Data in Brief, 67, Article 113063. Peer-reviewed.
- Hajdu, M., Hozzová, P., Kovács, L., Wagner, E. M. (2026). Completeness of Synthesis Under Realizability Assumptions Using Superposition. In A. Biere, C. Lutz, S. Negri (Eds.), Automated Reasoning : 13th International Joint Conference, IJCAR 2026, Lisbon, Portugal, July 26–29, 2026, Proceedings, Part I (pp. 22–40). Springer Cham. Peer-reviewed.
- Köll, C., Ciabattoni, A., Rozplokhas, D. (2026). SMT-Based Deontic Reasoning for Åqvist Logics. In A. Biere, C. Lutz, S. Negri (Eds.), Automated Reasoning : 13th International Joint Conference, IJCAR 2026, Lisbon, Portugal, July 26–29, 2026, Proceedings, Part I (pp. 455–464). Springer Cham. Peer-reviewed.
- Hofstadler, C., Kaufmann, D., Chen, C. (2026). Avoiding Big Integers: Parallel Multimodular Algebraic Verification of Arithmetic Circuits. In A. Biere, C. Lutz, S. Negri (Eds.), Automated Reasoning : 13th International Joint Conference, IJCAR 2026, Lisbon, Portugal, July 26–29, 2026, Proceedings, Part I (pp. 175–193). Springer Cham. Peer-reviewed.DOI: 10.1007/978-3-032-32589-1_11 / Project: CalgSAT
- Oudshoorn, A. M., Ortiz, M., Šimkus, M. (2026). Static Analysis of Recursive SHACL. In R. Wassermann, M. Mugnier, F. Baader (Eds.), Proceedings of the TwentyThird International Conference on Principles of Knowledge Representation and Reasoning : KR meets Machine Learning and Explanation (pp. 523–533). IJCAI Organization. Peer-reviewed.
- Ganian, R., Gründel, M. (2026). Bilateral Treewidth for QBF: Where Strategies and Resolution Meet. In A. Ignatiev S. Szeider (Eds.), 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Schloss Dagstuhl.
Recent Presentations
- Bankosegger, R., Eiter, T., Oetsch, J. (2026, November 24). Answer-Set-Programming-based Abstractions for Reinforcement Learning [Conference Presentation]. 8th Workshop on Trends and Applications of Answer Set Programming (TAASP 2025), Wien, Austria.HDL: 20.500.12708/230865
- Eiter, T., Nießen, T., Soldà, D. (2026, September 8). SAT Modulo Well-Founded Semantics: Extended Abstract [Conference Presentation]. 18th International Conference on Logic Programming and Non-monotonic Reasoning (LPNMR 2026), Austria.
- Kletzander, L. (2026, August 27). Multi-Contract Integrated Shift Design and Rostering [Conference Presentation]. The 15th Conference on the Practice and Theory of Automated Timetabling (PATAT 2026), Nottingham, United Kingdom of Great Britain and Northern Ireland (the).HDL: 20.500.12708/230853
- Leitsch, A., Lolic, A., Mahler, S. (2026, July 25). Schemata, Cyclic Proofs and Herbrand Systems [Conference Presentation]. Women in Logic 2026, Lisbon, Portugal.HDL: 20.500.12708/230611
- Baaz, M., Gamsakhurdia, M., Lolić, A., Mahler, S. (2026, July 24). How to deal with Henkin Quantifiers in First-Order Logic [Conference Presentation]. Sixth International Workshop on Structures and Deduction 2026 at FLoC 2026, Lisbon, Portugal.HDL: 20.500.12708/230904
- Varga, J., Raidl, G., Rodemann, T. (2026, July 16). Timing of Queries in Interactive Job Scheduling [Conference Presentation]. The 24th Conference of the International Federation of Operational Research Societies (IFORS 2026), Wien, Austria. Invited.HDL: 20.500.12708/230630
- Iurlano, E., Raidl, G., Weissenfels, A. (2026, July 16). A Beam Search for Linearly Covering all Subsets of a Finite Set [Conference Presentation]. The 24th Conference of the International Federation of Operational Research Societies (IFORS2026), Wien, Austria. Invited.HDL: 20.500.12708/230621
- Gjergji, I., Kletzander, L., Musliu, N. (2026, July 16). Hyper-heuristics for the capacitated p-median problem [Conference Presentation]. The 24th Conference of the International Federation of Operational Research Societies (IFORS 2026), Vienna, Austria.HDL: 20.500.12708/231635 / Project: BioLog
- Kletzander, L., Foschini, M., Guns, T. (2026, July 15). Automated Weight Setting for Interactive Exploration in Multi-objective Combinatorial Optimization [Conference Presentation]. The 24th Conference of the International Federation of Operational Research Societies (IFORS 2026), Vienna, Austria.HDL: 20.500.12708/230848
- van Berkel, K., Dik, J. F. (2026, June 10). Reasoning with Values in Norm-based Argumentation [Conference Presentation]. 21st International Conference on Artificial Intelligence and Law (ICAIL 2026), Singapur, Singapore.
- Mulhern, J. H., Zhao, B., Shibayama, T., Raidl, G. R. (2026, May 7). Public Transit Optimization via a Novel Connectivity Parameter [Poster Presentation]. ÖVG 100th Anniversary Conference 24th European Transport Congress, Austria.HDL: 20.500.12708/228050
- Sextl, F. (2026, April 13). Brushing off the Rust: Towards Compositional Memory Safety Verification for unsafe Rust [Presentation]. Sixth Rust Verification Workshop (RW2026), Turin, Italy.DOI: 10.34726/12079 / Download: PDF
- Fermüller, C. G. (2026, April 4). Towards a Logical Framework for Graded Deontic Reasoning [Poster Presentation]. The 5th Tsinghua Interdisciplinary Workshop on Logic, Language and Meaning : Modality in Logic and Language (TLLM 2026), Beijing, China.
- Raidl, G. (2025, December 2). Learning to Guide Search in Combinatorial Optimization [Presentation]. AI Festival: Industry Meets University, Wien, Austria.HDL: 20.500.12708/225853
- Cabalar, P., Eiter, T., Pearce, D., Soldà, D. (2025, November 25). Brief Temporal Equilibrium Logic [Conference Presentation]. 8th Workshop on Trends and Applications of Answer Set Programming (TAASP 2025), Wien, Austria.HDL: 20.500.12708/230927 / Project: TAIGER
- Beiser, A., Hecher, M., Woltran, S. (2025, November 24). Automated Hybrid Grounding Using Structural and Data-Driven Heuristics [Conference Presentation]. TAASP 2025 : Workshop on Trends and Applications of Answer Set Programming, Wien, Austria.HDL: 20.500.12708/222847
- Gjergji, I., Kletzander, L., Bierlee, H., Musliu, N., Stuckey, P. J. (2025, November 10). A Consecutive Flight Leg Model for the Aircraft Maintenance Routing Problem [Conference Presentation]. Knowledge Engineering for Planning and Scheduling (KEPS 2025), Melbourne, Australia.HDL: 20.500.12708/225746
- Tomandl, L. (2025, November 6). A Reinforcement Learning Guided Large Neighborhood Search for the Dynamic Electric Autonomous Dial-a-Ride Problem [Presentation]. Austrian Workshop on Metaheuristics and Machine Learning 2025 (AWMHML 2025), Wien, Austria.HDL: 20.500.12708/225750
- Bresich, M. (2025, November 6). Search Space Reduction Through Machine Learning for the Electric Autonomous Dial-A-Ride Problem [Presentation]. Austrian Workshop on Metaheuristics and Machine Learning 2025 (AWMHML 2025), Wien, Austria.
- Gjergji, I., Kletzander, L., Musliu, N., Schaerf, A., Smith-Miles, K. (2025, October 1). Investigating the Capacitated Facility Location Problem with Customer Incompatibilities Using Instance Space Analysis [Presentation]. Middle-European Conference on Applied Theoretical Computer Science, Slovenia.HDL: 20.500.12708/225683
Recent Theses
- Simola, S. H. E. (2026). Algorithmic Complexity of Matching and Games [Dissertation, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2026.138201 / Download: PDF
- Selzer, A. (2026). A Structural Approach to Query Optimisation for Efficient Join and Aggregate Processing [Dissertation, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2026.138101 / Download: PDF
- Dobler, A. (2026). Algorithmic Aspects of Ordering Problems in Information Visualization [Dissertation, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2026.139471 / Download: PDF
- Pleßberger, S. (2026). Semantic verification of ethereum smart contracts using KEVM [Diploma Thesis, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2026.128561 / Download: PDF
- Merkl, T. (2026). On the Diversity and Space-Time Complexity of Query Answering: Algorithms and Structural Foundations [Dissertation, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2026.140927 / Download: PDF
- Di Stefano, F. (2026). Non-monotonic Description Logics Based on Predicate Minimization [Dissertation, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2026.140693 / Download: PDF
- Mohr, R. (2026). Semantic properties in ethereum bytecode using static analysis [Diploma Thesis, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2026.135664 / Download: PDF
- Böhm, J. (2026). Message passing on the edge : going beyond triangles [Diploma Thesis, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2026.137416 / Download: PDF
- Tulcan, R. F. (2026). Built to behave : constraining reinforcement learning agents with restraining bolts [Diploma Thesis, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2026.130021 / Download: PDF
- Seka, D. (2026). Enumerating graphs with respect to their choosability [Diploma Thesis, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2026.142822 / Download: PDF
- Miarasadollahnejad, A. H. (2026). Using graph neural networks to capture SHACL constraints in graph data [Diploma Thesis, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2026.131965 / Download: PDF
- Forster, S. (2026). Thiele methods for comment selection under trichotomous preferences [Diploma Thesis, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2026.142862 / Download: PDF
- Luxbacher, B. (2026). An implementation of Shor’s algorithm for elliptic curve cryptography [Diploma Thesis, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2026.132746 / Download: PDF
- Bodingbauer, J. (2026). Vampires can lean into trust : checking proofs for soundness [Diploma Thesis, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2026.139594 / Download: PDF
- Hamm, S. (2026). Explainable RL agents for conflict resolution in air traffic control [Diploma Thesis, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2026.137226 / Download: PDF
- Funder, F. (2026). An UPgrade for HCP : solving the Hamiltonian cycle problem via user propagators [Diploma Thesis, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2026.139586 / Download: PDF
- Eyjólfsson, L. (2026). Reconfiguration of resource allocation [Diploma Thesis, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2026.129205 / Download: PDF
- Varonka, A. (2026). Algebraic Analysis of Loop Programs [Dissertation, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2026.145064 / Download: PDF
- Sallinger, S. S. (2026). Rigorous Debugging Techniques for Software Systems [Dissertation, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2026.145003 / Download: PDF
- Polaczek, A. (2026). Thousands of Problems to Lean [Diploma Thesis, Technische Universität Wien]. reposiTUm.DOI: 10.34726/hss.2026.143161 / Download: PDF
We shape the future.
Vienna has a long tradition in logic. In the 1920s, the Vienna Circle gathered the brightest minds in science for developing a modern worldview, with logic as a core element. A century later, logic and computation at TU Wien Informatics continuously revives this notable past, bridging foundational logic and modern computing. We commit to advancing science and provide trustworthy technologies sealed via logical arguments. We envision the analysis and verification of reliable systems, certify user-driven system guarantees by efficient computation, and improve decision accuracy in intelligent systems with neurosymbolic AI methods.
Want more? We have more. Head over to our Newsroom!