Hello everyone, We are seeking two outstanding postdocs (one theoretical, one more practical) with strong interests in the formal specification and verification of concurrent and distributed systems to join the Program Specification and Verification Group, led by Professor Philippa Gardner, at Imperial College London.
Two three-year positions will be funded as part of "REMS: Rigorous Engineering of Mainstream Systems", a 6-year EPSRC-funded programme grant for £5.6 million between Cambridge, Edinburgh and Imperial, which finishes in 2019. It is not easy to reason about concurrent programs. At Imperial, we have considerable expertise in specifying concurrent libraries and verifying concurrent programs. In particular, our recent work has focussed on the extension of concurrent separation logic to handle abstraction, abstract atomicity, fault-tolerance and progress. We have applied this reasoning to, for example, concurrent indexes (B-trees and java.util.concurrent skip lists), graph algorithms, the POSIX file system and an ARIES database recovery algorithm. Our immediate research goals are: to continue to provide logics for reasoning about concurrent programs; to develop automated tools based on our logics; to test the reasoning on key applications such as databases, file systems and data centres; and to extend the reasoning to distributed systems. Please take a look at our Concurrency web page (http://psvg.doc.ic.ac.uk/research/concurrency.html) for more details and do not hesitate to contact Philippa at [email protected] if you are interested in one of these postdoc positions. Best wishes, Petar Maksimovic Petar Maksimovic, Ph.D. Research Fellow Department of Computing Imperial College London South Kensington Campus London SW7 2AZ Email: [email protected] ---- [[ Petri Nets World: ]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ: ]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies: ]] [[ [email protected] ]]
