???global.info.a_carregar???
Identification

Personal identification

Full name
Viktor Vafeiadis

Citation names

  • Vafeiadis, Viktor

Author identifiers

Ciência ID
D11F-ED29-9981
ORCID iD
0000-0001-8436-0334

Websites

Knowledge fields

  • Exact Sciences - Computer and Information Sciences - Computer Sciences

Languages

Language Speaking Reading Writing Listening Peer-review
Greek (Mother tongue)
English Proficiency (C2) Proficiency (C2) Proficiency (C2) Proficiency (C2) Proficiency (C2)
Education
Degree Classification
2004 - 2008
Concluded
 PhD in Computer Science (Doctor of Philosophy)
University of Cambridge, United Kingdom
"Modular fine-grained concurrency verification" (THESIS/DISSERTATION)
2001 - 2004
Concluded
 BA Hons in Computer Science (Bachelor)
University of Cambridge, United Kingdom
Affiliation

Science

Category
Host institution 		Employer
2010 - Current Researcher (Research) Max-Planck-Institut für Softwaresysteme, Germany
2010 - 2010 Postdoc (Research) University of Cambridge, United Kingdom
2008 - 2009 Postdoc (Research) Microsoft Research Ltd, United Kingdom
2005 - 2007 Research Trainee (Research) Microsoft Research Ltd, United Kingdom
Projects

Grant

Designation Funders
2021 - 2025 PERSIST: A Semantic Foundation for Persistent Programming
ERC Consolidator Grant 101003349
Principal investigator
Max-Planck-Institut für Softwaresysteme, Germany
 European Research Council
Ongoing

Contract

Designation Funders
2013 - 2016 ADVENT: Architecture-driven verification of systems software
FET Young Explorers 308830
Principal investigator
Max-Planck-Institut für Softwaresysteme, Germany
 European Commission Seventh Framework Programme for Research and Technological Development Information and Communication Technologies
Concluded
Outputs

Publications

Book
  1. Abdulla, P.A.; Atig, M.F.; Godbole, A.; Krishna, S.; Vafeiadis, V.. The Decidability of Verification under PS 2.0. 2021.
    10.1007/978-3-030-72019-3_1
  2. Kokologiannakis, M.; Vafeiadis, V.. GenMC: A Model Checker for Weak Memory Models. 2021.
    10.1007/978-3-030-81685-8_20
  3. Oberhauser, J.; Oberhauser, L.; Paolillo, A.; Behrens, D.; Fu, M.; Vafeiadis, V.. Verifying and Optimizing the HMCS Lock for Arm Servers. 2021.
    10.1007/978-3-030-91014-3_17
  4. Kokologiannakis, M.; Vafeiadis, V.. BAM: Efficient Model Checking for Barriers. 2021.
    10.1007/978-3-030-91014-3_16
  5. Raad, A.; Lahav, O.; Vafeiadis, V.. On the semantics of snapshot isolation. 2019.
    10.1007/978-3-030-11245-5_1
  6. Svendsen, K.; Pichon-Pharabod, J.; Doko, M.; Lahav, O.; Vafeiadis, V.. A separation logic for a promising semantics. 2018.
    10.1007/978-3-319-89884-1_13
  7. Raad, A.; Lahav, O.; Vafeiadis, V.. On parallel snapshot isolation and release/acquire consistency. 2018.
    10.1007/978-3-319-89884-1_33
  8. Vafeiadis, V.. Program verification under weak memory consistency using separation logic. 2017.
    10.1007/978-3-319-63387-9_2
  9. Doko, M.; Vafeiadis, V.. Tackling real-life relaxed concurrency with FSL++. 2017.
    10.1007/978-3-662-54434-1_17
  10. Lahav, O.; Vafeiadis, V.. Explaining relaxed memory models with program transformations. 2016.
    10.1007/978-3-319-48989-6_29
  11. Doko, M.; Vafeiadis, V.. A program logic for c11 memory fences. 2016.
    10.1007/978-3-662-49122-5_20
  12. Lahav, O.; Vafeiadis, V.. Owicki-Gries reasoning for weak memory models. 2015.
    10.1007/978-3-662-47666-6_25
  13. Hemed, N.; Rinetzky, N.; Vafeiadis, V.. Modular verification of concurrency-aware linearizability. 2015.
    10.1007/978-3-662-48653-5_25
  14. Henzinger, T.A.; Sezgin, A.; Vafeiadis, V.. Aspect-oriented linearizability proofs. 2013.
    10.2168/LMCS-11(1:20)2015
  15. Vafeiadis, V.. Adjustable references. 2013.
    10.1007/978-3-642-39634-2_24
  16. Vafeiadis, V.; Zappa Nardelli, F.. Verifying fence elimination optimisations. 2011.
    10.1007/978-3-642-23702-7_14
  17. Vafeiadis, V.. RGSep action inference. 2010.
    10.1007/978-3-642-11319-2_25
  18. Dinsdale-Young, T.; Dodds, M.; Gardner, P.; Parkinson, M.J.; Vafeiadis, V.. Concurrent abstract predicates. 2010.
    10.1007/978-3-642-14107-2_24
  19. Vafeiadis, V.. Automatically proving linearizability. 2010.
    10.1007/978-3-642-14295-6_40
  20. Calcagno, C.; Distefano, D.; Vafeiadis, V.. Bi-abductive resource invariant synthesis. 2009.
    10.1007/978-3-642-10672-9_19
  21. Vafeiadis, V.. Shape-value abstraction for verifying linearizability. 2009.
    10.1007/978-3-540-93900-9_27
  22. Dodds, M.; Feng, X.; Parkinson, M.; Vafeiadis, V.. Deny-guarantee reasoning. 2009.
    10.1007/978-3-642-00590-9_26
