Viktor Vafeiadis

Rupak Majumdar

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2024

Specifying and Verifying Persistent Libraries.

[BibT_eX]

[DOI]

Léo Stefanesco

Proceedings of the Programming Languages and Systems, 2024

2023

Kater: Automating Weak Memory Model Metatheory and Consistency Checking.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., January, 2023

The Path to Durable Linearizability.

[BibT_eX]

[DOI]

Emanuele D'Osualdo

Proc. ACM Program. Lang., January, 2023

Formal Methods for Correct Persistent Programming (Dagstuhl Seminar 23412).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2023

Reconciling Preemption Bounding with DPOR.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

BWoS: Formally Verified Block-based Work Stealing for Parallel Processing.

[BibT_eX]

[DOI]

Proceedings of the 17th USENIX Symposium on Operating Systems Design and Implementation, 2023

Optimal Bounded Partial Order Reduction.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2023

Unblocking Dynamic Partial Order Reduction.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 35th International Conference, 2023

AtoMig: Automatically Migrating Millions Lines of Code from TSO to WMM.

[BibT_eX]

[DOI]

Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, 2023

2022

Extending Intel-x86 consistency and persistency: formalising the semantics of Intel-x86 memory types and non-temporal stores.

[BibT_eX]

[DOI]

Luc Maranget

Proc. ACM Program. Lang., 2022

Model checking for a multi-execution memory model.

[BibT_eX]

[DOI]

Evgenii Moiseenko

Proc. ACM Program. Lang., 2022

Truly stateless, optimal dynamic partial order reduction.

[BibT_eX]

[DOI]

Vladimir Gladstein

Proc. ACM Program. Lang., 2022

SMT-Based Verification of Persistency Invariants of Px86 Programs.

[BibT_eX]

[DOI]

Proceedings of the Verified Software. Theories, Tools and Experiments, 2022

2021

Making weak memory models fair.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2021

PerSeVerE: persistency semantics for verification under ext4.

[BibT_eX]

[DOI]

Ilya Kaysin

Rafael Lourenco de Lima Chehab

Proc. ACM Program. Lang., 2021

VSync: Push-Button Verification and Optimization for Synchronization Primitives on Weak Memory Models (Technical Report).

[BibT_eX]

[DOI]

Jonas Oberhauser

CoRR, 2021

Verifying and Optimizing the HMCS Lock for Arm Servers.

[BibT_eX]

[DOI]

Proceedings of the Networked Systems - 9th International Conference, 2021

BAM: Efficient Model Checking for Barriers.

[BibT_eX]

[DOI]

Proceedings of the Networked Systems - 9th International Conference, 2021

Dynamic Partial Order Reductions for Spinloops.

[BibT_eX]

[DOI]

Xiaowei Ren

Proceedings of the Formal Methods in Computer Aided Design, 2021

The Decidability of Verification under PS 2.0.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2021

GenMC: A Model Checker for Weak Memory Models.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

The Challenges of Weak Persistency (Invited Talk).

[BibT_eX]

[DOI]

Rafael Lourenco de Lima Chehab

Proceedings of the 9th Conference on Algebra and Coalgebra in Computer Science, 2021

VSync: push-button verification and optimization for synchronization primitives on weak memory models.

[BibT_eX]

[DOI]

Jonas Oberhauser

Proceedings of the ASPLOS '21: 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, 2021

2020

Persistency semantics of the Intel-x86 architecture.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2020

Persistent Owicki-Gries reasoning: a program logic for reasoning about persistent programs on Intel-x86.

[BibT_eX]

[DOI]

Shankaranarayanan Krishna

Proc. ACM Program. Lang., 2020

Reconciling Event Structures with Modern Multiprocessors (Artifact).

[BibT_eX]

[DOI]

Dagstuhl Artifacts Ser., 2020

The Decidability of Verification under Promising 2.0.

[BibT_eX]

[DOI]

Parosh Aziz Abdulla

Mohamed Faouzi Atig

Adwait Godbole

CoRR, 2020

Promising 2.0: global optimizations in relaxed memory concurrency.

[BibT_eX]

[DOI]

Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2020

Reconciling Event Structures with Modern Multiprocessors.

[BibT_eX]

[DOI]

Proceedings of the 34th European Conference on Object-Oriented Programming, 2020

