PRELIMINARY PROGRAM
Exploiting Concurrency Efficiently and Correctly -- (EC)2
CAV 2008 Workshop
July 7-8, 2008, Princeton, NJ
http://www.cs.utah.edu/ec2
Day 1, Monday, July 7
Session 1, 9am - 10.30am
  • Invited Talk (45 mins, including questions): Edward Lee, UC Berkeley
  • Position Papers (15 mins each, including questions):
    • Patrice Godefroid and Nachiappan Nagappan, ``Concurrency at Microsoft - An Exploratory Survey''
    • Thomas Ball, Sebastian Burckhardt, Madan Musuvathi, and Shaz Qadeer, ``First-class Concurrency Testing and Debugging''
    • Venkatram Vishwanath and Lenore Zuck, ``Verification of Data Intensive High Performance Computing Middleware''
Session 2, 11am - 12.30pm
  • Invited Talk (45 mins, including questions): Saman Amarsinghe, MIT
  • Position Papers (15 mins each, including questions):
    • Andrew W. Appel, ``Foundational High-Level Static Analysis''
    • Sriram Rajamani, G. Ramalingam, Venkatesh-Prasad Ranganath, and Kapil Vaswani, ``Controlling Non-determinism for Semantic Guarantees''
    • Loïc and Stephan Merz, ``Towards automatic proofs of lock-free algorithms''
Session 3, 2pm - 3.30pm
  • Invited Talk (45 mins, including questions): Vivek Sarkar, Rice University
  • Position Papers (15 mins each, including questions):
    • Kedar S. Namjoshi, ``Are Concurrent Programs That Are Easier to Write Also Easier to Check?''
    • Martin Vechev, Eran Yahav, Maged Michael, Hagit Attiya, and Greta Yorsh, ``Computer Assisted Construction of Efficient Concurrent Algorithms''
    • Kai Trojahner, ``Assembling Concurrent Programs Correctly from Data-Parallel Program Bricks''
Session 4, 4pm - 4.45pm
  • Position Papers (15 mins each, including questions):
    • Tevfik Bultan, ``Developing Verifiable Concurrent Software''
    • Fred G. Gustavson, ``The Relevance of New Data Structure Approaches for Dense Linear Algebra in the new Multi-Core / Many Core Environments''
    • Brad D. Bingham and Mark R. Greenstreet, ``An Energy Aware Model of Computation''
Session 5, Panel, 4.45pm - 6pm


Day 2, Tuesday, July 8
Session 6, 9am - 10.30am
  • Invited Talk (45 mins, including questions): Jim Larus, Microsoft Research
  • Position Papers (15 mins each, including questions):
    • Pawel T. Wojciechowski, ``Extending Atomic Tasks to Distributed Atomic Tasks''
    • Kousha Etessami and Patrice Godefroid, ``An Abort-Aware Model of Transactional Programming''
    • Rachid Guerraoui, Thomas A. Henzinger, Barbara Jobstmann, and Vasu Singh, ``Model Checking Transactional Memories''
Session 7, 11am - 12.30pm
  • Invited Talk (45 mins, including questions): Ravi Rajwar, Intel Corporation
  • Position Papers (15 mins each, including questions):
    • Ariel Cohen, Amir Pnueli, and Lenore D. Zuck, ``Formal Verification of Transactional Memories''
    • Eric Koskinen and Maurice Herlihy, ``Aggressive Transactional Boosting''
    • Sebastian Burckhardt and Madanlal Musuvathi, ``Memory Model Safety of Programs''
Session 8, 2pm - 3.30pm
  • Invited Talk (45 mins, including questions): Michael Scott, University of Rochester
  • Position Papers (15 mins each, including questions):
    • Shaz Qadeer, ``The Case for Context-Bounded Verification of Concurrent Programs''
    • Zijiang Yang and Karem Sakallah, ``SMT-based Symbolic Model Checking for Multi-Threaded Programs''
    • Murali Talupur and Helmut Veith, ``Domain Pattern Abstraction + Ptolemaic Abstract Domains = Environment Abstraction for Concurrent Systems''
Session 9, Open Mike, 4pm - 5pm



Description:
Our ability to effectively harness the computational power of the next generation of multiprocessor and multicore architectures is predicated upon advances in programming languages and tools for developing concurrent software. This has resulted in a surge of concurrency-related research activity from different viewpoints, such as rethinking of programming abstractions and memory models; standardization and formalization of commonly used APIs (e.g., MPI, OpenMP); and new forms of hardware support for parallel processing.

While developing tools for verifying and debugging concurrent systems has been an important theme at CAV, we believe that formal methods research can go beyond checking existing code/systems, and play a role in identifying the "right" abstractions for concurrency. The goal of this workshop is to bring together CAV researchers with experts who are involved in developing multicore architectures, programming languages, and concurrency libraries.

Invited Speakers:
Format:
The two-day workshop will include six invited talks and several panel sessions. Authors of position papers will be given an opportunity to present their ideas either as a short presentation or as a poster. A booklet consisting of all the position papers will be distributed to the workshop participants.

We seek submissions of position statements between 2 and 4 pages. There are many possible themes for a position paper, including a survey of the authors' relevant recent research, a discussion of deficiencies in current languages and tools, challenges for future verification research, and/or a vision for change. Submissions on all topics relevant to the workshop title are welcome, including Of particular interest are position statements from those engaged in significant case studies.

Submission deadline: April 10, 2008

Notification of acceptance: April 25, 2008

Submission instructions: Prepare a 2-4 page position paper in PDF format using any tool you like. The title and the name of the authors should appear at the top of the first page. Email this PDF document to ec2@cis.udel.edu. The position papers will be compiled into a booklet that will be handed out to all workshop participants on the first day of the workshop. The papers will not be published.

At least one author of each position paper is expected to register and attend to present the same.

For more information: Visit http://www.cs.utah.edu/ec2/

Organizers:
TV06 (a related workshop)

Detailed Plans
This document was translated from LATEX by HEVEA.