[Hol-info] 10 PhD and PostDoc positions in Formal Verification

[Georg W. <hi...@fo...>]

10 PhD AND POST-DOC POSITIONS IN FORMAL METHODS

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
(hi...@fo...), 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
hi...@fo.... 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)