HMC: Model Checking for Hardware Memory Models.

[BibT_eX]

[DOI]

Proceedings of the ASPLOS '20: Architectural Support for Programming Languages and Operating Systems, 2020

2019

Weak persistency semantics from the ground up: formalising the persistency semantics of ARMv8 and transactional models.

[BibT_eX]

[DOI]

John Wickerson

Proc. ACM Program. Lang., 2019

On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2019

Bridging the gap between programming languages and hardware weak memory models.

[BibT_eX]

[DOI]

Anton Podkopaev

Proc. ACM Program. Lang., 2019

Effective lock handling in stateless model checking.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2019

Grounding thin-air reads with event structures.

[BibT_eX]

[DOI]

Soham Chakraborty

Proc. ACM Program. Lang., 2019

On the Semantics of Snapshot Isolation.

[BibT_eX]

[DOI]

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2019

Model checking for weakly consistent libraries.

[BibT_eX]

[DOI]

Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

2018

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

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2018

Effective stateless model checking for C/C++ concurrency.

[BibT_eX]

[DOI]

Konstantinos Sagonas

Proc. ACM Program. Lang., 2018

GPS+: Reasoning About Fences and Relaxed Atomics.

[BibT_eX]

[DOI]

Int. J. Parallel Program., 2018

A Separation Logic for a Promising Semantics.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2018

On Parallel Snapshot Isolation and Release/Acquire Consistency.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2018

2017

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

[BibT_eX]

[DOI]

Dagstuhl Artifacts Ser., 2017

A promising semantics for relaxed-memory concurrency.

[BibT_eX]

[DOI]

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

Repairing sequential consistency in C/C++11.

[BibT_eX]

[DOI]

Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017

Tackling Real-Life Relaxed Concurrency with FSL++.

[BibT_eX]

[DOI]

Marko Doko

Proceedings of the Programming Languages and Systems, 2017

Promising Compilation to ARMv8 POP.

[BibT_eX]

[DOI]

Anton Podkopaev

Proceedings of the 31st European Conference on Object-Oriented Programming, 2017

Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris.

[BibT_eX]

[DOI]

Proceedings of the 31st European Conference on Object-Oriented Programming, 2017

Formalizing the concurrency semantics of an LLVM fragment.

[BibT_eX]

[DOI]

Soham Chakraborty

Proceedings of the 2017 International Symposium on Code Generation and Optimization, 2017

Program Verification Under Weak Memory Consistency Using Separation Logic.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 29th International Conference, 2017

2016

Geo-Replication: Fast If Possible, Consistent If Necessary.

[BibT_eX]

[DOI]

IEEE Data Eng. Bull., 2016

A Program Logic for C11 Memory Fences.

[BibT_eX]

[DOI]

Marko Doko

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2016

Taming release-acquire consistency.

[BibT_eX]

[DOI]

Nick Giannarakis

Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Lightweight verification of separate compilation.

[BibT_eX]

[DOI]

Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Reasoning about Fences and Relaxed Atomics.

[BibT_eX]

[DOI]

Proceedings of the 24th Euromicro International Conference on Parallel, 2016

Explaining Relaxed Memory Models with Program Transformations.

[BibT_eX]

[DOI]

Proceedings of the FM 2016: Formal Methods, 2016

Validating optimizations of concurrent C/C++ programs.

[BibT_eX]

[DOI]

Soham Chakraborty

Proceedings of the 2016 International Symposium on Code Generation and Optimization, 2016

2015

Mtac: A monad for typed tactic programming in Coq.

[BibT_eX]

[DOI]

Beta Ziliani

Neelakantan R. Krishnaswami

Aleksandar Nanevski

J. Funct. Program., 2015

Verification of Evolving Graph Structures (Dagstuhl Seminar 15451).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2015

Aspect-oriented linearizability proofs.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2015

Modular Verification of Concurrency-Aware Linearizability.

[BibT_eX]

[DOI]

Nir Hemed

Noam Rinetzky

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.

[BibT_eX]

[DOI]

Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

Separation logic for weak memory models.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages Mentoring Workshop, 2015

Verifying read-copy-update in a logic for weak memory.

[BibT_eX]

[DOI]

Joseph Tassarotti

Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

