Etudes Non Stop Study Non Stop
Related Articles
For more information please see Admission.
The LogiCS doctoral program is a PhD degree program funded by the Austrian Science Fund (FWF) and run jointly by the three Austrian universities; the TU Wien (Vienna University of Technology), Graz University of Technology and Johannes Kepler University Linz. This program is aimed at highly motivated students who want to work in the field of Logical Methods in Computer Science.
Why study Logical Methods in Computer Science?
LogiCS offers an international program characterized by the unique combination of disciplines where logical methods decisively impact practical computer science.
While many of the basic questions in computer science are now well understood, its role in science, technology, and everyday results in ever new challenges and big open research questions that require computers to perform non-trivial reasoning tasks.
Logic plays a key role in this evolving phase of computer science, similar to the role of calculus in the development of physics and engineering,
Logic is a powerful reasoning tool. Originally invented as an aid for sound argumentation, it reached maturity in the form of mathematical logic and analytic philosophy in the early 20th century, with significant contributions from Vienna.
We continue this tradition, using logic as a tool that enables computer programs to reason about the world. These reasoning tasks allow a natural classification into two broad areas: we can use logic to reason about the outside world, as well as to reason about computer programs themselves. This is reflected in our three core areas of research:
- In Databases and Artificial Intelligence, we use logic to model, store, analyze and predict information about the outside world including the Internet, different kinds of data sources, big data, and domain specific knowledge sources.
- In Verification, we use logic is used to model and analyze the behavior of computer programs, ensuring their correctness, from simple programs to complex software and hardware designs.
- The logical and algorithmic questions which underlie both application areas are studied in the area of Computational Logic.
We aim at developing new logical methods in these areas, and applying them to solving problems in emergent areas like Security and Privacy, Cyber-Physical Systems, and Distributed Systems.
You can read more about the areas that constitute the program here.
Why join the LogiCS program in Austria?
Vienna has a prominent history in mathematics, computer science, and logic research (Kurt Gödel, Vienna Circle, …). Additionally, it has repeatedly been ranked number 1 in the Mercer Quality of Living Survey.
The LogiCS faculty comprises 15 renowned researchers with strong records in research, teaching, and advising, complemented by 15 associated members who further strengthen the research and teaching activities of the college, as well as visiting professors and frequent guests.
The program is complemented by our faculty’s participation research initiatives such as the Austrian-wide National Research Network on Rigorous Systems Engineering (ARiSE) funded by the Austrian Science Fund, the Vienna Center for Logic and Algorithms (VCLA).
Which topics can I learn about in the LogiCS program?
The LogiCS program has three core areas. You will learn about all of them, and carry out research in specialized interdisciplinary topics within them:
- Computational Logic covers the theoretical and mathematical foundations, which are a prerequisite for logic to be the powerful tool that we deploy in application areas. Our focus here is proof theory (cut elimination, proof mining, Curry-Howard correspondence, interpolants), automated deduction (resolution, refutation, theorem proving), non-classical logics (substructural logics, multi-valued logics, juridical reasoning, deontic logics, modal and temporal logics), computational complexity (complexity analysis, parameterized complexity, decomposition methods) and constraint satisfaction (SAT, QSAT, CSP).
- Verification employs logic to model, analyze, and construct computer programs. This area is concerned with logical methods and automated tools for reasoning about the behavior and correctness of complex state-based systems, such as software and hardware designs as well as hybrid systems. It ranges from model checking, program analysis and abstraction to new interdisciplinary areas such as fault localization, program repair, program synthesis, and the analysis of biological systems.
- Databases and Artificial Intelligence uses logic to model, store, analyze and predict information about the outside world, for example, big data, the internet, and domain-specific knowledge sources. Here we study a large number of subjects, including query languages based on logical concepts (such as Datalog, variants of SQL, XML, and SPARQL), novel database-theoretical methods (like schema mappings, information extraction and integration, querying ontologies), logic programming, knowledge representation and reasoning (ontologies, answer-set programming, belief change, multi-context systems, inconsistency handling, argumentation, planning, preferential reasoning).
We are particularly focused on the design of logical methods in emergent application domains. In particular, you will have the opportunity of applying logic to solve challenging problems in the following areas:
- Security and Privacy: Security flaws and vulnerabilities affect virtually all IT infrastructures, and their devastating consequences touch each Internet user, as witnessed by recent high-profile vulnerabilities in TLS, mobile apps, Intel chips, or Ethereum contracts. Logic is a crucial tool to rigorously model the semantics of complex systems, which can be deterministic or probabilistic, and to specify the expected security properties (e.g., in terms of safety, liveness, or hyper-properties). Furthermore, it constitutes the foundation of formal security analysis (e.g., type systems and abstraction interpretation), monitoring (e.g., secure multiexecution), and synthesis techniques (e.g., secure compilation). The overarching goal of this research discipline is to develop formal methods that are capable to automatically verify security and privacy properties across all layers of modern IT infrastructures (e.g., mobile apps, browsers, cryptographic protocols, cloud services, and blockchain technologies) and to aid software developers in the design of provably secure and privacy-preserving systems.
- Cyber-Physical Systems: Cyber-physical systems are engineering, physical and biological systems whose operations are integrated, monitored, and/or controlled by a computational core. The behavior of CPS is a fully-integrated hybridisation of computational (logical) and physical action. The research related to this application domain includes formal analysis for hybrid-systems, symbolic and stochastic model checking, logic-based specification languages for spatio-temporal emergent behaviors, parameter synthesis, mining of requirements, adversarial attack of machine learning software components, runtime verification for safety and security properties, and synthesis of robust controllers.
- Distributed Systems: Distributed systems are omnipresent nowadays: besides traditional instances like server farms and local area networks, they constitute the backbone of various emerging domains, such as digital very-large scale integrated (VLSI) circuits, which can be seen as very large distributed systems implemented on a single piece of silicon, and the Internet-of-Things. Given that many of those applications are safety-critical, that hardware faults must be considered part of normal operation, and that severe resource and energy constraints are often inevitable, logic-based design and analysis methods are instrumental for establishing the vision of building systems that are correct by construction. Research in areas such as computer-aided verification, model-based design and, ultimately, synthesis for concurrent and distributed systems shall develop the scientific basis, the methods, and the tools that make this vision a reality.
