Suha Orhun Mutluergil

Suha Orhun Mutluergil

Instructor at Sabanci University

Sitemap

A list of all the posts and pages found on the site. For you robots out there is an XML version available for digesting as well.

Pages

Posts

Future Blog Post

less than 1 minute read

Published:

This post will show up by default. To disable scheduling of future posts, edit config.yml and set future: false.

Blog Post number 4

less than 1 minute read

Published:

This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.

Blog Post number 3

less than 1 minute read

Published:

This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.

Blog Post number 2

less than 1 minute read

Published:

This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.

Blog Post number 1

less than 1 minute read

Published:

This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.

portfolio

projects

publications

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.

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.

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.

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.

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.

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.

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.

teaching

CS 403/534: Distributed Systems

Graduate/Undergraduate Course, Sabanci University, 2021

This course focuses on the design, implementation and management of distributed computing systems. Topics include: naming, security, reliability, resource sharing , and remote execution; network protocol issues above the transport level; electronic mail; network and distributed file systems, and databases; handling transactions and coordination of multiple machines.

CS 307: Operating Systems

Undergraduate Course, Sabanci University, 2021

This course covers fundamental aspects of operating systems: management of resources such as CPU, memory space and peripheral devices. Topics include concurrent processes, mutual exclusion, process communication, cooperation, deadlocks, semaphores, scheduling, and and protection. The course will also highlight important aspects of operating systems such as UNIX, Windows, etc.