I have worked on theoretical topics (e.g., on separation and bunched logics, on category-theoretic models...) and on automated tools for program verification and analysis (e.g., Smallfoot, Space Invader, Abductor). I like to think that fundamental theory, tool development and application can and even should play off one another via mutual feedback in computer science research, in a way reminiscent of the experimental method.
Our group at UCL is part of a community in the southeast of England (in London, Cambridge and Oxford) who are enthusiastically pursuing program logic and semantics, mechanized program verification and static program analysis; it is a great place for this sort of research at the moment. This effort is partly (though by no means wholly!) underpinned by an EPSRC Programme Grant, Resource Reasoning, split between UCL, Imperial and Oxford.
Research positions
in Program Analysis and Systems at UCL;
closing dates 27 May (2 postdocs) and 21 May (1 research engineer)
Postdoc position at UCL on Compositional
Binary Analysis; closing date 27 May
Some Research Links:
Resource Reasoning (current)
Separation Logic
Smallfoot
SpaceInvader
SpaceInvader
Other:
Attack of the 50 Foot Spatial Dudes
Proof of Cyclic List Reversal
Matthew Parkinson has won the
2013 Dahl-Nygaard Junior Prize
for his work on reasoning about OO programs. Congrats Matthew!
In other news, Dino Distefano presented the
Needham Award lecture on 29 Nov
, for his work on program analysis with separation logic.
Check out the
entertaining headline in the Italian press.