Alastair F. Donaldson
Paper at ASE (August 2011) For a while I've been working with Matko Botincan and Mike Dodds at the Cambridge Computer Laboratory, and Matthew Parkinson at Microsoft Research Cambridge, on using separation logic-based techniques to prove safety of multicore programs which use asynchronous memory operations. A full paper on this work has just been accepted to the 26th IEEE/ACM International Conference On Automated Software Engineering (ASE 2011). Check it out here.
Paper at SAS (May 2011) Philipp Ruemmer, Leopold Haller, Daniel Kroening and I have had a paper accepted to the 18th International Static Analysis Symposium. The paper is on the use of k-induction for verification of imperative software. Among other things, we implemented k-induction in the Boogie verifier, and found it enabled us to verify programs with weaker invariants than standard Boogie requires. Check it out!
Paper at CAV (March 2011) Thomas Wahl, Alexander Kaiser, Daniel Kroening and I have had a paper accepted to the 23rd International Conference on Computer Aided Verification, on Symmetry-Aware Predicate Abstraction for Shared Variable Concurrent Programs. Check it out here.
Royal Society International Travel Grant funded (January 2011) The Royal Society will provide funding for Dragan Bosnacki of Eindhoven University of Technology to visit me at Oxford this summer, to work on the acceleration of formal verification algorithms using multicore systems. This is through the Society's International Travel Grants scheme.
Short papers accepted at PPoPP (October 2010) I have had two short papers accepted to the 2011 ACM SIGPLAN Conference on Principles and Practice of Parallel Programming. They are both on analysing multicore programs that use asynchronous memory operations. One gives preliminary details on an approach using separation logic, and is with Matko Botincan and Mike Dodds at the Cambridge Computer Laboratory, and Matthew Parkinson at Microsoft Research Cambridge. The other is a tool demonstration paper on SCRATCH, the DMA race analysis tool I have designed in collaboration with Daniel Kroening and Philipp Ruemmer at Oxford.
VMCAI paper on k-induction with static analysis (October 2010) Leopold Haller, Daniel Kroening and I have had a paper accepted at the 2011 conference on Verification, Model Checking and Abstract Interpretation. The paper explores the use of static analysis to aid k-induction as a technique for analysing races in multicore programs that use DMA. Check it out.
Offloading Threading Building Blocks (August 2010) George Russell from Codeplay just presented joint work with me, others at Codeplay, and Paul Keir at Glasgow, at the HPPC 2010 workshop, on using the Offload C++ system to get a subset of Intel's TBB running across the SPE cores of the Cell processor. Check it out.
Intel SCC Research Project (June 2010) Intel have accepted a proposal on Programming Tools for the Intel Single-chip Cloud Computer, which I put together with Paul Kelly at Imperial College London, and colleagues at Codeplay Software Ltd. The result is that Intel will grant us access to their 48-core research platform, to investigate formal verification and performance optimization techniques.
Symmetry Survey (April 2010) Thomas Wahl and I have published an up-to-date survey of symmetry reduction techniques for model checking. Check it out here. This survey complements and extends a previous ACM Computing Surveys article on the topic, which I published with Alice Miller and Muffy Calder.