Workshop on Software Reliability and Formal Methods.
Monday, May 31, 2010 at ENG 208, Koc University

Software verification and software reliability are very important!
Listen to how software verification and race conditions were relevant in the Toyota brake problem. (Fast forward to 4:40)

New!
Microsoft Research PhD Scholarship available for one qualified PhD student starting 2009-2010 academic year.
Here is the flyer for the Koc University PhD position for this project.
Topic of funded project: Software Verification and Reliability for Multi-Core Processors

This project proposal was one of the 18 recipients of the 2010 Microsoft Research PhD Scholarship.
Turkey was one of three countries that had a winning proposal for the first time this year since the program started in 2005.
Prospective PhD students, click here for more information

New! Our paper "Goldilocks: A Race and Transaction-Aware Java Runtime" (Elmas, Qadeer and Tasiran)
was selected to appear in the Research Highlights section of the Communications of the ACM.  The invitation e-mail says:

"CACM has been completely revamped along the lines of Science or Nature, with top-quality research content as a major component.[...]
Research Highlights, is devoted to the most important research results published in CS in recent years.[...]
With a readership of 95,000 from over 100 countries, we believe publication in the CACM Research Highlight section is
becoming regarded as a significant honor."

Research Group Sites:

Software Verification Research: http://theorem.ku.edu.tr
Center for Advanced Design Technologies: http://designtech.ku.edu.tr

Conference organization:

VSTTE 2010, RV 2010, PADTAD 2010, ICCD 2010
TRANSACT 2009, PADTAD 2009, CAV 2009, ICCD 2009, ICTAC 2009
ICCD 2008, RV 2008, PADTAD 2008, ICTAC 2008, HVC 2008, YKGS 2008, SAVBCS 2008

A few recent publications:

Simplifying Linearizability Proofs with Reduction and Abstraction. (Technical report version can be found here.)
Tayfun Elmas, Shaz Qadeer, Ali Sezgin, Omer Subasi, Serdar Tasiran.
To appear in ETAPS 2010 Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS).
Paphos, Cyprus. March 20-28, 2010.

Shaz Qadeer, Ali Sezgin, Serdar Tasiran
Back and Forth: Prophecy Variables for Static Verification of Concurrent Programs
Microsoft Research Technical Report, MSR TR-2009-142. October 13, 2009.

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

Tayfun Elmas, Shaz Qadeer, Serdar Tasiran
A Calculus of Atomic Actions
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '09)
Full version: Microsoft Research Technical Report, MSR TR-2008-99