[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
+-----------------------------------------+ Ph.D position in Formal Methods available at the Dept. of Informatics, University of Oslo. on the topic +--------------------------------------+ Formal Analysis for Concurrent Programs +--------------------------------------+ Deadline: 08. 04. 2022 1. Position =========== The position will be part of the research group on formal methods at the Department of Informatics (IFI). The research group develops and applies techniques for formal modelling and analysis in a range of problem domains. As a research fellow in this research group, you will be working in a friendly, stimulating and international research environment with a number of PhD and postdoctoral fellows. 2. Qualification requirements, employment details & how to apply ================================================================ For detailed information about how to apply, formal application requirements and expectations, terms of employment and wage etc., see the web announcements: - https://urldefense.com/v3/__https://www.jobbnorge.no/en/available-jobs/job/222897/phd-research-fellow-in-formal-analysis-of-concurrent-systems__;!!IBzWLUs!FPggx67PTjENQl-UxY3_A1TpO3eJYtOvN9_w60oLr9JWoF1KI3vQ8V1a34G7jZ4BsBd96oLLA4c0Qg$ 3. Contacts: =========== - Martin Steffen (mstef...@ifi.uio.no) - Einar Broch Johnsen (ein...@ifi.uio.no) 4. More details on the intended area of research ================================================ The planned PhD research aims to develop formal semantic-based analysis methods for tackling modern concurrency abstraction and memory models for multi-threaded programming languages and systems. That also involves developing and using appropriate software analysis and synthesis tools to ensure synchronisation-related correctness properties, such as deadlock-freedom, sequential consistency, functional determinacy or absence of information leakage. The results from the theoretical investigations will be encapsulated in programming libraries and analysis algorithms that fit into the existing eco-systems of the chosen host languages. Methodologically, the research will target mainly light-weight verification methods, analysis methods and corresponding tools that work automatically, without interactive user intervention. In particular, type-based analyses and synthesis methods to check for resource-consumption, conformance with interface specification, race freedom, etc.