Edit Profile Vafeiadis, Viktor Compute Distance To: Compute Author ID: vafeiadis.viktor Published as: Vafeiadis, Viktor Documents Indexed: 33 Publications since 2005 all top 5 Co-Authors 4 single-authored 7 Dreyer, Derek R. 7 Lahav, Ori 5 Hur, Chung-Kil 5 Zappa Nardelli, Francesco 4 Parkinson, Matthew J. 4 Sewell, Peter 3 Doko, Marko 3 Nanevski, Aleksandar 3 Neis, Georg 2 Allen-Williams, Mair 2 Chakraborty, Soham 2 Habouzit, Pierre 2 Henzinger, Thomas A. 2 Jagannathan, Suresh 2 Kang, Jeehoon 2 Krishnaswami, Neelakantan R. 2 Leifer, James J. 2 Raad, Azalea 2 Ševčík, Jaroslav 2 Sezgin, Ali 2 Wansbrough, Keith 2 Ziliani, Beta 1 Balabonski, Thibaut 1 Berdine, Josh 1 Calcagno, Cristiano 1 Cook, Byron 1 Dodds, Mike 1 Feng, Xinyu 1 Gavran, Ivan 1 Giannarakis, Nick 1 Gotsman, Alexey 1 Hemed, Nir 1 Kaiser, Jan-Oliver 1 Kanade, Aditya 1 Kim, Yoonseung 1 Majumdar, Rupak 1 McLaughlin, Craig A. 1 Morisset, Robin 1 Niksic, Filip 1 Pichon-Pharabod, Jean 1 Rinetzky, Noam 1 Svendsen, Kasper Serials 2 Journal of Functional Programming 1 Journal of the ACM 1 Logical Methods in Computer Science Fields 33 Computer science (68-XX) 5 Mathematical logic and foundations (03-XX) 1 Order, lattices, ordered algebraic structures (06-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH 25 Publications have been cited 148 times in 109 Documents Cited by ▼ Year ▼ A marriage of rely/guarantee and separation logic. Zbl 1151.68556Vafeiadis, Viktor; Parkinson, Matthew 31 2007 The power of parameterization in coinductive proof. Zbl 1301.68220Hur, Chung-Kil; Neis, Georg; Dreyer, Derek; Vafeiadis, Viktor 15 2013 Modular safety checking for fine-grained concurrency. Zbl 1211.68082Calcagno, Cristiano; Parkinson, Matthew; Vafeiadis, Viktor 13 2007 Proving that non-blocking algorithms don’t block. Zbl 1315.68093Gotsman, Alexey; Cook, Byron; Parkinson, Matthew; Vafeiadis, Viktor 11 2009 Deny-guarantee reasoning. Zbl 1234.68075Dodds, Mike; Feng, Xinyu; Parkinson, Matthew; Vafeiadis, Viktor 9 2009 CompCertTSO: a verified compiler for relaxed-memory concurrency. Zbl 1281.68072Ševčík, Jaroslav; Vafeiadis, Viktor; Zappa Nardelli, Francesco; Jagannathan, Suresh; Sewell, Peter 8 2013 Aspect-oriented linearizability proofs. Zbl 1390.68213Henzinger, Thomas A.; Sezgin, Ali; Vafeiadis, Viktor 7 2013 Acute: high-level programming language design for distributed computation. Zbl 1125.68023Sewell, Peter; Leifer, James J.; Wansbrough, Keith; Nardelli, Francesco Zappa; Allen-Williams, Mair; Habouzit, Pierre; Vafeiadis, Viktor 7 2007 The marriage of bisimulations and Kripke logical relations. Zbl 1321.68198Hur, Chung-Kil; Dreyer, Derek; Neis, Georg; Vafeiadis, Viktor 6 2012 Mtac: a monad for typed tactic programming in Coq. Zbl 1323.68236Ziliani, Beta; Dreyer, Derek; Krishnaswami, Neelakantan R.; Nanevski, Aleksandar; Vafeiadis, Viktor 5 2013 Concurrent separation logic and operational semantics. Zbl 1342.68104Vafeiadis, Viktor 5 2011 Pilsner: a compositionally verified compiler for a higher-order imperative language. Zbl 1360.68350Neis, Georg; Hur, Chung-Kil; Kaiser, Jan-Oliver; McLaughlin, Craig; Dreyer, Derek; Vafeiadis, Viktor 3 2015 Common compiler optimisations are invalid in the C11 memory model and what we can do about it. Zbl 1345.68087Vafeiadis, Viktor; Balabonski, Thibaut; Chakraborty, Soham; Morisset, Robin; Zappa Nardelli, Francesco 3 2015 Owicki-Gries reasoning for weak memory models. Zbl 1440.68046Lahav, Ori; Vafeiadis, Viktor 3 2015 Relaxed-memory concurrency and verified compilation. Zbl 1284.68152Ŝevčik, Jaroslav; Vafeiadis, Viktor; Zappa Nardelli, Francesco; Jagannathan, Suresh; Sewell, Peter 3 2011 Structuring the verification of heap-manipulating programs. Zbl 1312.68065Nanevski, Aleksandar; Vafeiadis, Viktor; Berdine, Josh 3 2010 Shape-value abstraction for verifying linearizability. Zbl 1206.68103Vafeiadis, Viktor 3 2009 A promising semantics for relaxed-memory concurrency. Zbl 1380.68103Kang, Jeehoon; Hur, Chung-Kil; Lahav, Ori; Vafeiadis, Viktor; Dreyer, Derek 2 2017 Taming release-acquire consistency. Zbl 1347.68086Lahav, Ori; Giannarakis, Nick; Vafeiadis, Viktor 2 2016 Modular verification of concurrency-aware linearizability. Zbl 1394.68229Hemed, Nir; Rinetzky, Noam; Vafeiadis, Viktor 2 2015 Mtac: a monad for typed tactic programming in Coq. Zbl 1420.68189Ziliani, Beta; Dreyer, Derek; Krishnaswami, Neelakantan R.; Nanevski, Aleksandar; Vafeiadis, Viktor 2 2015 Acute: high-level programming language design for distributed computation. Zbl 1302.68071Sewell, Peter; Leifer, James J.; Wansbrough, Keith; Nardelli, Francesco Zappa; Allen-Williams, Mair; Habouzit, Pierre; Vafeiadis, Viktor 2 2005 Lightweight verification of separate compilation. Zbl 1347.68085Kang, Jeehoon; Kim, Yoonseung; Hur, Chung-Kil; Dreyer, Derek; Vafeiadis, Viktor 1 2016 A program logic for C11 memory fences. Zbl 06559869Doko, Marko; Vafeiadis, Viktor 1 2016 Adjustable references. Zbl 1317.68234Vafeiadis, Viktor 1 2013 A promising semantics for relaxed-memory concurrency. Zbl 1380.68103Kang, Jeehoon; Hur, Chung-Kil; Lahav, Ori; Vafeiadis, Viktor; Dreyer, Derek 2 2017 Taming release-acquire consistency. Zbl 1347.68086Lahav, Ori; Giannarakis, Nick; Vafeiadis, Viktor 2 2016 Lightweight verification of separate compilation. Zbl 1347.68085Kang, Jeehoon; Kim, Yoonseung; Hur, Chung-Kil; Dreyer, Derek; Vafeiadis, Viktor 1 2016 A program logic for C11 memory fences. Zbl 06559869Doko, Marko; Vafeiadis, Viktor 1 2016 Pilsner: a compositionally verified compiler for a higher-order imperative language. Zbl 1360.68350Neis, Georg; Hur, Chung-Kil; Kaiser, Jan-Oliver; McLaughlin, Craig; Dreyer, Derek; Vafeiadis, Viktor 3 2015 Common compiler optimisations are invalid in the C11 memory model and what we can do about it. Zbl 1345.68087Vafeiadis, Viktor; Balabonski, Thibaut; Chakraborty, Soham; Morisset, Robin; Zappa Nardelli, Francesco 3 2015 Owicki-Gries reasoning for weak memory models. Zbl 1440.68046Lahav, Ori; Vafeiadis, Viktor 3 2015 Modular verification of concurrency-aware linearizability. Zbl 1394.68229Hemed, Nir; Rinetzky, Noam; Vafeiadis, Viktor 2 2015 Mtac: a monad for typed tactic programming in Coq. Zbl 1420.68189Ziliani, Beta; Dreyer, Derek; Krishnaswami, Neelakantan R.; Nanevski, Aleksandar; Vafeiadis, Viktor 2 2015 The power of parameterization in coinductive proof. Zbl 1301.68220Hur, Chung-Kil; Neis, Georg; Dreyer, Derek; Vafeiadis, Viktor 15 2013 CompCertTSO: a verified compiler for relaxed-memory concurrency. Zbl 1281.68072Ševčík, Jaroslav; Vafeiadis, Viktor; Zappa Nardelli, Francesco; Jagannathan, Suresh; Sewell, Peter 8 2013 Aspect-oriented linearizability proofs. Zbl 1390.68213Henzinger, Thomas A.; Sezgin, Ali; Vafeiadis, Viktor 7 2013 Mtac: a monad for typed tactic programming in Coq. Zbl 1323.68236Ziliani, Beta; Dreyer, Derek; Krishnaswami, Neelakantan R.; Nanevski, Aleksandar; Vafeiadis, Viktor 5 2013 Adjustable references. Zbl 1317.68234Vafeiadis, Viktor 1 2013 The marriage of bisimulations and Kripke logical relations. Zbl 1321.68198Hur, Chung-Kil; Dreyer, Derek; Neis, Georg; Vafeiadis, Viktor 6 2012 Concurrent separation logic and operational semantics. Zbl 1342.68104Vafeiadis, Viktor 5 2011 Relaxed-memory concurrency and verified compilation. Zbl 1284.68152Ŝevčik, Jaroslav; Vafeiadis, Viktor; Zappa Nardelli, Francesco; Jagannathan, Suresh; Sewell, Peter 3 2011 Structuring the verification of heap-manipulating programs. Zbl 1312.68065Nanevski, Aleksandar; Vafeiadis, Viktor; Berdine, Josh 3 2010 Proving that non-blocking algorithms don’t block. Zbl 1315.68093Gotsman, Alexey; Cook, Byron; Parkinson, Matthew; Vafeiadis, Viktor 11 2009 Deny-guarantee reasoning. Zbl 1234.68075Dodds, Mike; Feng, Xinyu; Parkinson, Matthew; Vafeiadis, Viktor 9 2009 Shape-value abstraction for verifying linearizability. Zbl 1206.68103Vafeiadis, Viktor 3 2009 A marriage of rely/guarantee and separation logic. Zbl 1151.68556Vafeiadis, Viktor; Parkinson, Matthew 31 2007 Modular safety checking for fine-grained concurrency. Zbl 1211.68082Calcagno, Cristiano; Parkinson, Matthew; Vafeiadis, Viktor 13 2007 Acute: high-level programming language design for distributed computation. Zbl 1125.68023Sewell, Peter; Leifer, James J.; Wansbrough, Keith; Nardelli, Francesco Zappa; Allen-Williams, Mair; Habouzit, Pierre; Vafeiadis, Viktor 7 2007 Acute: high-level programming language design for distributed computation. Zbl 1302.68071Sewell, Peter; Leifer, James J.; Wansbrough, Keith; Nardelli, Francesco Zappa; Allen-Williams, Mair; Habouzit, Pierre; Vafeiadis, Viktor 2 2005 all cited Publications top 5 cited Publications all top 5 Cited by 249 Authors 5 Bouajjani, Ahmed 5 da Rocha Pinto, Pedro 5 Enea, Constantin 5 Schellhorn, Gerhard 4 Birkedal, Lars 4 Dinsdale-Young, Thomas 4 Dreyer, Derek R. 4 Feng, Xinyu 4 Gardner, Philippa Anne 4 Jones, Cliff B. 4 Vafeiadis, Viktor 3 Hou, Zhe 3 Lenglet, Sergueï 3 Owens, Scott 3 Sewell, Peter 3 Tiu, Alwen Fernanto 3 Wehrheim, Heike 3 Zhang, Yu 2 Abel, Andreas M. 2 Amjad, Hasan 2 Bengtson, Jesper 2 Bornat, Richard 2 Brotherston, James 2 Cho, Kenta 2 Ciobâcă, Ştefan 2 Demri, Stéphane P. 2 Derrick, John 2 Deters, Morgan 2 Emmi, Michael 2 Fu, Ming 2 Gotsman, Alexey 2 Hamza, Jad 2 Hasuo, Ichiro 2 Hayes, Ian J. 2 Jung, Ralf 2 Kataoka, Toshiki 2 Krebbers, Robbert 2 Lochbihler, Andreas 2 Malecha, Gregory 2 Möller, Bernhard 2 Nanevski, Aleksandar 2 Pous, Damien 2 Reif, Wolfgang 2 Rossberg, Andreas 2 Roşu, Grigore 2 Rusu, Vlad 2 Sánchez, Alejandro D. 2 Sánchez, César 2 Schäfer, Steven 2 Schmitt, Alan 2 Shao, Zhong 2 Sozeau, Matthieu 2 Stefani, Jean-Bernard 2 Tofan, Bogdan 2 Travkin, Oleg 2 Zappa Nardelli, Francesco 2 Ziliani, Beta 2 Zucca, Elena 1 Abe, Tatsuya 1 Albert, Elvira 1 Allais, Guillaume 1 Anand, Abhishek 1 Ancona, Davide 1 Andersen, Kristoffer Just 1 Bach Poulsen, Casper 1 Bäumler, Simon 1 Beckert, Bernhard 1 Beillahi, Sidi Mohamed 1 Besson, Frédéric 1 Bierman, Gavin M. 1 Biernacki, Dariusz 1 Bizjak, Aleš 1 Blanchette, Jasmin Christian 1 Blazy, Sandrine 1 Böhm, Peter 1 Boulier, Simon 1 Bouzy, Aymeric 1 Brady, Edwin C. 1 Buisse, Alexandre 1 Cachera, David 1 Cai, Hongxu 1 Chatterjee, Satrajit 1 Chifflier, Pierre 1 Christensen, Michael 1 Clarke, Dave 1 Cohen, Cyril 1 Colvin, Robert J. 1 Crespo, Juan Manuel 1 Dagnino, Francesco 1 Dan, Andrei Marian 1 Dang, Han-Hing 1 Demange, Delphine 1 Deng, Yuxin 1 Devesas Campos, Marco 1 Dezani-Ciancaglini, Mariangiola 1 Dodds, Mike 1 Doherty, Simon 1 Doko, Marko 1 Dong, Yuan 1 Dongol, Brijesh ...and 149 more Authors all top 5 Cited in 24 Serials 11 Formal Aspects of Computing 10 Journal of Automated Reasoning 9 Journal of Functional Programming 8 Journal of Logical and Algebraic Methods in Programming 3 Theoretical Computer Science 3 Logical Methods in Computer Science 2 Information and Computation 2 Annals of Mathematics and Artificial Intelligence 2 Computer Languages, Systems & Structures 2 ACM Transactions on Computational Logic 2 Frontiers of Computer Science 1 Acta Informatica 1 Journal of Philosophical Logic 1 Science of Computer Programming 1 New Generation Computing 1 MSCS. Mathematical Structures in Computer Science 1 International Journal of Foundations of Computer Science 1 Journal of Applied Non-Classical Logics 1 Journal of the ACM 1 Higher-Order and Symbolic Computation 1 The Journal of Logic and Algebraic Programming 1 Algorithms 1 RAIRO. Theoretical Informatics and Applications 1 Frontiers of Computer Science in China all top 5 Cited in 6 Fields 107 Computer science (68-XX) 36 Mathematical logic and foundations (03-XX) 2 General algebraic systems (08-XX) 2 Category theory; homological algebra (18-XX) 1 Order, lattices, ordered algebraic structures (06-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) Citations by Year