Conference paper
  1. Oberhauser, J.; Chehab, R.L.D.L.; Behrens, D.; Fu, M.; Paolillo, A.; Oberhauser, L.; Bhat, K.; et al. "VSync: Push-button verification and optimization for synchronization primitives on weak memory models". 2021.
    10.1145/3445814.3446748
  2. Vafeiadis, V.. "The challenges of weak persistency". 2021.
    10.4230/LIPIcs.CALCO.2021.4
  3. Kokologiannakis, M.; Ren, X.; Vafeiadis, V.. "Dynamic Partial Order Reductions for Spinloops". 2021.
    10.34727/2021/isbn.978-3-85448-046-4_25
  4. Lee, S.-H.; Cho, M.; Podkopaev, A.; Chakraborty, S.; Hur, C.-K.; Lahav, O.; Vafeiadis, V.. "Promising 2.0: Global optimizations in relaxed memory concurrency". 2020.
    10.1145/3385412.3386010
  5. Moiseenko, E.; Podkopaev, A.; Lahav, O.; Melkonian, O.; Vafeiadis, V.. "Reconciling event structures with modern multiprocessors". 2020.
    10.4230/LIPIcs.ECOOP.2020.5
  6. Kokologiannakis, M.; Vafeiadis, V.. "HMC: Model checking for hardware memory models". 2020.
    10.1145/3373376.3378480
  7. Kokologiannakis, M.; Raad, A.; Vafeiadis, V.. "Model checking for weakly consistent libraries". 2019.
    10.1145/3314221.3314609
  8. Li, C.; Leitão, J.; Clement, A.; Preguiça, N.; Rodrigues, R.; Vafeiadis, V.. "Automating the choice of consistency levels in replicated systems". 2019.
  9. Bertot, Y.; Vafeiadis, V.. "Welcome from the chairs". 2017.
  10. Kaiser, J.-O.; Dang, H.-H.; Dreyer, D.; Lahav, O.; Vafeiadis, V.. "Strong logic for weak memory: Reasoning about release-acquire consistency in iris". 2017.
    10.4230/LIPIcs.ECOOP.2017.17
  11. Kang, J.; Hur, C.-K.; Lahav, O.; Vafeiadis, V.; Dreyer, D.. "A promising semantics for relaxed-memory concurrency". 2017.
    10.1145/3009837.3009850
  12. Podkopaev, A.; Lahav, O.; Vafeiadis, V.. "Promising compilation to ARMv8 POP". 2017.
    10.4230/LIPIcs.ECOOP.2017.22
  13. Lahav, O.; Vafeiadis, V.; Kang, J.; Hur, C.-K.; Dreyer, D.. "Repairing sequential consistency in C/C++11". 2017.
    10.1145/3062341.3062352
  14. Chakraborty, S.; Vafeiadis, V.. "Formalizing the concurrency semantics of an LLVM fragment". 2017.
    10.1109/CGO.2017.7863732
  15. Chakraborty, S.; Vafeiadis, V.. "Validating optimizations of concurrent C/C++ programs". 2016.
    10.1145/2854038.2854051
  16. He, M.; Vafeiadis, V.; Qin, S.; Ferreira, J.F.. "Reasoning about Fences and Relaxed Atomics". 2016.
    10.1109/PDP.2016.103
  17. Lahav, O.; Giannarakis, N.; Vafeiadis, V.. "Taming release-acquire consistency". 2016.
    10.1145/2837614.2837643
  18. Kang, J.; Kim, Y.; Hur, C.-K.; Dreyer, D.; Vafeiadis, V.. "Lightweight verification of separate compilation". 2016.
    10.1145/2837614.2837642
  19. Vafeiadis, V.; Balabonski, T.; Chakraborty, S.; Morisset, R.; Nardelli, F.Z.. "Common compiler optimisations are invalid in the C11 memory model and what we can do about it". 2015.
    10.1145/2676726.2676995
  20. Gavran, I.; Niksic, F.; Kanade, A.; Majumdar, R.; Vafeiadis, V.. "Rely/guarantee reasoning for asynchronous programs". 2015.
    10.4230/LIPIcs.CONCUR.2015.483
  21. Vafeiadis, V.. "Formal reasoning about the C11 weak memory model". 2015.
    10.1145/2676724.2693181
  22. Jia, X.; Li, W.; Vafeiadis, V.. "Proving lock-freedom easily and automatically". 2015.
    10.1145/2676724.2693179
  23. Kloos, J.; Majumdar, R.; Vafeiadis, V.. "Asynchronous liquid separation types". 2015.
    10.4230/LIPIcs.ECOOP.2015.396
  24. Turon, A.; Vafeiadis, V.; Dreyer, D.. "GPS: Navigating weak memory with ghosts, protocols, and separation". 2014.
    10.1145/2660193.2660243
  25. Ziliani, B.; Dreyer, D.; Krishnaswami, N.R.; Nanevski, A.; Vafeiadis, V.. "Mtac: A monad for typed tactic programming in Coq". 2013.
    10.1017/S0956796815000118
  26. Zengin, M.; Vafeiadis, V.. "A programming language approach to fault tolerance for fork-join parallelism". 2013.
    10.1109/TASE.2013.22
  27. Vafeiadis, V.; Narayan, C.. "Relaxed separation logic: A program logic for C11 concurrency". 2013.
    10.1145/2509136.2509532
  28. Hur, C.-K.; Dreyer, D.; Vafeiadis, V.. "Separation logic in the presence of garbage collection". 2011.
    10.1109/LICS.2011.46
  29. Nanevski, A.; Vafeiadis, V.; Berdine, J.. "Structuring the verification of heap-manipulating programs". 2010.
    10.1145/1706299.1706331
  30. Cook, B.; Gupta, A.; Magill, S.; Rybalchenko, A.; Simsa, J.; Singh, S.; Vafeiadis, V.. "Finding heap-bounds for hardware synthesis". 2009.
    10.1109/FMCAD.2009.5351120
  31. Gotsman, A.; Cook, B.; Parkinson, M.; Vafeiadis, V.. "Proving that non-blocking algorithms don't block". 2009.
    10.1145/1480881.1480886
