Open Positions

Funded PhD and PostDoc positions

The Formal Methods in Systems Engineering Group at Vienna University of Technology is looking for PhD students and PostDocs. We are looking for new colleagues in the areas of Formal Methods, Software Model Checking, Abstract Interpretation, Static Analysis, Automata Theory, …

If you are mathematically inclined and/or a versatile programmer willing to combine theory and practice, one of the following exciting research projects might offer the job of your dreams:

  • Doctoral Program “Logical Methods in Computer Science” (LogiCS)

Doctoral Program LogiCS

As part of the joint doctoral program LogiCS of TU Wien, TU Graz, and JKU Linz, we are seeking exceptionally talented and motivated students. The LogiCS doctoral college focuses on interdisciplinary research topics covering

(i) computational logic, and applications of logic to
(ii) databases and artificial intelligence as well as to
(iii) computer-aided verification.

For further details, consider the Call for Students and the LogiCS website.

Heisenbugs are software bugs that defy attempts to analyse their causes. The Heisenbugs project is concerned with the detection, reproduction, and explanation of intricate error scenarios in concurrent programs and embedded systems (such as smartphones). To tackle the problem, we will apply a wide spectrum of debugging techniques, program analyses, and automated reasoning.

The project offers ample research opportunities for talented students and postdocs, from system enthusiasts to logic buffs. We are looking for outstanding (prospective) researchers who are excited about at least one of the following areas:

  • Static analysis, model checking, and abstract interpretation. If it was always your dream to to keep that state space from exploding, this might be the right job for you.
  • Logic and automated decision procedures. You’re fascinated by unsatisfiable cores and don’t shy away from logical abduction? Austria is the right place for you.
  • Compilers, debuggers, and run-time monitoring. If you’re an abstract syntax tree hugger and don’t scare away from the nitty-gritty details of multi-core architectures or virtual machines, we want you for our team!
  • Automated Program Analysis for Bounds on Resource Consumption (Florian Zuleger)

Computer programs are consuming physical resources such as time, memory, power and bandwidth which are crucial for non-functional correctness. To guarantee efficiency, energy use, accuracy of bid placement by cloud providers etc. we need development tools that can predict the resource consumption of a program in the form of upper bounds.  In this project we will develop a quantitative modeling framework for bound analysis, and apply this framework as backbone for practical bound analysis tools.

The project offers intriguing research challenges ranging from practical to theoretical problems:

  • The design and analysis of appropriate abstractions for bound analysis using tools from logic, automata theory, formal methods, etc.
  • The developement and implementation of new static analyses for bound analysis problems using methods such as software model checking and abstract interpretation.
  • The extension and application of bound analyses to real-world problems such as finding perfomance bugs through static program analysis techniques.

Vienna: A thriving environment for working on Formal Methods

Vienna is home to a number of world-class researchers in the field of automated verification and logic. The city has evolved into a hub in a network of excellence on formal methods.

  • World-class Faculty in Formal Methods and Logic at TU Vienna:
    Radu Grosu, Laura Kovács, Ulrich Schmid, Uwe Egly, Thomas Eiter, Stefan Szeider, Reinhard Pichler, Alex Leitsch, Matthias Baaz, Agata Ciabattoni, and many more …
  • Network of Excellence on Formal Methods in Austria (RiSE)
    Many opportunities to collaborate with renowned scientists across Austria
  • The Vienna Center for Logic and Algorithms (VCLA) invites visiting researchers and hosts workshops and student schools such as the Winter School on Verification
  • We have a joint weekly seminar with IST Austria with many international guests
  • We organize a joint workshop with the PUMA graduate school at TU Munich once a year
  • We organise CAV 2013 in St. Petersburg!
  • We will host FLoC 2014 in Vienna!

Vienna: The best living standard in the world!

  • A beautiful city in the heart of Europe
  • Continually ranked no. 1 in the Mercer Quality of Living Survey
  • Enjoy the Viennese Coffee Houses listed as ‘Intangible Cultural Heritage’ by the UNESCO
  • Find out about the notorious “Wiener Schmäh” (Viennese charm)

How to apply

Please submit your application material via the web-page of our doctoral college. Please tell us why you think that you are a good match for the FORSYTE group and whether there is a specific project you would like to work on (if you haven’t made up your mind yet, you can leave the decision to our sorting hat ;-)).

Schikaneder – bar, cinema, club

View on the roof of the Stephan’s Cathedral and the city center

Roof of Stephan’s Cathedral and City Center (Photo by Miroslav Petrasko)

Coffee house "Caf&eqcute; Central"

Coffee house “Café Central”


Latest News

WWTF ICT project awarded to Igor Konnov

Igor Konnov (PI), together with Josef Widder (co-PI) and Helmut Veith (core team), are awarded an ICT research project APALACHE “Abstraction-based Parameterized TLA Checker” by the Vienna Science and Technology Fund WWTF.

Continue reading

Austrian Computer Science Day 2015

The Austrian Computer Science Day 2015, which takes place on October 15, features a range of talks by leading Austrian computer scientists, including topics such as computer games, augmented reality, aware systems, semantic web, business processes, and reliable systems. Register for free by October 7, 2015! This year’s speakers are: Alois Ferscha (JKU Linz) Tom […]

Continue reading

Helmut Veith receives CAV Award

The 2015 CAV Award is given to Edmund Clarke, Orna Grumberg, Ron Hardin, Zvi Harel, Somesh Jha, Robert Kurshan, Yuan Lu, and Helmut Veith for the development and implementation of the localization-reduction technique and the formulation of counterexample-guided abstraction refinement (CEGAR).

Continue reading


We had great talks at FRIDA’15 workshop in Grenoble. The slides of some of the talks are available online.

Continue reading

Full news archive