[TYPES/announce] Postdoctoral Position in Munich on Type-based Enforcement of Programming Guidelines

[Ulrich Schöpp]

The following job offer might be interesting for those who would like to get more in touch with problems coming from the industry but without leaving academia completely. The work will be carried out at fortiss, a research institute in Munich with close connections both to the Munich universities TUM and LMU and to industry.

We invite applications for a two-year postdoctoral position in the DFG-funded project "GuideForce: Type-based Enforcement of Secure Programming Guidelines". The GuideForce project develops a lightweight static analysis method for verifying that Java programs adhere to programming guidelines. A first use-case are guidelines for secure programming, but other applications are of interest too. The project combines ideas from type systems and abstract interpretation to develop a scalable, type-based analysis method for Java.

The core of the project is a region-based type system that can capture interesting properties of program traces. Using this type system as a basis, the project investigates a number of directions.
- Improving the expressiveness of the type system: In addition to fairness-properties (nothing bad happens during execution), we extend the type system to be able to express liveness-properties (something good will eventually happen). The work in this direction is based on the Büchi-types approach of [1].
- Extending the method to handle more features of the Java programming language, such as reflection, concurrency, generic types and higher-order features.
- Develop practical applications of the method.

We are looking for a postdoctoral researcher with a background in programming languages and with experience in one of the following areas: type systems and logic, static program analysis, abstract interpretation, implementation of programming languages.

The successful candidate will be working in the Safety and Security group at fortiss in Munich. fortiss is the research institute of the Free State of Bavaria for software-intensive systems and services. Our scientists collaborate on research, development and transfer projects with universities and technology companies in Bavaria, Germany and Europe. Research is focused on state of the art methods, techniques and tools of software development, systems & service engineering and their application to reliable, secure cyber-physical systems. We have close connections to both TUM and LMU Munich. fortiss has the legal structure of a non-profit limited liability company (GmbH). Its shareholders are the Free State of Bavaria (as majority shareholder) and the Fraunhofer Society for the Promotion of Applied Research.

The position is available for two years, starting as soon as possible. The salary will be set at level TV-L 13 of the German public salary scale.

For any questions about the project or the position, please do not hesitate to contact Ulrich Schöpp <schoepp at fortiss.org>.

Please submit your application before the end of the year via the following link:
https://recruitment.fortiss.org/POSTDOCTORAL-RESEARCHER-TYPE-BASED-ENFORCEMENT-OF-SECURE-P-eng-j74.html

The project builds on the following publications.
[1] Chen, Hofmann. Büchi Types for Infinite Traces and Liveness. CoRR abs/1401.5107 (2014)
[2] Serdar Erbatur, Martin Hofmann, Eugen Zalinescu. Enforcing Programming Guidelines with Region Types and Effects. APLAS 2017
[3] Hofmann, Ledent. A cartesian-closed category for higher-order model checking. LICS 2017

Best regards,
Ulrich Schöpp


-- 
fortiss · Landesforschungsinstitut des Freistaats Bayern
An-Institut Technische Universität München
Guerickestraße 25
80805 München
Germany
Tel.: +49 (89) 3603522 166
Fax: +49 (89) 3603522 50
E-Mail: schoepp at fortiss.org
http://www.fortiss.org

Amtsgericht München: HRB: 176633
USt-IdNr.: DE263907002, Steuer-Nr.: 143/237/25900
Rechtsform: gemeinnützige GmbH
Sitz der Gesellschaft: München
Geschäftsführer: Dr. Harald Rueß, Thomas Vallon
Vorsitzender des Aufsichtsrats: Dr. Manfred Wolter