Short Academic History:
- PhD (Computer Science) from University of Utah, 2004.
Supervisor: Dr. Ganesh Gopalakrishnan.
Thesis Title: Formalization and Verification of Shared Memory.
- MS (Electrical and Electronics Engineering) from Middle East Technical University, 1994.
Supervisor: Dr. Kemal Inan.
Thesis Title: A Comparison of Process Specifications Using the Languages
SDL and ERPAL.
- BS (Electrical and Electronics Engineering) from Middle East Technical University, 1991.
Keywords for Research Interests:
- Concurrency, multi-core computing, linearizability, concurrent data structure implementations, quantitative relaxation, verification
- Genetic regulatory circuits, computational models for gene transcription
Publications (see CV for the complete list):
- Aspect Oriented Linearizability Proofs. Soham Chakraborty, Thomas A. Henzinger, Ali Sezgin, Viktor Vafeiadis. To appear in Logical Methods in Computer Science.
- Local Linearizability. Andreas Haas, Thomas A. Henzinger, Andreas Holzer, Christoph M. Kirsch, Michael Lippautz, Hannes Payer, Ali Sezgin, Ana Sokolova, Helmut Veith. Under review.
- Replacing Competition with Cooperation to Achieve Scalable Lock-Free FIFO Queues. Thomas A. Henzinger, Hannes Payer, Ali Sezgin. IST Technical Report, IST-124-v1+1.
- How Free is Your Linearizable Data Structure?. Thomas A. Henzinger and Ali Sezgin. IST Technical Report, IST-123-v1+2.
- Aspect-Oriented Linearizability Proofs. Thomas A. Henzinger, Ali Sezgin and Viktor Vafeiadis. CONCUR 2013.
- Distributed Queues in Shared Memory - Multicore Performance and Scalability through Quantitative Relaxation. Andreas Haas, Thomas A. Henzinger, Christoph M. Kirsch, Michael Lippautz, Hannes Payer, Ali Sezgin and Ana Sokolova (Invited Paper). Computing Frontiers, CF2013.
- Quantitative Relaxation of Concurrent Data Structures. Thomas A. Henzinger, Christoph M. Kirsch, Hannes Payer, Ali Sezgin and Ana Sokolova. POPL 2013.
- Delayed Continuous Time Markov Chains for Genetic Regulatory Circuits. Calin Guet, Ashutosh Gupta, Thomas A. Henzinger, Maria Mateescu and Ali Sezgin. CAV 2012.
- Run-Time Verification of Optimistic Concurrency. Ali Sezgin, Serdar Tasiran, Kivanc Muslu and Shaz Qadeer. RV 2010.
- Tressa: Claiming the Future. Ali Sezgin, Serdar Tasiran and Shaz Qadeer. VSTTE 2010.
- Simplifying Linearizability Proofs with Reduction and Abstraction. Tayfun Elmas, Shaz Qadeer, Ali Sezgin, Omer Subasi and Serdar Tasiran. TACAS 2010.
- Verifying Optimistic Concurrency: Prophecy Variables and Backward Reasoning. Serdar Tasiran, Ali Sezgin and Shaz Qadeer. Design and Validation of Concurrent Systems, Dagstuhl Seminar Proceedings, 2010.
Also, appeared as a technical report: Back and Forth: Prophecy Variables for Static
Verification of Concurrent Programs. Shaz Qadeer, Ali Sezgin and Serdar Tasiran. Microsoft Research Technical Report, MSR-TR-2009-142, 2009.
- An Annotation Assistant for
Interactive Debugging of Programs with Common Synchronization Idioms.
Tayfun Elmas, Ali Sezgin, Serdar Tasiran and Shaz Qadeer. PADTAD 2009.
- On the Definition of
Sequential Consistency. Ali Sezgin and Ganesh Gopalakrishnan.
Information Processing Letters, 96(6): 193-196, 2005.
- On the Decidability of
Shared Memory Consistency Verification. Ali Sezgin and Ganesh
Gopalakrishnan. MEMOCODE 2005: 199-208.
- Emptiness of Linear Weak
Alternating Automata. Stephan Merz and
Ali Sezgin. Technical Report A03-R-503, Loria, 2003.