The Formal Methods in Systems Engineering Group at Vienna University of Technology offers 10 
funded PhD/PostDoc positions in three exciting research projects addressing the reliability and 
correctness of software. The topics range from model checking, abstract interpretation, static 
analysis and automata theory to testing and runtime verification, offering ample research 
opportunities for talented scientists, from system enthusiasts to the more theoretically minded. 
You can find more details below or on our website http://www.forsyte.at/hiring. Please do not 
hestitate to contact us (hiring@forsyte.at), if you have further questions.

REQUIREMENTS

We are looking for highly motivated students and scientists who are willing to make outstanding 
contributions in the field of formal methods and want to work in a team of world-class researchers.
Applicants are expected to hold a master's degree (for PhD positions) or a doctorate (for PostDoc 
positions) in computer science, electrical engineering, or a related discipline, and have excellent
communication skills in spoken and written English.

VIENNA - A great place to work on Formal Methods

Vienna has recently evolved into a major hub for formal methods. The city is home to a number of 
renowned and highly visible researchers in the field of automated verification and logic. Vienna, 
the capital of Austria, is a beautiful city in the heart of Europe, and consistently ranked no. 1 
in the 'Quality of Living' study by Mercer.

HOW TO APPLY

We would be happy to receive an email with your resume at hiring@forsyte.at. 
Please tell us why you think that you are a good match for our group and whether there is a 
specific project you would like to work on.


=============================================================
Proof Seeding for Software Verification (PROSEED)
Rigorous Systems Engineering (RiSE)
(principal investigator: 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
(principal investigator: 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
(principal investigator: 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
- The Network of Excellence on Formal Methods in Austria (RiSE) provides 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
- No. 1 in 'Quality of Living' ranking by Mercer (since 2009)
- Enjoy the Viennese Coffee Houses listed as 'Intangible Cultural Heritage' by 
the UNESCO
- Find out about the notorious 'Wiener Schmaeh' (Viennese charm)