A formal C memory model supporting integer-pointer casts.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, 2015

Owicki-Gries Reasoning for Weak Memory Models.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages, and Programming - 42nd International Colloquium, 2015

Asynchronous Liquid Separation Types.

[BibT_eX]

[DOI]

Johannes Kloos

Rupak Majumdar

Proceedings of the 29th European Conference on Object-Oriented Programming, 2015

Formal Reasoning about the C11 Weak Memory Model.

[BibT_eX]

[DOI]

Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015

Proving Lock-Freedom Easily and Automatically.

[BibT_eX]

[DOI]

Xiao Jia

Wei Li

Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015

Rely/Guarantee Reasoning for Asynchronous Programs.

[BibT_eX]

[DOI]

Proceedings of the 26th International Conference on Concurrency Theory, 2015

2014

Automating the Choice of Consistency Levels in Replicated Systems.

[BibT_eX]

[DOI]

Proceedings of the 2014 USENIX Annual Technical Conference, 2014

GPS: navigating weak memory with ghosts, protocols, and separation.

[BibT_eX]

[DOI]

Aaron Turon

Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, 2014

2013

CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency.

[BibT_eX]

[DOI]

Jaroslav Sevcík

Suresh Jagannathan

Peter Sewell

J. ACM, 2013

A Programming Language Approach to Fault Tolerance for Fork-Join Parallelism.

[BibT_eX]

[DOI]

Mustafa Zengin

Proceedings of the Seventh International Symposium on Theoretical Aspects of Software Engineering, 2013

The power of parameterization in coinductive proof.

[BibT_eX]

[DOI]

Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

Relaxed separation logic: a program logic for C11 concurrency.

[BibT_eX]

[DOI]

Chinmay Narayan

Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, 2013

Adjustable References.

[BibT_eX]

[DOI]

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

Aspect-Oriented Linearizability Proofs.

[BibT_eX]

[DOI]

Thomas A. Henzinger

Ali Sezgin

Proceedings of the CONCUR 2013 - Concurrency Theory - 24th International Conference, 2013

2012

The marriage of bisimulations and Kripke logical relations.

[BibT_eX]

[DOI]

Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

2011

Concurrent Separation Logic and Operational Semantics.

[BibT_eX]

[DOI]

Proceedings of the Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics, 2011

Verifying Fence Elimination Optimisations.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis - 18th International Symposium, 2011

Relaxed-memory concurrency and verified compilation.

[BibT_eX]

[DOI]

Jaroslav Sevcík

Suresh Jagannathan

Peter Sewell

Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

Separation Logic in the Presence of Garbage Collection.

[BibT_eX]

[DOI]

Chung-Kil Hur

Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, 2011

2010

RGSep Action Inference.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2010

Structuring the verification of heap-manipulating programs.

[BibT_eX]

[DOI]

Aleksandar Nanevski

Josh Berdine

Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

Concurrent Abstract Predicates.

[BibT_eX]

[DOI]

Thomas Dinsdale-Young

Proceedings of the ECOOP 2010, 2010

Automatically Proving Linearizability.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

2009

Shape-Value Abstraction for Verifying Linearizability.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2009

Proving that non-blocking algorithms don't block.

[BibT_eX]

[DOI]

Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2009

Finding heap-bounds for hardware synthesis.

[BibT_eX]

[DOI]

Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, 2009

Deny-Guarantee Reasoning.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2009

Bi-abductive Resource Invariant Synthesis.

[BibT_eX]

[DOI]

Cristiano Calcagno

Dino Distefano

Proceedings of the Programming Languages and Systems, 7th Asian Symposium, 2009

2008

Modular fine-grained concurrency verification.

[BibT_eX]

[DOI]

PhD thesis, 2008

2007

Acute: High-level programming language design for distributed computation.

[BibT_eX]

[DOI]

Peter Sewell

James J. Leifer

Keith Wansbrough

Mair Allen-Williams

Pierre Habouzit

J. Funct. Program., 2007

Modular Safety Checking for Fine-Grained Concurrency.

[BibT_eX]

[DOI]

Cristiano Calcagno

Matthew J. Parkinson

Proceedings of the Static Analysis, 14th International Symposium, 2007

A Marriage of Rely/Guarantee and Separation Logic.

[BibT_eX]

[DOI]