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

WAIT 2016 in Vienna

The third WAIT workshop on induction is held between 17-18 November at the TU Wien. Details are available on the workshop page.

Continue reading

Two papers at POPL’17

Two papers co-authored by researchers from our group have been accepted for POPL’17: “Coming to Terms with Quantified Reasoning” by Simon Robillard, Andrei Voronkov, and Laura Kovacs; and “A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms” by Igor Konnov, Marijana Lazic, Helmut Veith, and Josef Widder

Continue reading

Helmut Veith Stipend

Outstanding female students in the field of computer science who pursue (or plan to pursue) one of the master‘s programs in Computer Science at TU Wien taught in English are invited to apply for the Helmut Veith Stipend

Continue reading

LogicLounge in memoriam Helmut Veith

Will robots take away your job? In memory of Helmut Veith, this year’s Conference on Computer Aided Verification (CAV), which takes place in Toronto, will feature a LogicLounge on the effect of automation and artificial intelligence on our jobs.

Continue reading

Questions answered by Leslie Lamport

Leslie Lamport is going to answer questions about a Mathematical View of Computer Systems in Informatikhörsaal on Tuesday at 6pm. Check the announcement at the VCLA website and do not forget to watch the lecture beforehand.

Continue reading

Full news archive