Viktor Vafeiadis

According to our database1, Viktor Vafeiadis authored at least 65 papers between 2005 and 2018.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

2018
Persistence semantics for weak memory: integrating epoch persistency with the TSO memory model.
PACMPL, 2018

Effective stateless model checking for C/C++ concurrency.
PACMPL, 2018

GPS $$+$$ + : Reasoning About Fences and Relaxed Atomics.
International Journal of Parallel Programming, 2018

Bridging the Gap Between Programming Languages and Hardware Weak Memory Models.
CoRR, 2018

On the Semantics of Snapshot Isolation.
CoRR, 2018

A Separation Logic for a Promising Semantics.
Proceedings of the Programming Languages and Systems, 2018

On Parallel Snapshot Isolation and Release/Acquire Consistency.
Proceedings of the Programming Languages and Systems, 2018

2017
Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris (Artifact).
DARTS, 2017

A promising semantics for relaxed-memory concurrency.
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

Repairing sequential consistency in C/C++11.
Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017

Tackling Real-Life Relaxed Concurrency with FSL++.
Proceedings of the Programming Languages and Systems, 2017

Promising Compilation to ARMv8 POP.
Proceedings of the 31st European Conference on Object-Oriented Programming, 2017

Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris.
Proceedings of the 31st European Conference on Object-Oriented Programming, 2017

Formalizing the concurrency semantics of an LLVM fragment.
Proceedings of the 2017 International Symposium on Code Generation and Optimization, 2017

Program Verification Under Weak Memory Consistency Using Separation Logic.
Proceedings of the Computer Aided Verification - 29th International Conference, 2017

2016
Geo-Replication: Fast If Possible, Consistent If Necessary.
IEEE Data Eng. Bull., 2016

A Program Logic for C11 Memory Fences.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2016

Taming release-acquire consistency.
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Lightweight verification of separate compilation.
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Reasoning about Fences and Relaxed Atomics.
Proceedings of the 24th Euromicro International Conference on Parallel, 2016

Explaining Relaxed Memory Models with Program Transformations.
Proceedings of the FM 2016: Formal Methods, 2016

Validating optimizations of concurrent C/C++ programs.
Proceedings of the 2016 International Symposium on Code Generation and Optimization, 2016

2015
Mtac: A monad for typed tactic programming in Coq.
J. Funct. Program., 2015

Verification of Evolving Graph Structures (Dagstuhl Seminar 15451).
Dagstuhl Reports, 2015

Aspect-oriented linearizability proofs.
Logical Methods in Computer Science, 2015

Modular Verification of Concurrency-Aware Linearizability.
Proceedings of the Distributed Computing - 29th International Symposium, 2015

Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it.
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

Separation logic for weak memory models.
Proceedings of the Programming Languages Mentoring Workshop, 2015

Verifying read-copy-update in a logic for weak memory.
Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

A formal C memory model supporting integer-pointer casts.
Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

Pilsner: a compositionally verified compiler for a higher-order imperative language.
Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, 2015

Owicki-Gries Reasoning for Weak Memory Models.
Proceedings of the Automata, Languages, and Programming - 42nd International Colloquium, 2015

Asynchronous Liquid Separation Types.
Proceedings of the 29th European Conference on Object-Oriented Programming, 2015

Formal Reasoning about the C11 Weak Memory Model.
Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015

Proving Lock-Freedom Easily and Automatically.
Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015

Rely/Guarantee Reasoning for Asynchronous Programs.
Proceedings of the 26th International Conference on Concurrency Theory, 2015

2014
Automating the Choice of Consistency Levels in Replicated Systems.
Proceedings of the 2014 USENIX Annual Technical Conference, 2014

GPS: navigating weak memory with ghosts, protocols, and separation.
Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, 2014

2013
CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency.
J. ACM, 2013

A Programming Language Approach to Fault Tolerance for Fork-Join Parallelism.
Proceedings of the Seventh International Symposium on Theoretical Aspects of Software Engineering, 2013

The power of parameterization in coinductive proof.
Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

Relaxed separation logic: a program logic for C11 concurrency.
Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, 2013

Adjustable References.
Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

Mtac: a monad for typed tactic programming in Coq.
Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2013

Aspect-Oriented Linearizability Proofs.
Proceedings of the CONCUR 2013 - Concurrency Theory - 24th International Conference, 2013

2012
The marriage of bisimulations and Kripke logical relations.
Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

2011
Concurrent Separation Logic and Operational Semantics.
Electr. Notes Theor. Comput. Sci., 2011

Verifying Fence Elimination Optimisations.
Proceedings of the Static Analysis - 18th International Symposium, 2011

Relaxed-memory concurrency and verified compilation.
Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

Separation Logic in the Presence of Garbage Collection.
Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, 2011

2010
RGSep Action Inference.
Proceedings of the Verification, 2010

Structuring the verification of heap-manipulating programs.
Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

Concurrent Abstract Predicates.
Proceedings of the ECOOP 2010, 2010

Automatically Proving Linearizability.
Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

2009
Shape-Value Abstraction for Verifying Linearizability.
Proceedings of the Verification, 2009

Proving that non-blocking algorithms don't block.
Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2009

Finding heap-bounds for hardware synthesis.
Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, 2009

Deny-Guarantee Reasoning.
Proceedings of the Programming Languages and Systems, 2009

Bi-abductive Resource Invariant Synthesis.
Proceedings of the Programming Languages and Systems, 7th Asian Symposium, 2009

2008
Modular fine-grained concurrency verification.
PhD thesis, 2008

2007
Acute: High-level programming language design for distributed computation.
J. Funct. Program., 2007

Modular Safety Checking for Fine-Grained Concurrency.
Proceedings of the Static Analysis, 14th International Symposium, 2007

A Marriage of Rely/Guarantee and Separation Logic.
Proceedings of the CONCUR 2007 - Concurrency Theory, 18th International Conference, 2007

2006
Proving correctness of highly-concurrent linearisable objects.
Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2006

2005
Acute: high-level programming language design for distributed computation.
Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, 2005


  Loading...