See also:
[By subject]
[DBLP]
[GoogleScholar]
### PhD dissertation

### Journal articles

### Conference papers (peer-reviewed)

### Position papers and technical reports

**Modular fine-grained concurrency verification.**

Viktor Vafeiadis.

University of Cambridge, July 2007.

Also published as technical report UCAM-CL-TR-726, University of Cambridge Computer Laboratory, July 2008.

[TR version]

**Geo-Replication: Fast If Possible, Consistent If Necessary.**

Valter Balegas, Cheng Li, Mahsa Najafzadeh, Daniel Porto, Allen Clement, SÃ©rgio Duarte, Carla Ferreira, Johannes Gehrke, João Leitão, Nuno M. Preguiça, Rodrigo Rodrigues, Marc Shapiro, Viktor Vafeiadis.

IEEE Data Engineering Bulletin 39(1): 81-92 (March 2016)

[@IEEE]**Mtac: A monad for typed tactic programming in Coq.**

Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis.

J. Functional Programming 25 (August 2015)

[Paper] [@CUP] [More...]**Aspect-oriented linearizability proofs.**

Soham Chakraborty, Thomas A. Henzinger, Ali Sezgin, Viktor Vafeiadis.

Logical Methods in Computer Science 11(1:20) (March 2015)

[@LMCS]**CompCertTSO: A verified compiler for relaxed-memory concurrency.**

Jaroslav Sevcik, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell.

J. ACM. 60(3):22 (June 2013)

[Paper] [@ACM] [More...]**Acute: High-level programming language design for distributed computation.**

Peter Sewell, James J. Leifer, Keith Wansbrough, Francesco Zappa Nardelli, Mair Allen-Williams, Pierre Habouzit, Viktor Vafeiadis.

J. Functional Programming 17(4-5): 547-612 (2007)

[Paper] [@CUP] [More...]

**Repairing sequential consistency in C/C++11.**

Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, Derek Dreyer.

In PLDI 2017. ACM (June 2017)

[Paper] [More...]**Tackling real-life relaxed concurrency with FSL++.**

Marko Doko, Viktor Vafeiadis.

In ESOP 2017 (April 2017)

[Paper] [More...]**Formalizing the concurrency semantics of an LLVM fragment**

Soham Chakraborty, Viktor Vafeiadis.

In CGO 2017. ACM (February 2017)

[Paper] [More...]-
**A promising semantics for relaxed-memory concurrency**

Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer.

In POPL 2017. ACM (January 2017)

[Paper] [@ACM] [More...] **Explaining relaxed memory models with program transformations.**

Ori Lahav, Viktor Vafeiadis.

In FM 2016 (November 2016)

[Paper] [@Springer] [More...]-
**Validating optimizations of concurrent C/C++ programs.**

Soham Chakraborty, Viktor Vafeiadis.

In CGO 2016. ACM (March 2016)

[Paper] [@ACM] [More...] **Reasoning about fences and relaxed atomics.**

Mengda He, Viktor Vafeiadis, Shengchao Qin, João F. Ferreira.

In PDP 2016 (February 2016)

[Paper] [@IEEE]-
**Taming release-acquire consistency.**

Ori Lahav, Nick Giannarakis, Viktor Vafeiadis.

In POPL 2016, pp. 649-662. ACM (January 2016)

[Paper] [@ACM] [More...] -
**Lightweight verification of separate compilation.**

Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis.

In POPL 2016, pp. 178-190. ACM (January 2016)

[Draft paper] [@ACM] [More...] **A program logic for C11 memory fences.**

Marko Doko, Viktor Vafeiadis.

In VMCAI 2016, LNCS vol. 9583, pp. 413-430 (January 2016)

[Paper] [@Springer] [More...]**Modular verification of concurrency-aware linearizability.**

Nir Hemed, Noam Rinetzky, Viktor Vafeiadis.

In DISC 2015, pp. 371-387 (October 2015)

[Paper] [@Springer]**Pilsner: A compositionally verified compiler for a higher-order imperative language.**

Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, Viktor Vafeiadis.

In ICFP 2015, pp. 166-178 (September 2015)

[Paper] [More...]**Rely/guarantee reasoning for asynchronous programs.**

