University of Oxford

Open Data about the University of Oxford

data.ox.ac.uk

beta

Research Associate on Counter Automata - Verification and Synthesis

Applications for this vacancy closed on 5 December 2016 at 12:00PM
We are looking for a Research Associate to work on the EPSRC-funded project
“Counter Automata: Verification and Synthesis”. The aim of this project is to
enhance the algorithmic toolkit for verification and synthesis, building on
connections between counter automata and extensions of Presburger arithmetic.



Presburger arithmetic is one of the most widely implemented and applied
theories in SMT solvers. In this project, we are concerned with an extension
of Presburger arithmetic with the binary divisibility predicate. One of the
main objectives is to characterise the complexity of deciding satisfiability
for quantifier-free sentences in this logic. More pragmatically we are also
interested in developing practical decision procedures for this problem. A
second objective of the project is to tackle verification and synthesis
problems for counter automata with input and parameters, including developing
connections with Presburger arithmetic with divisibility.



As a Research Associate on this project you will be expected to manage your
own research and administrative activities which will include small scale
project management, as well as collaborate in the preparation of research
papers for publication in conferences and journals. You may also be required
to assist in the supervision of post-graduate students working on related
projects.



You will have a PhD or be very close to completion, in a relevant area of
science (such as computer science or mathematics) together with a documented
track record of completing research projects in the area of algorithms, logic,
or verification, as witnessed by published peer-reviewed work. You will
possess excellent communication skills and be able to work both independently
and as part of a collaborative team.



This is a fixed-term post until 30 June 2017.



The closing date for applications is 12.00 noon on 5 December 2016. Interviews
are expected to be held in the week commencing 12 December 2016.

dc:spatial
Department of Computer Science, Wolfson Building, Parks Road, Oxford.
Subject
oo:contact
oo:formalOrganization
oo:organizationPart
vacancy:applicationClosingDate
2016-12-05 12:00:00+00:00
vacancy:applicationOpeningDate
2016-11-03 09:00:00+00:00
vacancy:furtherParticulars
vacancy:internalApplicationsOnly
False
vacancy:salary
type
comment

We are looking for a Research Associate to work on the EPSRC-funded project “Counter Automata: Verification and Synthesis”. The aim of this project is to enhance the algorithmic toolkit for verification and synthesis, building on connections between counter automata and extensions of Presburger arithmetic.


Presburger arithmetic is one of the most widely implemented and applied theories in SMT solvers. In this project, we are concerned with an extension of Presburger arithmetic with the binary divisibility predicate. One of the main objectives is to characterise the complexity of deciding satisfiability for quantifier-free sentences in this logic. More pragmatically we are also ...

We are looking for a Research Associate to work on the EPSRC-funded project
“Counter Automata: Verification and Synthesis”. The aim of this project is to
enhance the algorithmic toolkit for verification and synthesis, building on
connections between counter automata and extensions of Presburger arithmetic.



Presburger arithmetic is one of the most widely implemented and applied
theories in SMT solvers. In this project, we are concerned with an extension
of Presburger arithmetic with the binary divisibility predicate. One of the
main objectives is to characterise the complexity of deciding satisfiability
for quantifier-free sentences in this logic. More pragmatically we are also ...
label
Research Associate on Counter Automata - Verification and Synthesis
notation
126165
based near
page