Journal article
  1. Kokologiannakis, M.; Marmanis, I.; Gladstein, V.; Vafeiadis, V.. "Truly stateless, optimal dynamic partial order reduction". Proceedings of the ACM on Programming Languages 6 POPL (2022): http://www.scopus.com/inward/record.url?eid=2-s2.0-85123209521&partnerID=MN8TOARS.
    10.1145/3498711
  2. Raad, A.; Maranget, L.; Vafeiadis, V.. "Extending Intel-x86 consistency and persistency: Formalising the semantics of Intel-x86 memory types and non-Temporal stores". Proceedings of the ACM on Programming Languages 6 POPL (2022): http://www.scopus.com/inward/record.url?eid=2-s2.0-85123195819&partnerID=MN8TOARS.
    10.1145/3498683
  3. Lahav, O.; Namakonov, E.; Oberhauser, J.; Podkopaev, A.; Vafeiadis, V.. "Making weak memory models fair". Proceedings of the ACM on Programming Languages 5 OOPSLA (2021): http://www.scopus.com/inward/record.url?eid=2-s2.0-85115860610&partnerID=MN8TOARS.
    10.1145/3485475
  4. Kokologiannakis, M.; Kaysin, I.; Raad, A.; Vafeiadis, V.. "PerSeVerE: Persistency semantics for verification under ext4". Proceedings of the ACM on Programming Languages 5 POPL (2021): http://www.scopus.com/inward/record.url?eid=2-s2.0-85099061457&partnerID=MN8TOARS.
    10.1145/3434324
  5. Raad, A.; Wickerson, J.; Neiger, G.; Vafeiadis, V.. "Persistency semantics of the intel-x86 architecture". Proceedings of the ACM on Programming Languages 4 POPL (2020): http://www.scopus.com/inward/record.url?eid=2-s2.0-85089761998&partnerID=MN8TOARS.
    10.1145/3371079
  6. Raad, A.; Lahav, O.; Vafeiadis, V.. "Persistent Owicki-Gries reasoning: A program logic for reasoning about persistent programs on Intel-x86". Proceedings of the ACM on Programming Languages 4 OOPSLA (2020): http://www.scopus.com/inward/record.url?eid=2-s2.0-85097585673&partnerID=MN8TOARS.
    10.1145/3428219
  7. Chakraborty, S.; Vafeiadis, V.. "Grounding thin-air reads with event structures". Proceedings of the ACM on Programming Languages 3 POPL (2019): http://www.scopus.com/inward/record.url?eid=2-s2.0-85120138097&partnerID=MN8TOARS.
    10.1145/3290383
  8. Podkopaev, A.; Lahav, O.; Vafeiadis, V.. "Bridging the gap between programming languages and hardware weak memory models". Proceedings of the ACM on Programming Languages 3 POPL (2019): http://www.scopus.com/inward/record.url?eid=2-s2.0-85067676825&partnerID=MN8TOARS.
    10.1145/3290382
  9. Kokologiannakis, M.; Raad, A.; Vafeiadis, V.. "Effective lock handling in stateless model checking". Proceedings of the ACM on Programming Languages 3 OOPSLA (2019): http://www.scopus.com/inward/record.url?eid=2-s2.0-85089765590&partnerID=MN8TOARS.
    10.1145/3360599
  10. Raad, A.; Doko, M.; Rožic, L.; Lahav, O.; Vafeiadis, V.. "On library correctness under weak memory consistency specifying and verifying concurrent libraries under declarative consistency models". Proceedings of the ACM on Programming Languages 3 POPL (2019): http://www.scopus.com/inward/record.url?eid=2-s2.0-85120109852&partnerID=MN8TOARS.
    10.1145/3290381
  11. Raad, A.; Wickerson, J.; Vafeiadis, V.. "Weak persistency semantics from the ground up formalising the persistency semantics of ARMv8 and transactional models". Proceedings of the ACM on Programming Languages 3 OOPSLA (2019): http://www.scopus.com/inward/record.url?eid=2-s2.0-85120094999&partnerID=MN8TOARS.
    10.1145/3360561
  12. He, M.; Vafeiadis, V.; Qin, S.; Ferreira, J.F.. "GPS + : Reasoning About Fences and Relaxed Atomics". International Journal of Parallel Programming 46 6 (2018): 1157-1183. http://www.scopus.com/inward/record.url?eid=2-s2.0-85029906820&partnerID=MN8TOARS.
    10.1007/s10766-017-0518-x
  13. Kokologiannakis, M.; Lahav, O.; Sagonas, K.; Vafeiadis, V.. "Effective stateless model checking for C/C++ concurrency". Proceedings of the ACM on Programming Languages 2 POPL (2018): http://www.scopus.com/inward/record.url?eid=2-s2.0-85120105923&partnerID=MN8TOARS.
    10.1145/3158105
  14. Raad, A.; Vafeiadis, V.. "Persistence semantics for weak memory". Proceedings of the ACM on Programming Languages 2 OOPSLA (2018): http://www.scopus.com/inward/record.url?eid=2-s2.0-85120136622&partnerID=MN8TOARS.
    10.1145/3276507
  15. Neis, G.; Hur, C.-K.; Kaiser, J.-O.; McLaughlin, C.; Dreyer, D.; Vafeiadis, V.. "Pilsner: A compositionally verified compiler for a higher-order imperative language". ACM SIGPLAN Notices 50 9 (2015): 166-178. http://www.scopus.com/inward/record.url?eid=2-s2.0-85112820852&partnerID=MN8TOARS.
    10.1145/2784731.2784764
  16. Kang, J.; Hur, C.-K.; Mansky, W.; Garbuzov, D.; Zdancewic, S.; Vafeiadis, V.. "A formal C memory model supporting integer-pointer casts". ACM SIGPLAN Notices 50 6 (2015): 326-335. http://www.scopus.com/inward/record.url?eid=2-s2.0-84951124762&partnerID=MN8TOARS.
    10.1145/2737924.2738005
  17. Tassarotti, J.; Dreyer, D.; Vafeiadis, V.. "Verifying read-copy-update in a logic for weak memory". ACM SIGPLAN Notices 50 6 (2015): 110-120. http://www.scopus.com/inward/record.url?eid=2-s2.0-84951002614&partnerID=MN8TOARS.
    10.1145/2737924.2737992
  18. Ševcík, J.; Vafeiadis, V.; Nardelli, F.Z.; Jagannathan, S.; Sewell, P.. "CompCertTSO: A verified compiler for relaxed-memory concurrency". Journal of the ACM 60 3 (2013): http://www.scopus.com/inward/record.url?eid=2-s2.0-84880356634&partnerID=MN8TOARS.
    10.1145/2487241.2487248
  19. Hur, C.-K.; Neis, G.; Dreyer, D.; Vafeiadis, V.. "The power of parameterization in coinductive proof". ACM SIGPLAN Notices 48 1 (2013): 193-205. http://www.scopus.com/inward/record.url?eid=2-s2.0-84877898390&partnerID=MN8TOARS.
    10.1145/2429069.2429093
  20. Hur, C.-K.; Dreyer, D.; Neis, G.; Vafeiadis, V.. "The marriage of bisimulations and Kripke logical relations". ACM SIGPLAN Notices 47 1 (2012): 59-72. http://www.scopus.com/inward/record.url?eid=2-s2.0-84857167050&partnerID=MN8TOARS.
    10.1145/2103656.2103666
  21. Vafeiadis, V.. "Concurrent separation logic and operational semantics". Electronic Notes in Theoretical Computer Science 276 1 (2011): 335-351. http://www.scopus.com/inward/record.url?eid=2-s2.0-80054882854&partnerID=MN8TOARS.
    10.1016/j.entcs.2011.09.029
  22. Ševcík, J.; Vafeiadis, V.; Nardelli, F.Z.; Jagannathan, S.; Sewell, P.. "Relaxed-memory concurrency and verified compilation". ACM SIGPLAN Notices 46 1 (2011): 43-54. http://www.scopus.com/inward/record.url?eid=2-s2.0-79251546778&partnerID=MN8TOARS.
    10.1145/1925844.1926393
  23. Vafeiadis, V.; Parkinson, M.. "A marriage of rely/guarantee and separation logic". Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 4703 LNCS (2007): 256-271. http://www.scopus.com/inward/record.url?eid=2-s2.0-38149033563&partnerID=MN8TOARS.
  24. Calcagno, C.; Parkinson, M.; Vafeiadis, V.. "Modular safety checking for fine-grained concurrency". Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 4634 LNCS (2007): 233-248. http://www.scopus.com/inward/record.url?eid=2-s2.0-38149043440&partnerID=MN8TOARS.
  25. Sewell, P.; Leifer, J.J.; Wansbrough, K.; Zappa Nardelli, F.; Allen-Williams, M.; Habouzit, P.; Vafeiadis, V.. "Acute: High-level programming language design for distributed computation". Journal of Functional Programming 17 4-5 (2007): 547-612. http://www.scopus.com/inward/record.url?eid=2-s2.0-34547725597&partnerID=MN8TOARS.
    10.1017/S0956796807006442
  26. Vafeiadis, V.; Herlihy, M.; Hoare, T.; Shapiro, M.. "Proving correctness of highly-concurrent linearisable objects". Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP 2006 (2006): 129-136. http://www.scopus.com/inward/record.url?eid=2-s2.0-33749871295&partnerID=MN8TOARS.

