See also: [By subject] [DBLP] [GoogleScholar]

PhD dissertation

Journal articles

  1. 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]
  2. 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...]
  3. Aspect-oriented linearizability proofs.
    Soham Chakraborty, Thomas A. Henzinger, Ali Sezgin, Viktor Vafeiadis.
    Logical Methods in Computer Science 11(1:20) (March 2015)
    [@LMCS]
  4. 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...]
  5. 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...]

Conference papers (peer-reviewed)

  1. Strong logic for weak memory: Reasoning about release-acquire consistency in Iris.
    Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, Viktor Vafeiadis.
    In ECOOP 2017 (June 2017)
    Best paper award at ECOOP'17
    [Paper] [More...]
  2. Promising compilation to ARMv8 POP.
    Anton Podkopaev, Ori Lahav, Viktor Vafeiadis.
    In ECOOP 2017 (June 2017)
    [Paper]
  3. Repairing sequential consistency in C/C++11.
    Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, Derek Dreyer.
    In PLDI 2017. ACM (June 2017)
    Distinguished paper award at PLDI'17
    [Paper] [More...]
  4. Tackling real-life relaxed concurrency with FSL++.
    Marko Doko, Viktor Vafeiadis.
    In ESOP 2017. LNCS 10201, pp. 448-475. Springer (April 2017)
    [Paper] [@Springer] [More...]
  5. Formalizing the concurrency semantics of an LLVM fragment.
    Soham Chakraborty, Viktor Vafeiadis.
    In CGO 2017, pp. 100-110. ACM (February 2017)
    [Paper] [@ACM] [More...]
  6. A promising semantics for relaxed-memory concurrency.
    Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer.
    In POPL 2017, pp. 175-189. ACM (January 2017)
    [Paper] [@ACM] [More...]
  7. Explaining relaxed memory models with program transformations.
    Ori Lahav, Viktor Vafeiadis.
    In FM 2016. LNCS 9995, pp. 479-495. Springer (November 2016)
    [Paper] [@Springer] [More...]
  8. Validating optimizations of concurrent C/C++ programs.
    Soham Chakraborty, Viktor Vafeiadis.
    In CGO 2016, pp. 216-226. ACM (March 2016)
    [Paper] [@ACM] [More...]
  9. Reasoning about fences and relaxed atomics.
    Mengda He, Viktor Vafeiadis, Shengchao Qin, João F. Ferreira.
    In PDP 2016, pp. 520-527. IEEE (February 2016)
    [Paper] [@IEEE]
  10. Taming release-acquire consistency.
    Ori Lahav, Nick Giannarakis, Viktor Vafeiadis.
    In POPL 2016, pp. 649-662. ACM (January 2016)
    [Paper] [@ACM] [More...]
  11. 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)
    [Paper] [@ACM] [More...]
  12. A program logic for C11 memory fences.
    Marko Doko, Viktor Vafeiadis.
    In VMCAI 2016, LNCS 9583, pp. 413-430. Springer (January 2016)
    [Paper] [@Springer] [More...]
  13. Modular verification of concurrency-aware linearizability.
    Nir Hemed, Noam Rinetzky, Viktor Vafeiadis.
    In DISC 2015, pp. 371-387 (October 2015)
    [Paper] [@Springer]
  14. 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...]
  15. 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]
  16. Asynchronous liquid separation types.
    Johannes Kloos, Rupak Majumdar, Viktor Vafeiadis.
    In ECOOP 2015, pp. 396-420 (July 2015)
    [Paper] [@LIPIcs] [More...]
  17. Owicki-Gries reasoning for weak memory models.
    Ori Lahav, Viktor Vafeiadis.
    In ICALP 2015, Track B. LNCS 9135, pp. 311-323. Springer (July 2015)
    [Paper] [@Springer] [More...]
  18. 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...]
  19. 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...]
  20. 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...]
  21. Proving lock-freedom easily and automatically.
    Xiao Jia, Wei Li, Viktor Vafeiadis.
    In CPP 2015, pp. 119-127. ACM (January 2015)
    [Paper] [@ACM] [More...]
  22. 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...]
  23. Automating the choices of consistency levels in replicated systems.
    Cheng Li, João Leitão, Allen Clement, Nuno Preguiça, Rodrigo Rodrigues, Viktor Vafeiadis
    In USENIX ATC 2014, pp. 281-292. USENIX (June 2014)
    [Paper] [@USENIX]
  24. 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...]
  25. 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)]
  26. Aspect-oriented linearizability proofs.
    Thomas A. Henzinger, Ali Sezgin, Viktor Vafeiadis.
    In CONCUR 2013. LNCS 8052, pp. 242-256. Springer (August 2013)
    [Paper] [@Springer]
  27. Adjustable references.
    Viktor Vafeiadis.
    In ITP 2013. LNCS 7998, pp. 328-337. Springer (July 2013)
    [Paper] [@Springer] [More...]
  28. 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...]
  29. 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)]
  30. 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...]
  31. Verifying fence elimination optimisations.
    Viktor Vafeiadis, Francesco Zappa Nardelli.
    In SAS 2011. LNCS 6887, pp. 146-162. Springer (September 2011)
    [Paper] [@Springer] [More...]
  32. Concurrent separation logic and operational semantics.
    Viktor Vafeiadis.
    In MFPS 2011. ENTCS 276, pp. 335-351. Elsevier (September 2011)
    [Paper] [@Elsevier] [More...]
  33. 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]
  34. 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...]
  35. Automatically proving linearizability.
    Viktor Vafeiadis.
    In CAV 2010. LNCS 6174, pp. 450-464. Springer (July 2010)
    [Paper] [@Springer] [Technical report] [Tool (Cave)]
  36. Concurrent abstract predicates.
    Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew Parkinson, Viktor Vafeiadis.
    In ECOOP 2010. LNCS 6183, pp. 504-528. Springer (June 2010)
    [Paper] [@Springer] [Technical report]
  37. RGSep action inference.
    Viktor Vafeiadis.
    In VMCAI 2010. LNCS 5944, pp. 345-361. Springer (January 2010)
    [Paper] [@Springer] [Tool (Cave)]
  38. 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]
  39. Bi-abductive resource invariant synthesis.
    Cristiano Calcagno, Dino Distefano, Viktor Vafeiadis.
    In APLAS 2009. LNCS 5904, pp. 259-274. Springer (December 2009)
    [Paper] [@Springer]
  40. 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]
  41. Deny-guarantee reasoning.
    Mike Dodds, Xinyu Feng, Matthew Parkinson, Viktor Vafeiadis.
    In ESOP 2009. LNCS 5502, pp. 363-377. Springer (March 2009)
    [Paper] [@Springer] [Technical report]
  42. 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]
  43. Shape-value abstraction for verifying linearizability.
    Viktor Vafeiadis.
    In VMCAI 2009. LNCS 5403, pp. 335-348. Springer (January 2009)
    [Paper] [@Springer] [Tool (Cave)]
  44. A marriage of rely/guarantee and separation logic.
    Viktor Vafeiadis, Matthew Parkinson.
    In CONCUR 2007. LNCS 4703, pp. 256-271. Springer (September 2007)
    [Paper] [@Springer] [Technical report] [More...]
  45. Modular safety checking for fine-grained concurrency.
    Cristiano Calcagno, Matthew Parkinson, Viktor Vafeiadis.
    In SAS 2007. LNCS 4634, pp. 233-238. Springer (August 2007)
    [Paper] [@Springer] [Tool (SmallfootRG)]
  46. 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]
  47. 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...]

Position papers and technical reports

Valid XHTML 1.0 Strict