Ivan Gavran, Filip Niksic, Aditya Kanade, Rupak Majumdar, Viktor Vafeiadis.

In CONCUR 2015, pp. 483-496 (September 2015)

[Paper] [@LIPIcs]**Asynchronous liquid separation types.**

Johannes Kloos, Rupak Majumdar, Viktor Vafeiadis.

In ECOOP 2015, pp. 396-420 (July 2015)

[Paper] [@LIPIcs] [More...]**Owicki-Gries reasoning for weak memory models.**

Ori Lahav, Viktor Vafeiadis.

In ICALP 2015, Track B, pp. 311-323. Springer (July 2015)

[Paper] [@Springer] [More...]**Verifying read-copy-update in a logic for weak memory.**

Joseph Tassarotti, Derek Dreyer, Viktor Vafeiadis.

In PLDI 2015, pp. 110-120, ACM (June 2015)

[Paper] [@ACM] [More...]-
**A formal C memory model supporting integer-pointer casts.**

Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, Viktor Vafeiadis.

In PLDI 2015, pp. 326-335. ACM (June 2015)

[Paper] [@ACM] [More...] -
**Common compiler optimisations are invalid in the C11 memory model and what we can do about it.**

Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, Francesco Zappa Nardelli.

In POPL 2015, pp. 209-220. ACM (January 2015)

[Paper] [@ACM] [More...] **Proving lock-freedom easily and automatically.**

Xiao Jia, Wei Li, Viktor Vafeiadis.

In CPP 2015, pp. 119-127. ACM (January 2015)

[Paper] [@ACM] [More...]-
**GPS: Navigating weak memory with ghosts, protocols, and separation.**

Aaron Turon, Viktor Vafeiadis, Derek Dreyer.

In OOPSLA 2014, pp. 691-707. ACM (October 2014)

[Paper] [@ACM] [More...] **Automating the choices of consistency levels in replicated systems.**

Cheng Li, João Leitão, Allen Clement, Nuno Preguiça, Rodrigo Rodrigues and Viktor Vafeiadis

In USENIX ATC 2014, pp. 281-292. USENIX (June 2014)

[Paper] [@USENIX]**Relaxed separation logic: A program logic for C11 concurrency.**

Viktor Vafeiadis, Chinmay Narayan.

In OOPSLA 2013, pp. 867-884. ACM (October 2013)

[Paper] [@ACM] [More...]**Mtac: A monad for typed tactic programming in Coq.**

Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis.

In ICFP 2013, pp. 87-100. ACM (September 2013)

[Paper] [@ACM] [Implementation (Mtac)]**Aspect-oriented linearizability proofs.**

Thomas A. Henzinger, Ali Sezgin, Viktor Vafeiadis.

In CONCUR 2013. LNCS, vol. 8052, pp. 242-256. Springer (August 2013)

[Paper] [@Springer]**Adjustable references.**

Viktor Vafeiadis.

In ITP 2013. LNCS, vol. 7998, pp. 328-337. Springer (July 2013)

[Paper] [@Springer] [More...]**A programming language approach to fault tolerance for fork-join parallelism.**

Mustafa Zengin, Viktor Vafeiadis.

In TASE 2013, pp. 105-112. IEEE (July 2013)

[Paper] [@IEEE] [More...]**The power of parameterization in coinductive proof.**

Chung-Kil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis.

In POPL 2013, pp. 193-206. ACM (January 2013)

[Paper] [@ACM] [Coq library (Paco)]**The marriage of bisimulations and Kripke logical relations.**

Chung-Kil Hur, Derek Dreyer, Georg Neis, Viktor Vafeiadis.

In POPL 2012, pp. 59-72. ACM (January 2012)

[Paper] [@ACM] [More...]**Verifying fence elimination optimisations.**

Viktor Vafeiadis, Francesco Zappa Nardelli.

In SAS 2011. LNCS, vol. 6887, pp. 146-162. Springer (September 2011)

[Paper] [@Springer] [More...]**Concurrent separation logic and operational semantics.**

Viktor Vafeiadis.

In MFPS 2011. ENTCS 276, pp. 335-351. Elsevier (September 2011)

[Paper] [@Elsevier] [More...]**Separation logic in the presence of garbage collection.**

Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis.