Other

Other output
  1. VSYNC: Push-button verification and optimization for synchronization primitives on weak memory models (technical report). 2021. Oberhauser, J.; de Lima Chehab, R.L.; Behrens, D.; Fu, M.; Paolillo, A.; Oberhauser, L.; Bhat, K.; et al. http://www.scopus.com/inward/record.url?eid=2-s2.0-85101839267&partnerID=MN8TOARS.
  2. The Decidability of Verification under Promising 2.0. 2020. Abdulla, P.A.; Atig, M.F.; Godbole, A.; Krishna, S.N.; Vafeiadis, V.. http://www.scopus.com/inward/record.url?eid=2-s2.0-85095360802&partnerID=MN8TOARS.
  3. Making weak memory models fair. 2020. Lahav, O.; Namakonov, E.; Oberhauser, J.; Podkopaev, A.; Vafeiadis, V.. http://www.scopus.com/inward/record.url?eid=2-s2.0-85117394199&partnerID=MN8TOARS.
  4. Reconciling event structures with modern multiprocessors. 2019. Moiseenko, E.; Podkopaev, A.; Lahav, O.; Melkonian, O.; Vafeiadis, V.. http://www.scopus.com/inward/record.url?eid=2-s2.0-85093192013&partnerID=MN8TOARS.
  5. On the semantics of snapshot isolation. 2018. Raad, A.; Lahav, O.; Vafeiadis, V.. http://www.scopus.com/inward/record.url?eid=2-s2.0-85093125190&partnerID=MN8TOARS.
  6. Bridging the gap between programming languages and hardware weak memory models. 2018. Podkopaev, A.; Lahav, O.; Vafeiadis, V.. http://www.scopus.com/inward/record.url?eid=2-s2.0-85093416497&partnerID=MN8TOARS.
