• Steve's Matrix Mutiply Verification Challenge is HERE.

Day 1, Monday, July 7

Opening Remarks, 8:55am - 9:00am

Session 1, 9am - 10.30am

• Invited Talk (45 mins, including questions): James Larus, Microsoft Research. ``Spending Moore's Dividend'' [Talk Slides]
  
  
• 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''
  • Murali Talupur and Helmut Veith, ``Domain Pattern Abstraction + Ptolemaic Abstract Domains = Environment Abstraction for Concurrent Systems''

Session 2, 11am - 12.30pm

• Invited Talk (45 mins, including questions): Edward Lee, UC Berkeley ``Balancing Expressiveness and Analyzability in Stream Formalisms'' [Talk Slides]
  
  
• 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''
  • Loic Fejoz and Stephan Merz, ``Towards automatic proofs of lock-free algorithms''

Session 3, 2pm - 3.30pm

• Invited Talk (45 mins, including questions): Saman Amarsinghe, MIT ``StreamIt --- A Programming Language for the Era of Multicores'' [Talk Slides]
  
  
• 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'' [Talk Slides]
  • Brad D. Bingham and Mark R. Greenstreet, ``An Energy Aware Model of Computation''

Session 5, Open Mike, 4.45pm - 6pm

Day 2, Tuesday, July 8

Session 6, 9am - 10.30am

• Invited Talk (45 mins, including questions): Michael Scott, University of Rochester ``Tracking Transactional State'' [Talk Slides]
  
  
• 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.15pm

• Invited Talk (45 mins, including questions): Ravi Rajwar, Intel Corporation ``Building Functionally Correct Systems in the Multi-Core Era''
  
  
• Position Papers (15 mins each, including questions):
  • Ariel Cohen, Amir Pnueli, and Lenore D. Zuck, ``Formal Verification of Transactional Memories''
  • Sebastian Burckhardt and Madanlal Musuvathi, ``Memory Model Safety of Programs''

Session 8, 2pm - 3.30pm

• Invited Talk (45 mins, including questions): Vivek Sarkar, Rice University ``Static and Dynamic Analysis of Parallel Programs''
  
  
• 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''
  • Venkatram Vishwanath and Lenore Zuck, ``Verification of Data Intensive High Performance Computing Middleware''
  
  

Session 9, Panel, 4pm - 5.30pm

Title:

CAV for multi-core / concurrent programming

Panelists:

Sharad Malik, Milo Martin, Amir Pnueli, and Serdar Tasiran

Moderator:

Ganesh Gopalakrishnan

Agenda:

The panelists will begin with a statement of their views on what concrete directions the CAV community can pursue to advance our capabilities in areas that (EC)² covers. The floor will then be open for focussed questions, opinions, and discussions around them.

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:

• Saman Amarsinghe, MIT
• Jim Larus, Microsoft Research
• Edward Lee, UC Berkeley
• Ravi Rajwar, Intel Corporation
• Vivek Sarkar, Rice University
• Michael Scott, University of Rochester

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

• Transactional memory
• Programming constructs for concurrency
• Formalization of concurrency libraries
• Verification tools
• Hardware support for correctness
• Introducing concurrency in education

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:

• Rajeev Alur, University of Pennsylvania
• Ganesh Gopalakrishnan, University of Utah
• Vineet Kahlon, NEC Labs
• Stephen Siegel, University of Delaware

TV06 (a related workshop)

Detailed Plans

This document was translated from L^AT_EX by H^EV^EA.