Last updated

Publications


Copyright notice. This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

Refereed Conference Papers


[PDF]
CONCURRIT: Testing Concurrent Programs with Programmable State-Space Exploration 
Jacob Burnim, Tayfun Elmas, George Necula, Koushik Sen.
In the 4nd USENIX Workshop on Hot Topics in Parallelism (HotPar), 2012. (Position paper)

[PDF]
On Justifying and Verifying Relaxed Detection of Conflicts in Concurrent Programs
Omer Subasi, Tayfun Elmas, Adrian Cristal, Tim Harris, Serdar Tasiran, Ruben Titos-Gil, Osman Unsal.
Workshop on Determinism and Correctness in Parallel Programming (WoDet). (Position paper)
London, England, UK, March 4, 2012.

[PDF
KUDA: GPU Accelerated Split Race Checker
Can Bekar, Tayfun Elmas, Semih Okur, Serdar Tasiran.
Workshop on Determinism and Correctness in Parallel Programming (WoDet). (Position paper)
London, England, UK, March 4, 2012.


NDetermin: Inferring Nondeterministic Sequential Specifications for Parallelism Correctness.

Jacob Burnim, Tayfun Elmas

George Necula, Koushik Sen.

ACM SIGPLAN 2012 Symposium on Principles and Practice of Parallel Programming (PPoPP). (Poster paper)
New Orleans, LA, USA, February 25-29, 2012.

[PDF]

NDSeq: Runtime Checking for Nondeterministic Sequential Specifications of Parallel Correctness.


Jacob Burnim, Tayfun Elmas

George Necula, Koushik Sen.

ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation (PLDI).
San Jose, CA, USA, June 4-8, 2011.

[PDF]
Goldilocks: A Race-Aware Java Runtime.
Tayfun Elmas, Serdar Tasiran, Shaz Qadeer.
In the November 2010 Communications of the ACM - Research Highlights (Nominated in January 2009).

[PDF]

QED: A Proof System based on Reduction and Abstraction for the Static Verification of Concurrent Software

Tayfun Elmas.
In ACM Student Research Competition (SRC). Hosted by ACM/IEEE 2010 Conference on Software Engineering (ICSE).
Cape Town, South Africa, May 5-7, 2010. 

Simplifying Linearizability Proofs with Reduction and Abstraction.
Tayfun Elmas, Shaz Qadeer, Ali Sezgin, Omer Subasi, Serdar Tasiran.
In ETAPS 2010 Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS).
Paphos, Cyprus. March 20-28, 2010.

[PDF] [BibTex] [Slides]
An Annotation Assistant for Interactive Debugging of Programs with Common Synchronization Idioms.
Tayfun Elmas, Ali Sezgin, Serdar Tasiran, Shaz Qadeer.
In ACM 2009 Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging (PADTAD).
Chicago, Illionis, USA, July 19-20, 2009. 

