PhD position in Formal Verification of Concurrent Systems at Uppsala University, Sweden
----------------------------------------------------------------------- Multi-core processors are ubiquitous, but writing correct concurrent code is hard. Multi-threaded applications are prone to subtle bugs, such as deadlocks and race conditions. These bugs are notoriously difficult to find. Consequently, there is great interest in formal verification techniques for concurrent code. The objective of this project is to build a trustworthy framework that supports the interactive and semi-automated verification of programs that utilize low-level concurrency. The work will be carried out in the Modeling of Concurrent Computation research group (http://www.it.uu.se/research/group/mobility), which is part of the Uppsala Programming for Multicore Architectures Research Centre (http://www.it.uu.se/research/upmarc). Qualifications: The candidate should have a Master of Science in Computer Science, Computer Engineering or equivalent, ideally with a strong background in logic, formal semantics and concurrent/parallel programming. Experience with interactive theorem proving (e.g., Isabelle, Coq) is a plus. Please see the official announcement at http://www.uu.se/en/about-uu/join-us/jobs-detail-page/?positionId=46736 for further details. Applications close on December 14, 2014. ------------------------------------------------------------------------------ Download BIRT iHub F-Type - The Free Enterprise-Grade BIRT Server from Actuate! Instantly Supercharge Your Business Reports and Dashboards with Interactivity, Sharing, Native Excel Exports, App Integration & more Get technology previously reserved for billion-dollar corporations, FREE http://pubads.g.doubleclick.net/gampad/clk?id=157005751&iu=/4140/ostg.clktrk _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
