NEWS: Since October 2010, I have moved to MPI-SWS.
Please visit my new home page.
I used to be a research associate at the University of Cambridge Computer
Laboratory, where I did my undergraduate and postgraduate studies. Previously,
I was a postdoc researcher at Microsoft
Research Cambridge.
My research interests are: program analysis/verification, programming
languages, program logics and concurrency.
Program logics
I have (co)developed the following program logics:
- RGSep, a combination rely/guarantee and separation logic; and
- Deny-Guarantee, another combination of RG and SL allowing
dynamically splitting of interference.
Software
I have written the following software tools:
- SmallfootRG: a verification tool that proves
safety properties of concurrent programs.
[More information...]
- Cave: a verification tool that proves linearizability of concurrent programs.
(Please contact me for more information.)
Recent publications
| CAV 2010 |
Automatically proving linearizability.
|
| ECOOP 2010 |
Concurrent abstract predicates.
(with Dinsdale-Young, Dodds, Gardner, Parkinson)
|
| VMCAI 2010 |
RGSep action inference.
|
| POPL 2010 |
Structuring the verification of heap-manipulating programs.
(with Nanevski, Berdine)
|
| APLAS 2009 |
Bi-abductive resource invariant synthesis.
(with Calcagno, Distefano)
|
| FMCAD 2009 |
Finding heap-bounds for hardware synthesis.
(with Cook, Gupta, Magill, Rybalchenko, Simsa, Singh)
|
| ESOP 2009 |
Deny-guarantee reasoning.
(with Dodds, Feng, Parkinson)
|
| POPL 2009 |
Proving that nonblocking algorithms don't block.
(with Gotsman, Cook, Parkinson)
|
| VMCAI 2009 |
Shape-value abstraction for verifying linearizability.
|
| SAS 2007 |
Modular safety checking for fine-grained concurrency.
(with Calcagno, Parkinson)
|
| CONCUR 2007 |
A marriage of rely/guarantee and separation logic.
(with Parkinson)
|
[All publications...]
PhD dissertation
Contact Details
| Email: |
Viktor dot Vafeiadis at cl.cam.ac.uk |