Email Gateway (Aug 22 2022 at 09:52): Email Gateway (Aug 22 2022 at 09:52):From: Gudmund Grov <gudmundgrov@gmail.com>
Post-doc position in Tactics for Program Verifiers
The Research Associate will work on the EPSRC project "DTacs - Program
Verifier Tactics : Reducing the Development Time for Program Verifiers
with Re-usable Verification Strategies". This project addresses a
new method for proof automation for the Dafny program verifier by
developing support for user-provided and re-usable proof patterns. The
end goal is to liberate users from low-level and repetitive search
tasks by replacing these with higher-level underlying patterns that
can be reused for similar tasks; increasing automation and reducing
development time and cost.
The work is inspired by proof tactics used to encode reasoning
patterns for interactive theorem provers. The novelty of the `Dafny
tactics' we seek to develop is that proof patterns will be encoded as
special Dafny methods within the program text, making them accessible
to a wider group of users. We are therefore seeking a candidate with
expertise in tactic languages (for interactive theorem provers) and/or
expertise with program verifiers. The successful candidate will work
closely with the investigator in developing the concept of Dafny
tactics, and will therefore be integral in shaping this new and
exciting research area. Project collaborators include Microsoft
Research (Redmond, USA) and NUI Maynooth (Ireland), and the successful
candidate will have the opportunity to make research visits to these
sites. The work will involve analysis of existing Dafny case studies,
as well as developing new examples from scratch. It is therefore
desirable to have experience with formal development of software. A
key outcome of the project will be a prototype implementation of Dafny
tactics. Good programming skills are therefore essential, and
familiarity with C# and Visual Studio are desirable. The successful
candidate should also be able to communicate effectively with people
from other disciplines, and will be expected to:
The post is available for twelve months. Candidates should have, or be
near to completing, a PhD in formal methods or automated reasoning, or
a similar area. Experience with formal verification is essential, and
experience with program verification, in particular Dafny, and
interactive theorem proving and collaborative research is also
desirable. Candidates should have good programming and software
development skills, be comfortable working to tight deadlines, working
with other people, and be able to communicate complex ideas
effectively in person and in writing.
Informal enquiries should be made to Gudmund Grov:
G.Grov@hw.ac.uk
Details about how to apply can be found at:
http://www.hw.ac.uk/about/careers/job-opportunities/research-associate-in-tactics-for-program.htm
Closing date: 25 May.
Last updated: Apr 20 2024 at 01:05 UTC