[TYPES/announce] Postdoc position at Imperial on Automated Reasoning for Approximate Real Number Computation

[Alastair Donaldson]

Dear all

I'd be grateful if you could forward this job advert on to anyone you 
think might be interested.

For full details about the post, please see:

http://www.jobs.ac.uk/job/AII323/research-associate-or-research-assistant-automated-reasoning-for-approximate-real-number-computation/

Cheers

Ally Donaldson


  Research Associate or Research Assistant: Automated Reasoning for
  Approximate Real Number Computation


      *Imperial College London* -Department of Computing and Department
      of Electrical and Electronic Engineering

*Salary range: £32,750 -- £41,540per annum (Research Associate)*

*Salary range: £28,770 to £31,880 per annum (Research Assistant)*

*Fixed term appointment for 12 months in the first instance

***

Dr Alastair Donaldson and Professor George Constantinides are seeking 
talented Researchers for an exciting project running between the 
Departments of Computing and Electronic Engineering.

Many software applications conceptually involve computation with real 
numbers, which is in practice realised through real approximations, such 
as fixed-point and floating representations. These approximations 
involve associated calculation error.  While in some domains, e.g. video 
games, a relatively high degree of error may be acceptable, in others, 
e.g. scientific computing or computational geometry, the correctness of 
algorithms may depend critically on errors remaining within some 
range. This motivates techniques for verifying numerical accuracy of 
algorithms that use real number approximations.  Another motivation is 
the desire to implement algorithms in hardware, optimising for energy 
and area. Minimising the precision of components that approximate real 
number calculations can lead to energy and area gains, as long as 
precision remains adequate for correctness. This leads to a large 
potential optimisation space, and verification methods for assessing the 
adequacy of precision bounds provide a means for navigating this space.

This project will investigate the verification of correctness 
specifications for programs that manipulate real number approximations, 
through compilation from source code (e.g. OpenCL) into an intermediate 
format (e.g. Microsoft's Boogie language) where approximate calculations 
are transformed into (non-approximate) real number computation, with the 
introduction of real-valued error functions to model loss of 
precision. From this intermediate format, verification will involve 
discharging verification conditions to a satisfiability modulo theories 
(SMT) solver equipped with methods for reasoning about real 
arithmetic. For example, the Z3 SMT solver employs cylindrical algebraic 
decomposition (CAD), a semi-algebraic method, for this purpose. This 
will open the door for two avenues for further investigation: firstly, 
the (manual or automatic) synthesis of loop invariants to allow 
reasoning about these sorts of programs; secondly, the possibility of 
domain-specific methods for reasoning in real arithmetic, taking 
advantage of problem structure to overcome the scalability limitations 
arising from the worst case complexity of general semi-algebraic methods.

The position will be based at the South Kensington campus of Imperial 
College and could begin as soon as possible, although candidates who 
require some delay could be equally accommodated.

Strong applicants will have a background in formal verification or 
computer arithmetic and strong programming skills.  Candidates should 
have a PhD (or equivalent) in Computer Science, Electronic Engineering 
or a closely related subject.  Suitable applicants nearing completion of 
a PhD will be considered for initial appointment at Research Assistant 
level.

Our preferred method of application is online via our website at the 
following link: http://www3.imperial.ac.uk/employment (select "Job 
Search" and enter the job reference no *EN20140069AS*). Please complete 
and upload an application form as directed and submit any other relevant 
supporting documents such as your full CV.

If you are unable to apply online, please contact Mrs Wiesia Hsissen at 
email address: w.hsissen at imperial.ac.uk 
<mailto:w.hsissen at imperial.ac.uk> to request an application form, 
quoting reference number EN20140069AS in the request.

*Closing date: * 9 April 2014

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20140314/69fb50e2/attachment-0001.html>