In LICS 2011, pp. 247-256. IEEE (June 2011)

[Paper] [@IEEE] [Technical appendix]**Relaxed-memory concurrency and verified compilation.**

Jaroslav Sevcik, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell.

In POPL 2011, pp. 43-54. ACM (January 2011)

[Paper] [@ACM] [More...]**Automatically proving linearizability.**

Viktor Vafeiadis.

In CAV 2010. LNCS, vol. 6174, pp. 450-464. Springer (July 2010)

[Paper] [@Springer] [Technical report] [Tool (Cave)]**Concurrent abstract predicates.**

Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew Parkinson, Viktor Vafeiadis.

In ECOOP 2010. LNCS, vol. 6183, pp. 504-528. Springer (June 2010)

[Paper] [@Springer] [Technical report]**RGSep action inference.**

Viktor Vafeiadis.

In VMCAI 2010. LNCS, vol. 5944, pp. 345-361. Springer (January 2010)

[Paper] [@Springer] [Tool (Cave)]**Structuring the verification of heap-manipulating programs.**

Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine.

In POPL 2010, pp. 261-273. ACM (January 2010)

[Paper] [@ACM] [Proof scripts]**Bi-abductive resource invariant synthesis.**

Cristiano Calcagno, Dino Distefano, Viktor Vafeiadis.

In APLAS 2009. LNCS, vol. 5904, pp. 259-274. Springer (December 2009)

[Paper] [@Springer]**Finding heap-bounds for hardware synthesis.**

Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko, Jiri Simsa, Satnam Singh, Viktor Vafeiadis.

In FMCAD 2009, pp. 205-212. IEEE (November 2009)

[Paper] [@IEEE]**Deny-guarantee reasoning.**

Mike Dodds, Xinyu Feng, Matthew Parkinson, Viktor Vafeiadis.

In ESOP 2009. LNCS, vol. 5502, pp. 363-377. Springer (March 2009)

[Paper] [@Springer] [Technical report]**Proving that nonblocking algorithms don't block.**

Alexey Gotsman, Byron Cook, Matthew Parkinson, Viktor Vafeiadis.

In POPL 2009, pp. 16-28. ACM (January 2009)

[Paper] [@ACM]**Shape-value abstraction for verifying linearizability.**

Viktor Vafeiadis.

In VMCAI 2009. LNCS, vol. 5403, pp. 335-348. Springer (January 2009)

[Paper] [@Springer] [Tool (Cave)]**A marriage of rely/guarantee and separation logic.**

Viktor Vafeiadis, Matthew Parkinson.

In CONCUR 2007. LNCS, vol. 4703, pp. 256-271. Springer (September 2007)

[Paper] [@Springer] [Technical report] [More...]**Modular safety checking for fine-grained concurrency.**

Cristiano Calcagno, Matthew Parkinson, Viktor Vafeiadis.

In SAS 2007. LNCS, vol. 4634, pp. 233-238. Springer (August 2007)

[Paper] [@Springer] [Tool (SmallfootRG)]**Proving correctness of highly-concurrent linearisable objects.**

Viktor Vafeiadis, Maurice Herlihy, Tony Hoare, Marc Shapiro.

In PPoPP 2006, pp. 129-136. ACM (March 2006)

[Paper] [@ACM] [Technical report]**Acute: High-level programming language design for distributed computation.**

Peter Sewell, James J. Leifer, Keith Wansbrough, Francesco Zappa Nardelli, Mair Allen-Williams, Pierre Habouzit, Viktor Vafeiadis.

In ICFP 2005, pp. 15-26. ACM (September 2005)

[Paper] [@ACM] [More...]

**Formal reasoning about the C11 weak memory model.**

Viktor Vafeiadis.

In CPP 2015, pp. 1-2. ACM (January 2015)

[Paper] [@ACM] [Slides]**A logical step forward in parametric bisimulations.**

Chung-Kil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis.

Technical report MPI-SWS-2014-003 (January 2014)

[Paper] [Project page with Coq scripts]**The transitive composability of relation transition systems.**

Chung-Kil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis.

Technical report MPI-SWS-2012-002 (April 2012)

[Paper] [Coq scripts]