Number of items: 37.
Conference or Workshop Item (A Paper)
Kang, Jeehoon and Hur, Chung-Kil and Lahav, Ori and Vafeiadis, Viktor and Dreyer, Derek
(2017)
A promising semantics for relaxed-memory concurrency.
Chakraborty, Soham and Vafeiadis, Viktor
(2017)
Formalizing the concurrency semantics of an LLVM fragment.
Vafeiadis, Viktor
(2017)
Program Verification Under Weak Memory Consistency Using Separation Logic.
Podkopaev, Anton and Lahav, Ori and Vafeiadis, Viktor
(2017)
Promising Compilation to ARMv8 POP.
Lahav, Ori and Vafeiadis, Viktor and Kang, Jeehoon and Hur, Chung-Kil and Dreyer, Derek
(2017)
Repairing sequential consistency in C/C++11.
Lahav, Ori and Vafeiadis, Viktor and Kang, Jeehoon and Hur, Chung-Kil and Dreyer, Derek
(2017)
Repairing sequential consistency in C/C++11.
Kaiser, Jan-Oliver and Dang, Hoang-Hai and Dreyer, Derek and Lahav, Ori and Vafeiadis, Viktor
(2017)
Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris.
Doko, Marko and Vafeiadis, Viktor
(2017)
Tackling Real-Life Relaxed Concurrency with FSL++.
Kang, Jeehoon and Kim, Yoonseung and Hur, Chung-Kil and Dreyer, Derek and Vafeiadis, Viktor
(2016)
Lightweight verification of separate compilation.
Lahav, Ori and Giannarakis, Nick and Vafeiadis, Viktor
(2016)
Taming release-acquire consistency.
Lahav, Ori and Vafeiadis, Viktor
(2016)
Explaining Relaxed Memory Models with Program Transformations.
Doko, Marko and Vafeiadis, Viktor
(2016)
A Program Logic for C11 Memory Fences.
He, Mengda and Vafeiadis, Viktor and Qin, Shengchao and Ferreira, João F.
(2016)
Reasoning about Fences and Relaxed Atomics.
Chakraborty, Soham and Vafeiadis, Viktor
(2016)
Validating optimizations of concurrent C/C++ programs.
Kloos, Johannes and Majumdar, Rupak and Vafeiadis, Viktor
(2015)
Asynchronous Liquid Separation Types.
Hemed, Nir and Rinetzky, Noam and Vafeiadis, Viktor
(2015)
Modular Verification of Concurrency-Aware Linearizability.
Neis, Georg and Hur, Chung-Kil and Kaiser, Jan-Oliver and McLaughlin, Craig and Dreyer, Derek and Vafeiadis, Viktor
(2015)
Pilsner: a compositionally verified compiler for a higher-order imperative language.
Gavran, Ivan and Niksic, Filip and Kanade, Aditya and Majumdar, Rupak and Vafeiadis, Viktor
(2015)
Rely/Guarantee Reasoning for Asynchronous Programs.
Tassarotti, Joseph and Dreyer, Derek and Vafeiadis, Viktor
(2015)
Verifying read-copy-update in a logic for weak memory.
Kang, Jeehoon and Hur, Chung-Kil and Mansky, William and Garbuzov, Dmitri and Zdancewic, Steve and Vafeiadis, Viktor
(2015)
A formal C memory model supporting integer-pointer casts.
Vafeiadis, Viktor and Balabonski, Thibaut and Chakraborty, Soham and Morisset, Robin and Nardelli, Francesco Zappa
(2015)
Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it.
Vafeiadis, Viktor
(2015)
Formal Reasoning about the C11 Weak Memory Model.
Lahav, Ori and Vafeiadis, Viktor
(2015)
Owicki-Gries Reasoning for Weak Memory Models.
Jia, Xiao and Li, Wei and Vafeiadis, Viktor
(2015)
Proving Lock-Freedom Easily and Automatically.
Li, Cheng and Leitão, João and Clement, Allen and Preguiça, Nuno M. and Rodrigues, Rodrigo and Vafeiadis, Viktor
(2014)
Automating the Choice of Consistency Levels in Replicated Systems.
Turon, Aaron and Vafeiadis, Viktor and Dreyer, Derek
(2014)
GPS: navigating weak memory with ghosts, protocols, and separation.
Ziliani, Beta and Dreyer, Derek and Krishnaswami, Neelakantan R. and Nanevski, Aleksandar and Vafeiadis, Viktor
(2013)
Mtac: a monad for typed tactic programming in Coq.
Zengin, Mustafa and Vafeiadis, Viktor
(2013)
A Programming Language Approach to Fault Tolerance for Fork-Join Parallelism.
Hur, Chung-Kil and Neis, Georg and Dreyer, Derek and Vafeiadis, Viktor
(2013)
The power of parameterization in coinductive proof.
Hur, Chung-Kil and Dreyer, Derek and Neis, Georg and Vafeiadis, Viktor
(2012)
The marriage of bisimulations and Kripke logical relations.
Sevcík, Jaroslav and Vafeiadis, Viktor and Nardelli, Francesco Zappa and Jagannathan, Suresh and Sewell, Peter
(2011)
Relaxed-memory concurrency and verified compilation.
Hur, Chung-Kil and Dreyer, Derek and Vafeiadis, Viktor
(2011)
Separation Logic in the Presence of Garbage Collection.
Article
Kokologiannakis, Michalis and Lahav, Ori and Sagonas, Konstantinos and Vafeiadis, Viktor
(2018)
Effective stateless model checking for C/C++ concurrency.
PACMPL, 2 (POPL).
17:1–17:32.
Balegas, Valter and Li, Cheng and Najafzadeh, Mahsa and Porto, Daniel and Clement, Allen and Duarte, Sérgio and Ferreira, Carla and Gehrke, Johannes and Leitão, João and Preguiça, Nuno M. and Rodrigues, Rodrigo and Shapiro, Marc and Vafeiadis, Viktor
(2016)
Geo-Replication: Fast If Possible, Consistent If Necessary.
IEEE Data Eng. Bull., 39 (1).
81–92.
Ziliani, Beta and Dreyer, Derek and Krishnaswami, Neelakantan R. and Nanevski, Aleksandar and Vafeiadis, Viktor
(2015)
Mtac: A monad for typed tactic programming in Coq.
J. Funct. Program., 25.
Chakraborty, Soham and Henzinger, Thomas A. and Sezgin, Ali and Vafeiadis, Viktor
(2015)
Aspect-oriented linearizability proofs.
Logical Methods in Computer Science, 11 (1).
Sevcík, Jaroslav and Vafeiadis, Viktor and Nardelli, Francesco Zappa and Jagannathan, Suresh and Sewell, Peter
(2013)
CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency.
Journal of the ACM, 60 (3).
p. 22.
This list was generated on Thu Nov 21 12:32:43 2024 CET.