NSF Workshop on Symbolic Computation

NSF Workshop on Symbolic Computation for Constraint Satisfaction Problems

This workshop is focused on the role of symbolic decision procedures for constraint satisfaction problems. The workshop brings together computer science researchers in diverse areas such as program analysis, formal verification, AI planning, optimization, and hybrid systems. The program consists of a series of talks that will review the state of the art in symbolic decision procedures, the role that constraint satisfaction plays in various computing problems, and challenges for future research.

Workshop Report

Logistics

Location: Room A2002, FDIC Building, 3501 Fairfax Drive, Arlington, VA.
Time: Friday, November 14, 2008, 8.30am -- 5pm
Organizer: Rajeev Alur, University of Pennsylvania
NSF Program Manager: Lenore Mullin, CISE CCF

Schedule

Coffee / Breakfast : 8.30 -- 9.00
9.00 -- 9.15: Welcome by Lenore Mullin, Program Director, Algorithmic Foundations Cluster, CISE
Session I : Computational Tools for Constraint Satisfaction Problems : 9.15 -- 11.45
- Sharad Malik, Princeton University
  SAT and QBF: Trick or Treat? Talk slides
- Clark Barrett, New York University
  Satisfiability Modulo Theories: Successes and Challenges. Talk slides
- Jose Meseguer, University of Illinois at Urbana-Champaign
  Rewriting Needs Constraints, and Constraints Need Rewriting. Talk slides Martine Ceberio, University of Texas at El Paso
  Symbolic-Numeric Algorithms for Constraint Solving. Talk slides
- Bart Selman, Cornell University
  Planning as Satisfiability: Progress and Challenges. Talk slides
Lunch : 11.45 -- 12.45
Session II : Role of Constraint Satisfaction in Computer Science Problems : 12.45 -- 3.15
- Leonardo de Moura, Microsot Research
  Software Verification and Testing. Talk slides
- Alex Aiken, Stanford University
  From the Sublime to the Ridiculous: Constraint Satisfaction Problems in Program Analysis. Talk slides
- Ken McMillan, Cadence Labs
  Symbolic Model Checking
- Andre Platzer, Carnegie Mellon University
  Symbolic Computations in Hybrid Systems Verification. Talk slides
- Werner Damm, Universitat Oldenburg, Germany
  Automatic Verification and Analysis of Complex Systems: Key results of the transregional collaborative research project AVACS. Talk slides
Coffee Break: 3.15 -- 3.30
Panel Discussion on Research Challenges : 3.30 -- 4.30
- Amir Pnueli, New York University
- Tom Reps, University of Wisconsin, Madison
- Natarajan Shankar, SRI. Talk slides
Wrap-up : 4.30 -- 5.00

Security and Building Access

The FDIC building security policy requires that all individuals entering the hotel/training facility present government issued photo identification. Please arrive ½ hour prior to scheduled event in order to process through security. Security has been notified of your visit. The security guards may ask you to identify whom you are visiting or the meeting you are attending. Please also remember to bring identification. The FDIC accepts the following forms of ID:

State Driver's License with photograph (Most efficient method)
State non-driver's identification card with photograph
Military identification
Valid United States Passport
Government issued photographic identification card with prior approval
INS Identification card
Foreign Passport with prior approval from FDIC (pre-registered)
FDIC Sponsor Verification

Maintained by Rajeev Alur