[PDF] [Technical report] [BibTex[Slides[ACM SRC paper]
A Calculus of Atomic Actions. (describes the QED proof system)
Tayfun Elmas, Shaz Qadeer, Serdar Tasiran.
In ACM SIGPLAN-SIGACT 2009 Symposium on Principles of Programming Languages (POPL).
Savannah, Georgia, USA, January 21-23, 2009. 

A Causality-Based Runtime Check for (Rollback) Atomicity.
Serdar Tasiran, Tayfun Elmas.
In Runtime Verification Workshop (RV).
Vancouver, Canada. March 13, 2007.
Lecture Notes in Computer Science, Springer. 

[PDF] [BibTex[Slides]
Goldilocks: A Race and Transaction-Aware Java Runtime.
Tayfun Elmas, Serdar Tasiran, Shaz Qadeer.
ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation (PLDI).
San Diego, CA, USA, June 10-13, 2007.
Selected for publication in SIGPLAN CACM Research Highlights (Nominated in January 2009).
Goldilocks: Efficiently computing the happens-before relation using locksets.
Tayfun Elmas, Shaz Qadeer, Serdar Tasiran.
Proceedings of the Workshop on Formal Approaches to Testing and Runtime Verification (FATES/RV). 
Seattle, WA, August 15-16 2006.
Lecture Notes in Computer Science, Springer, LNCS 4262. 

[PDF]
A Classification of Concurrency Bugs in Java Benchmarks by Developer Intent.
M. Erkan Keremoglu, Serdar Tasiran, Tayfun Elmas.
In ACM 2006 Workshop Parallel and Distributed Systems: Testing and Debugging (PADTAD).
Portland, Maine, USA. July 17, 2006. 
A Novel Test Coverage Metric for Concurrently-Accessed Software Components.
Serdar Tasiran, Tayfun Elmas, Guven Bolukbasi, M. Erkan Keremoglu.
Fifth International Workshop on Formal Approaches to Testing of Software (FATES). 
University of Edinburgh, Scotland, UK, July 11, 2005. 
Lecture Notes in Computer Science, Springer (2006), vol. 3997, pp. 62-71. 

[PDF]  [BibTex[Slides]
VyrdMC: Driving Runtime Refinement Checking with Model Checkers.
Tayfun Elmas, Serdar Tasiran.
Fifth Workshop on Runtime Verification (RV).
January 2006, pp. 41-56. The University of Edinburgh, Scotland, UK. July 12, 2005.
Electronic Notes in Theoretical Computer Science, Volume 144, Number 1. 

[PDF] [BibTex[Slides[Poster]
VYRD: VerifYing Concurrent Programs by Runtime Refinement-Violation Detection.
Tayfun Elmas, Serdar Tasiran, Shaz Qadeer.
ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation (PLDI). 
Chicago, Illinois, USA, June 12-15, 2005. 
ACM SIGPLAN Notices Vol. 40 No. 6. pp 27-37.

[PDF] [Poster]
Retrieval and Path Diversity Techniques on Content-Addressable Networks for Multiple Description Coded Video Transport.
Tayfun Elmas, Reha Civanlar.
In the 14th International Packet Video Workshop (PV2004).
December 13-14, 2004 at University of California, Irvine. 

[PDF]
Distributed Document Sharing with Text Classification over Content-Addressable Networks.
Tayfun Elmas, Oznur Ozkasap.
In AWCC 2004, Advanced Workshop on Content Computing, China.
Lecture Notes in Computer Science, Springer Verlag. 2004. 

[PDF]
A Statistical Analysis System with Java Web Services.
Yasemin Topaloglu, Hulya Atli, Tayfun Elmas, Arda Goknil.
International Congress on Information Technology in Agriculture, Food and Environment (ITAFE).
Ege University, Izmir, Turkey. 2003.
Proc. of ITAFE'03 pages 477-482.

National Conferences

[Poster]
QED: A Proof System for the Static Verification of Concurrent Software.
Tayfun Elmas and Ömer Subaşı.
In the 1st Computer Science Student Workshop (CSW).
Koc University, Istanbul, Turkey, February 21, 2010.

Paralel Yazilim Gelistirme Surecinde Yaris Durumu Denetimi. (in Turkish)
Tayfun Elmas, Serdar Tasiran.
In the 1st National Symposium on Software Quality and Software Development Tools.
Istanbul Kultur University, Hava Harp Okulu, Istanbul, Turkey, October 9-10, 2008. 

[PDF[Slides]
Kosutzamanli Yazilim Bilesenleri icin Bir Otomatik Dogrulama CerCevesi: VyrdMC. (in Turkish)
Tayfun Elmas, Serdar Tasiran.
In the 2nd National Symposium on Software Engineering.
METU, Ankara, Turkey, September 22-24 2005. 

[PDF]
Tasarim Desenleri ve Java Web Servisleri ile Cok Katmanli Bir Sistem Tasarimi. (in Turkish)
Arda Goknil, Tayfun Elmas, Yasemin Topaloglu.
In the 1st National Symposium on Software Engineering.
Ege University, Izmir, Turkey. 2003. 

Technical Reports

[PDF]

NDetermin: Inferring Nondeterministic Sequential Specifications for Parallelism Correctness.

Jacob Burnim, Tayfun Elmas

George Necula, Koushik Sen.

EECS Department, University of California, Berkeley, Tech. Rep. 
UCB/EECS-2011-143
, December 2011.

[PDF]
Rethinking Runtime Verification on Hundreds of Cores: Challenges and Opportunities.
Tayfun Elmas, Semih Okur, and Serdar Tasiran
EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2011-74, June 2011.


A Calculus of Atomic Actions.
Tayfun Elmas, Shaz Qadeer, Serdar Tasiran.
Technical Report MSR-TR-2008-99.
Microsoft Research. July 2008. 

[PDF] [BibTex]
Goldilocks: Efficiently computing the happens-before relation using locksets.
Tayfun Elmas, Shaz Qadeer, Serdar Tasiran.
Technical Report MSR-TR-2006-163.
Microsoft Research. September 2006. 

[PDF] [BibTex]
Precise Race Detection and Efficient Model Checking Using Locksets.
Tayfun Elmas, Shaz Qadeer, Serdar Tasiran.
Technical Report MSR-TR-2005-118.
Microsoft Research. September 2005. 

[PDF[Slides]
Runtime Checking of Refinement for Concurrent Software Components.
Tayfun Elmas.
The thesis for Master of Science in Electrical and Computer Engineering.
Advised by Dr. Serdar Tasiran.
Koc University, Istanbul. December 26, 2005.

Vyrd+: A Toolbox for Runtime Verification of Concurrent Software
Selcuk Atli, Nihal Dindar, Tayfun Elmas, Serdar Tasiran
Technical Report, Koc University.

Tasarim Desenleri ve Java Web Servisleri ile Cok Katmanli Bir Sistem Tasarimi. (in Turkish)
Arda Goknil, Tayfun Elmas.
The senior project technical report.
Advised by Dr. Yasemin Topaloglu.
Ege University, Izmir, Turkey. 2003.