×

zbMATH — the first resource for mathematics

Vafeiadis, Viktor

Compute Distance To:
Author ID: vafeiadis.viktor Recent zbMATH articles by "Vafeiadis, Viktor"
Published as: Vafeiadis, Viktor
Documents Indexed: 33 Publications since 2005

Publications by Year

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.68556
Vafeiadis, Viktor; Parkinson, Matthew
31
2007
The power of parameterization in coinductive proof. Zbl 1301.68220
Hur, Chung-Kil; Neis, Georg; Dreyer, Derek; Vafeiadis, Viktor
15
2013
Modular safety checking for fine-grained concurrency. Zbl 1211.68082
Calcagno, Cristiano; Parkinson, Matthew; Vafeiadis, Viktor
13
2007
Proving that non-blocking algorithms don’t block. Zbl 1315.68093
Gotsman, Alexey; Cook, Byron; Parkinson, Matthew; Vafeiadis, Viktor
11
2009
Deny-guarantee reasoning. Zbl 1234.68075
Dodds, 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.68213
Henzinger, Thomas A.; Sezgin, Ali; Vafeiadis, Viktor
7
2013
Acute: high-level programming language design for distributed computation. Zbl 1125.68023
Sewell, 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.68198
Hur, Chung-Kil; Dreyer, Derek; Neis, Georg; Vafeiadis, Viktor
6
2012
Mtac: a monad for typed tactic programming in Coq. Zbl 1323.68236
Ziliani, Beta; Dreyer, Derek; Krishnaswami, Neelakantan R.; Nanevski, Aleksandar; Vafeiadis, Viktor
5
2013
Concurrent separation logic and operational semantics. Zbl 1342.68104
Vafeiadis, Viktor
5
2011
Pilsner: a compositionally verified compiler for a higher-order imperative language. Zbl 1360.68350
Neis, 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.68087
Vafeiadis, Viktor; Balabonski, Thibaut; Chakraborty, Soham; Morisset, Robin; Zappa Nardelli, Francesco
3
2015
Owicki-Gries reasoning for weak memory models. Zbl 1440.68046
Lahav, 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.68065
Nanevski, Aleksandar; Vafeiadis, Viktor; Berdine, Josh
3
2010
Shape-value abstraction for verifying linearizability. Zbl 1206.68103
Vafeiadis, Viktor
3
2009
A promising semantics for relaxed-memory concurrency. Zbl 1380.68103
Kang, Jeehoon; Hur, Chung-Kil; Lahav, Ori; Vafeiadis, Viktor; Dreyer, Derek
2
2017
Taming release-acquire consistency. Zbl 1347.68086
Lahav, Ori; Giannarakis, Nick; Vafeiadis, Viktor
2
2016
Modular verification of concurrency-aware linearizability. Zbl 1394.68229
Hemed, Nir; Rinetzky, Noam; Vafeiadis, Viktor
2
2015
Mtac: a monad for typed tactic programming in Coq. Zbl 1420.68189
Ziliani, Beta; Dreyer, Derek; Krishnaswami, Neelakantan R.; Nanevski, Aleksandar; Vafeiadis, Viktor
2
2015
Acute: high-level programming language design for distributed computation. Zbl 1302.68071
Sewell, 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.68085
Kang, Jeehoon; Kim, Yoonseung; Hur, Chung-Kil; Dreyer, Derek; Vafeiadis, Viktor
1
2016
A program logic for C11 memory fences. Zbl 06559869
Doko, Marko; Vafeiadis, Viktor
1
2016
Adjustable references. Zbl 1317.68234
Vafeiadis, Viktor
1
2013
A promising semantics for relaxed-memory concurrency. Zbl 1380.68103
Kang, Jeehoon; Hur, Chung-Kil; Lahav, Ori; Vafeiadis, Viktor; Dreyer, Derek
2
2017
Taming release-acquire consistency. Zbl 1347.68086
Lahav, Ori; Giannarakis, Nick; Vafeiadis, Viktor
2
2016
Lightweight verification of separate compilation. Zbl 1347.68085
Kang, Jeehoon; Kim, Yoonseung; Hur, Chung-Kil; Dreyer, Derek; Vafeiadis, Viktor
1
2016
A program logic for C11 memory fences. Zbl 06559869
Doko, Marko; Vafeiadis, Viktor
1
2016
Pilsner: a compositionally verified compiler for a higher-order imperative language. Zbl 1360.68350
Neis, 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.68087
Vafeiadis, Viktor; Balabonski, Thibaut; Chakraborty, Soham; Morisset, Robin; Zappa Nardelli, Francesco
3
2015
Owicki-Gries reasoning for weak memory models. Zbl 1440.68046
Lahav, Ori; Vafeiadis, Viktor
3
2015
Modular verification of concurrency-aware linearizability. Zbl 1394.68229
Hemed, Nir; Rinetzky, Noam; Vafeiadis, Viktor
2
2015
Mtac: a monad for typed tactic programming in Coq. Zbl 1420.68189
Ziliani, Beta; Dreyer, Derek; Krishnaswami, Neelakantan R.; Nanevski, Aleksandar; Vafeiadis, Viktor
2
2015
The power of parameterization in coinductive proof. Zbl 1301.68220
Hur, 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.68213
Henzinger, Thomas A.; Sezgin, Ali; Vafeiadis, Viktor
7
2013
Mtac: a monad for typed tactic programming in Coq. Zbl 1323.68236
Ziliani, Beta; Dreyer, Derek; Krishnaswami, Neelakantan R.; Nanevski, Aleksandar; Vafeiadis, Viktor
5
2013
Adjustable references. Zbl 1317.68234
Vafeiadis, Viktor
1
2013
The marriage of bisimulations and Kripke logical relations. Zbl 1321.68198
Hur, Chung-Kil; Dreyer, Derek; Neis, Georg; Vafeiadis, Viktor
6
2012
Concurrent separation logic and operational semantics. Zbl 1342.68104
Vafeiadis, 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.68065
Nanevski, Aleksandar; Vafeiadis, Viktor; Berdine, Josh
3
2010
Proving that non-blocking algorithms don’t block. Zbl 1315.68093
Gotsman, Alexey; Cook, Byron; Parkinson, Matthew; Vafeiadis, Viktor
11
2009
Deny-guarantee reasoning. Zbl 1234.68075
Dodds, Mike; Feng, Xinyu; Parkinson, Matthew; Vafeiadis, Viktor
9
2009
Shape-value abstraction for verifying linearizability. Zbl 1206.68103
Vafeiadis, Viktor
3
2009
A marriage of rely/guarantee and separation logic. Zbl 1151.68556
Vafeiadis, Viktor; Parkinson, Matthew
31
2007
Modular safety checking for fine-grained concurrency. Zbl 1211.68082
Calcagno, Cristiano; Parkinson, Matthew; Vafeiadis, Viktor
13
2007
Acute: high-level programming language design for distributed computation. Zbl 1125.68023
Sewell, 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.68071
Sewell, Peter; Leifer, James J.; Wansbrough, Keith; Nardelli, Francesco Zappa; Allen-Williams, Mair; Habouzit, Pierre; Vafeiadis, Viktor
2
2005
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

Citations by Year