Activities

Oral presentation

Presentation title Event name
Host (Event location)
2021 Keynote: The challenges of weak persistency CALCO 2021
2021 PLDI Tutorial: Beyond Weak Memory Consistency: The Challenges of Memory Persistency PLDI 2021
2017 Keynote: Program verification under weak memory consistency using separation logic CAV 2017
2017 CONCUR Tutorial: An introduction to weak memory consistency and the out-of-thin-air problem CONCUR 2017
2015 Keynote: Formal reasoning about the C11 weak memory model CPP 2015
2014 POPL Tutorial: Relaxed separation logic POPL 2014
2011 FM Tutorial: Rely/Guarantee-thinking and Separation Logic FM 2011

Supervision

Thesis Title
Role 		Degree Subject (Type)
Institution / Organization
2021 - Current Postdoc supervision on reasoning about concurrent and persistent programs
Supervisor of Léo Stefanesco
Max-Planck-Institut für Softwaresysteme, Germany
2021 - Current Model checking for concurrency
Supervisor
Max-Planck-Institut für Softwaresysteme, Germany
2018 - Current Stateless model checking for verifying C/C++ programs under weak memory models
Supervisor
Max-Planck-Institut für Softwaresysteme, Germany
2014 - Current Postdoc supervision on program logics for structured reasoning about weak memory
Supervisor
Max-Planck-Institut für Softwaresysteme, Germany
2013 - 2021 Program Logic for Weak Memory Concurrency
Supervisor of Marko Dodo
2019 - 2020 Postdoc supervision on Hardware Weak Memory Models
Supervisor
Max-Planck-Institut für Softwaresysteme, Germany
2014 - 2019 Correct Compilation of Relaxed Memory Concurrency
Supervisor of Soham Chakraborty
2015 - 2017 Postdoc supervision on Weak Concurrency
Co-supervisor
Max-Planck-Institut für Softwaresysteme, Germany
2015 - 2017 Postdoc supervision on weak consistency and weak persistency
Co-supervisor
Max-Planck-Institut für Softwaresysteme, Germany
2010 - 2012 Postdoc supervision on Relaxed-Memory Concurrency
Supervisor
Max-Planck-Institut für Softwaresysteme, Germany

Event organisation

Event name
Type of event (Role) 		Institution / Organization
2017 - 2017 Program chair for CPP 2017 (2017)
Conference

Conference scientific committee

Conference name Conference host
2021 - 2021 OOPSLA 2021
2021 - 2021 PLDI 2021
2021 - 2021 POPL 2021 POPL 2021
2020 - 2020 ESOP 2020
2018 - 2018 POPL 2018

Course / Discipline taught

Academic session Degree Subject (Type) Institution / Organization
2019 - Current Program Verification Under Weak Memory Consistency (Summer School Marktoberdorf 2019)
Distinctions

Award

2008 ACM SIGPLAN 2008 Outstanding Doctoral Dissertation Award
2004 Gates Cambridge Fellow
Microsoft Research Ltd, United Kingdom
2003 Best CS undergraduate thesis; best CS student of my year (twice) at Cambridge
University of Cambridge, United Kingdom