???global.info.a_carregar???
Identificação

Identificação pessoal

Nome completo
Viktor Vafeiadis

Nomes de citação

  • Vafeiadis, Viktor

Identificadores de autor

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

Websites

Domínios de atuação

  • Ciências Exatas - Ciências da Computação e da Informação - Ciências da Computação

Idiomas

Idioma Conversação Leitura Escrita Compreensão Peer-review
Grego (Idioma materno)
Inglês Utilizador proficiente (C2) Utilizador proficiente (C2) Utilizador proficiente (C2) Utilizador proficiente (C2) Utilizador proficiente (C2)
Formação
Grau Classificação
2004 - 2008
Concluído
 PhD in Computer Science (Doctor of Philosophy)
University of Cambridge, Reino Unido
"Modular fine-grained concurrency verification" (TESE/DISSERTAÇÃO)
2001 - 2004
Concluído
 BA Hons in Computer Science (Bachelor)
University of Cambridge, Reino Unido
Percurso profissional

Ciência

Categoria Profissional
Instituição de acolhimento 		Empregador
2010 - Atual Investigador (Investigação) Max-Planck-Institut für Softwaresysteme, Alemanha
2010 - 2010 Pós-doutorado (Investigação) University of Cambridge, Reino Unido
2008 - 2009 Pós-doutorado (Investigação) Microsoft Research Ltd, Reino Unido
2005 - 2007 Estagiário de Investigação (Investigação) Microsoft Research Ltd, Reino Unido
Projetos

Bolsa

Designação Financiadores
2021 - 2025 PERSIST: A Semantic Foundation for Persistent Programming
ERC Consolidator Grant 101003349
Investigador responsável
Max-Planck-Institut für Softwaresysteme, Alemanha
 European Research Council
Em curso

Projeto

Designação Financiadores
2013 - 2016 ADVENT: Architecture-driven verification of systems software
FET Young Explorers 308830
Investigador responsável
Max-Planck-Institut für Softwaresysteme, Alemanha
 European Commission Seventh Framework Programme for Research and Technological Development Information and Communication Technologies
Concluído
Produções

Publicações

Artigo em conferência
  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
Artigo em revista
  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.
Livro
  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

Outros

Outra produção
  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.
Atividades

Apresentação oral de trabalho

Título da apresentação Nome do evento
Anfitrião (Local do evento)
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

Orientação

Título / Tema
Papel desempenhado 		Curso (Tipo)
Instituição / Organização
2021 - Atual Postdoc supervision on reasoning about concurrent and persistent programs
Orientador de Léo Stefanesco
Max-Planck-Institut für Softwaresysteme, Alemanha
2021 - Atual Model checking for concurrency
Orientador
Max-Planck-Institut für Softwaresysteme, Alemanha
2018 - Atual Stateless model checking for verifying C/C++ programs under weak memory models
Orientador
Max-Planck-Institut für Softwaresysteme, Alemanha
2014 - Atual Postdoc supervision on program logics for structured reasoning about weak memory
Orientador
Max-Planck-Institut für Softwaresysteme, Alemanha
2013 - 2021 Program Logic for Weak Memory Concurrency
Orientador de Marko Dodo
2019 - 2020 Postdoc supervision on Hardware Weak Memory Models
Orientador
Max-Planck-Institut für Softwaresysteme, Alemanha
2014 - 2019 Correct Compilation of Relaxed Memory Concurrency
Orientador de Soham Chakraborty
2015 - 2017 Postdoc supervision on Weak Concurrency
Coorientador
Max-Planck-Institut für Softwaresysteme, Alemanha
2015 - 2017 Postdoc supervision on weak consistency and weak persistency
Coorientador
Max-Planck-Institut für Softwaresysteme, Alemanha
2010 - 2012 Postdoc supervision on Relaxed-Memory Concurrency
Orientador
Max-Planck-Institut für Softwaresysteme, Alemanha

Organização de evento

Nome do evento
Tipo de evento (Tipo de participação) 		Instituição / Organização
2017 - 2017 Program chair for CPP 2017 (2017)
Conferência

Arbitragem científica em conferência

Nome da conferência Local da conferência
2021 - 2021 OOPSLA 2021
2021 - 2021 PLDI 2021
2021 - 2021 POPL 2021 POPL 2021
2020 - 2020 ESOP 2020
2018 - 2018 POPL 2018

Curso / Disciplina lecionado

Disciplina Curso (Tipo) Instituição / Organização
2019 - Atual Program Verification Under Weak Memory Consistency (Summer School Marktoberdorf 2019)
Distinções

Prémio

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