The Formal Methods in Systems Engineering Group at Vienna University of Technology offers 10 PhD/PostDoc positions. 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:

Proof Seeding for Software Verification (PROSEED)
Rigorous Systems Engineering (RiSE)  (Helmut Veith)

The PROSEED research project proposes an innovative approach to verification which is based on the insight that program texts are carrying important information which is directed at the human readers of the program. We will utilize this human engineering information in a logically sound framework for computer-aided verification. RiSE investigates techniques beyond classical model checking and a-posteriori verification. We are trying to answer the following questions:

• How can we exploit informal information in program source code for model checking?
• How can we model check distributed algorithms?
• How can we test concurrent software?
• How many processes/threads suffice to find an error?
• How can we combine abstraction and bit-precision?
• How can we build networks with guaranteed properties?
• How can we combine testing and model checking?

Heisenbugs: From Detection to Explanation (Georg Weissenbacher)

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 Suvey
• 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

We would be happy to receive an email with your resume at ta.etysrofnull@bnessiew. 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

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

Coffee house “Café Central”