DTC CS 21 - Extracting advanced SMT solvers from proofs
In U. Berger, A. Lawrence. F. Nordvall Forsberg, M. Seisenberger, Extracting Verified Decisions Procedures, LMCS, 2015, it was demonstrated how to extract a basic SAT solver from a proof. The objective of this PhD project is to lift this technique to the next level and extract SMT solvers, i.e. solvers that can deal with a much richer logical language, and therefore cover many more problems. In particular we have problems in mind arising from the industrial context (connection to Railway Verification), and conversely, on the theoretical side, also want to be able to deal with infinite clauses sets (connection to the Computing with Infinite Data (CID) project), and more advanced problems arising in Complexity theory.
Candidates must have a minimum of an upper second class honours degree or equivalent in a relevant subject, or an appropriate Master’s degree (with Merit). Informal enquiries are welcome by emailing the project supervisor.
For candidates whose first language is not English, we require IELTS 6.5 (with 6.0 in each component) or equivalent. Please visit our website for a list of acceptable English language tests. We prefer candidates to have already met the English Language requirements at the point of application, although this is not a requirement.
How to apply
Visit our webpage for details - http://www.swansea.ac.uk/science/research/dtc/biosciences-projects-2018-19/
Please include the project ID and title in your email subject header (eg. DTC CS xxxxxx)
Student Finance England have announced plans to offer student loans for PhD level courses from September 2018 for courses at any PhD awarding university (including Swansea University). Full details are still to be confirmed. Visit our website for updated information. – http://www.swansea.ac.uk/postgraduate/fees-and-funding/pg-loans/