Chalmers University of Technology CSE Department is hiring: 3 PhD students and 1 Post-Doctoral researcher in formal methods and in language-based security.
Those I hire (1 PhD student and 1 Post-Doc) are encouraged to work with interactive theorem proving in higher-order logic using HOL4. Feel free to contact me with questions regarding these positions. * Application deadline: 10 April 2016. * Expected starting date: preferably around September 2016. For details, including employment conditions and how to apply, see: http://www.chalmers.se/en/about-chalmers/vacancies/?rmpage=job&rmjob=3853 http://www.chalmers.se/en/about-chalmers/vacancies/?rmpage=job&rmjob=3854 http://www.chalmers.se/en/about-chalmers/vacancies/?rmpage=job&rmjob=3855 2 PhD student and 1 Post-Doctoral researcher position in Formal Methods: ------------------------------------------------------------------------ The Formal Methods group of Chalmers is internationally recognised for its high-profile research track record and extensive network of collaborators. The group's research focus are the theoretical and practical aspects of rigorous software analysis and verification, including techniques such as automated reasoning, interactive theorem proving, runtime verification, automated test generation, and program synthesis. In collaboration with other researchers worldwide, Chalmers’ Formal Methods group developed and maintains verification tools such as the CakeML toolchain (https://cakeml.org/) and the HOL4 theorem proving system (http://hol-theorem-prover.org/), KeY (http://www.key-project.org), Vampire (http://vprover.org), ALIGATOR (http://mtc.epfl.ch/software-tools/Aligator), the Eiffel Verification Environment (http://se.inf.ethz.ch/research/eve/ and http://comcom.csail.mit.edu/autoproof/), and LARVA. We are looking for outstanding candidates with interest in pursuing research in one or more of the following areas: 1. Automated program repair 2. Functional-correctness verification of software 3. Combining heterogeneous verification techniques 4. Synthesis of programs and specifications 5. Compiler correctness (for e.g. just-in-time compilation) These positions will be supervised by Prof. Carlo A. Furia (1 PhD student, research areas 1-4, see http://bugcounting.net) and Prof. Magnus Myreen (1 PhD student and 1 Post-Doctoral researcher, research areas 2-5, see http://www.cse.chalmers.se/~myreen/). 1 PhD student position in language-based security ------------------------------------------------- The PhD students will join a high-profile group of researchers on software security with a rich network of collaborators and visibility across several research communities (security, programming languages, and systems research). In collaboration with top universitites, researchers at Chalmers have developed some of the state of the art tools for protecting users' private data in Haskell programs (e.g., LIO https://hackage.haskell.org/package/lio) as well as web browsers (COWL http://cowl.ws/). The position focuses on developing techniques to protect confidentiality and integrity of users' data when manipulated by untrusted code -- a pressing problem for the web as well as mobile platforms. It is expected that the work carried out by the applicant ranges from establishing new theoretical foundations to deploying prototypes in production systems. We are looking for outstanding candidates with background in either programming languages and/or systems research interest in pursuing one or more of the following topics: 1. Combining static and dynamic techniques to secure Haskell programs 2. Leveraging hardware-level security components (e.g, Intel SGX and ARM TrustZones) to provide security in depth, where private data can be protected from the application level down to the low-level physical layers. 3. Developing domain specific languages to express different kind of security policies This position will be supervised by Prof. Alejandro Russo (http://www.cse.chalmers.se/~russo/). ------------------------------------------------------------------------------ Transform Data into Opportunity. Accelerate data analysis in your applications with Intel Data Analytics Acceleration Library. Click to learn more. http://pubads.g.doubleclick.net/gampad/clk?id=278785231&iu=/4140 _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
