We invite applications for: - *two* Research Fellow/Senior Research Fellow positions (Deadline: Janua= ry 5, 2020). Positions are 1 year in the first instance, with the possibili= ty of extension until December 2022. One position will be at University Col= lege London, and one at Royal Holloway University of London. - *one* PhD studentship at UCL. Successful applicants will be working on the EPSRC-funded "Verification of = Hardware Concurrency via Model Learning" (CLeVer) project. This is a joint research endeavour involving the Computer Science Departmen= ts of two UK's leading research-intensive universities -- University Colleg= e London and Royal Holloway University of London -- and ARM, world-leading = designer of multi-core chips. We are looking for candidates with experience in one or more of the followi= ng areas: model learning techniques, verification, concurrency, and formal = methods. Experience in tool implementation will also be valued. # HOW TO APPLY - Applications for *both* the (Senior) Research Fellow positions should be = made here before *January 5, 2020*: https://atsv7.wcn.co.uk/search_engine/jobs.cgi?owner=3D5041404&ownertype=3D= fair&jcode=3D1847641&vt_template=3D965&adminview=3D1 - Applications for the PhD position should be made here: https://www.ucl.ac.uk/prospective-students/graduate/apply Interested applicants are encouraged to contact Prof. Alexandra Silva (alex= andra.silva@ucl.ac.uk) and Dr. Matteo Sammartino (m.sammartino@ucl.ac.uk). # ABOUT THE PROJECT Digital devices increasingly rely on multi-threaded computation, with sophi= sticated concurrent behaviour becoming prevalent at any scale. As the complexity of these systems increases, there is a pressing need to a= utomate the assessment of their correctness, especially with respect to con= currency-related aspects. Formal verification provides highly effective techniques to assess the corr= ectness of systems. However, formal models are usually built by humans, and as such can be erro= r-prone and inaccurate.=20 This project aims to: - develop a verification framework that relies on learning techniques to au= tomatically build and verify models of concurrency, with a particular focus= on multi-core systems. - apply the framework to industrial verification tasks, in collaboration wi= th ARM. The project will provide opportunities for both theoretical and applied res= earch in several areas of Computer Science, including model learning techni= ques, verification, concurrency, and formal methods. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]