Publications

Root Causing Linearizability Violations

Published in International Conference on Computer Aided Verification (CAV), 2020

This paper presents a testing based method for finding root causes of linearizability violations of concurrent libraries.

Recommended citation: Berk Cirisci, Constantin Enea, Azadeh Farzan. "Root Causing Linearizability Violations." In Proceedings of the 31st International Conference on Computer Aided Verification (CAV), 2020.

Inductive Sequentialization of Asynchronous Programs

Published in ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2020

This paper introduces a new proof rule that can be combined with the standard abstraction and reduction techniques that can be useful for proving correctness of concurrent inductive programs.

Recommended citation: Bernhard Kragl, Constantin Enea, Thomas Henzinger, Suha Mutluergil and Shaz Qadeer. "Inductive Sequentialization of Asynchronous Programs." In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, 2020.

Replication-aware Linearizability

Published in ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2019

This paper proposes a new correctness criterion called RA-linearizability for distributed data types and shows that the well know CRDTs satisfy this new criterion in a natural way.

Recommended citation: Chao Wang, Constantin Enea, Suha Mutluergil and Gustavo Petri. "Replication-aware Linearizability." In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019.

Reasoning About TSO Programs Using Reduction and Abstraction

Published in International Conference on Computer Aided Verification (CAV), 2018

This paper aims to apply well known reduction and abstraction technique for sequentially consistent programs to the TSO weak memory model.

Recommended citation: Ahmed Bouajjani, Constantin Enea, Suha Mutluergil and Serdar Tasiran. "Reasoning About TSO Programs Using Reduction and Abstraction." In Proceedings of the 29th International Conference on Computer Aided Verification (CAV), 2018.

Proving Linearizability Using Forward Simulations

Published in International Conference on Computer Aided Verification (CAV), 2017

This paper is about how to perform refinement proofs for concurrent objects by finding forward simulation relations.

Recommended citation: Ahmed Bouajjani, Constantin Enea and Suha Mutluergil. "Proving Linearizability Using Forward Simulations." In Proceedings of the 28th International Conference on Computer Aided Verification (CAV), 2017.

A Mechanized Proof of the Chase-Lev Deque Using a Proof System

Published in International Conference on Networked Systems (NETYS), 2016

This paper is about verification of a non-trivial concurrent double ended queue using the Boogie assistant.

Recommended citation: Suha Mutluergil and Serdar Tasiran. " A Mechanized Proof of the Chase-Lev Deque Using a Proof System." Proceedings of 4th International Conference on Networked Systems (NETYS), 2016.

Verifying Programs Under Snapshot Isolation and Similar Relaxed Consistency Models

Published in ACM SIGPLAN Workshop on Transactional Computing (TRANSACT), 2014

This paper presents a source-to-source translation technique for encoding SI semantics to C programs so that they can be verified using existing static verification tools like VCC.

Recommended citation: Ismail Kuru, Burcu Kulahcioglu Ozkan, Suha Mutluergil, Serdar Tasiran, Tayfun Elmas and Ernie Cohen. "Verifying Programs Under Snapshot Isolation and Similar Relaxed Consistency Models." Proceedings of 9th ACM SIGPLAN Workshop on Transactional Computing (TRANSACT), 2014.