Workshop: Special Year on Logic and Algorithms - One Year Later
July 23-25, 1997
DIMACS Center, CoRE Building, Rutgers University
Organizers:
Eric Allender allender@cs.rutgers.edu
Robert Kurshan k@research.bell-labs.com
Moshe Vardi vardi@cs.rice.edu
The 1995-1996 Special Year on Logic and Algorithms (SYLA) was aimed at
bridging a dichotomy in computer science between two major branches of
research, one in algorithms and complexity, and the other one in models
and semantics. SYLA focused on three bridge areas: computer-aided
Verification (CAV), finite-model theory (FMT), and proof complexity
(PC). Computer-Aided Verification studies algorithms and structures for
verifying properties of programs. Finite-model theory studies the
logical properties of finite structures, and has intimate connections
with complexity theory and database theory. Proof complexity studies
the length of proofs and the complexity of the inference steps within
the proof. SYLA consisted of a 3-week long summer school, 11 workshops,
and a federated logic conference.
You are invited to participate in a DIMACS Workshop on "Logic and
Algorithms: One Year Later", which will be held at Rutgers University,
on July 23-25, 1997. The goal of the workshop is to follow up on SYLA.
The workshop will cover the three major topics of the Special Year,
computer-aided verification, finite-model theory, and proof complexity.
The program of the workshop will consist of 1-hour-long survey talks
as well as shorter 1/2-hour-long talks. The speakers will report on
research results that arose during the Special Year or following it.
During the Special Year, we conducted many specialized workshops. In
this workshop, we will focus on bringing the three topics together,
in an attempt to provide participants with a broader view of the field.
For more information see
http://dimacs.rutgers.edu/Workshops/SYLA-Yearlater/index.html
Prospective attendees are asked to register for the workshop
by June 20, 1997, in order to enable the organizers estimate
attendance.
Tentative Program:
July 23, 1997
Wednesday Morning: PC
8:00 - 8:30: Continental breakfast
8:30 - 9:30: T. Pitassi: On the Status of Propositional Proof
Complexity
9:30 - 10:00: S. Cook: Proof Complexity and the Collapse of P
to NC1
10:00 - 10:30: Coffee Break
10:30 - 11:30: A. Razborov: Lower Bounds for Algebraic Proof Systems
11:30 - 12:00: R. Impagliazzo: Lower bounds for the propositional
calculus and Groebner basis algorithm
12:00 - 1:30: Lunch
Wednesday Afternoon: FMT
1:30 - 2:30: L. Libkin: Local properties in finite-model theory
2:30 - 3:00: S. Burris: Bootstrapping 0--1 Laws
3:00 - 3:30: Coffee Break
3:30 - 4:30: E. Rosen: On fragments of existential finite-variable logic
4:30 - 5:00: K. St. Jon: Limit Probabilities for Random Unary Predicates
5:00 - 5:15: Coffee Break
5:15 - 5:45: G. Turan: Computational learning theory and logic
5:45 - 6:15: L. Thoma: On the Limit Probabilities of the First Order
Properties of Graphs
July 24, 1997
Thursday Morning: CAV
8:00 - 8:30: Continental breakfast
8:30 - 9:30: R. Kurshan: Verification Technology Transfer
9:30 - 10:00: E. Boumamova: Compiler Design using a Formal
Specification
10:00 - 10:30: Coffee Break
10:30 - 11:30: N. Immerman: Descriptive Complexity and Computer-Aided
Verification
11:30 - 12:00: V. Levin: Verification of Message Sequence Charts using
COSPAN
12:00 - 1:30: Lunch
Thursday Afternoon: PC
1:30 - 2:30: S. Buss: Interpolation, Arithmetic, and Cryptography
2:30 - 3:00: C. Pollett: General Definability and Conservation Results
in Bounded Arithmetic
3:00 - 3:30: Coffee Break
3:30 - 4:30: P. Pudlak: On proof systems for integer linear programing
4:30 - 5:00: J. Avigad: Building Finite Approximations to Models
of Arithmetic
5:00 - 5:15: Coffee Break
5:15 - 5:45: M.L. Bonet: On Feasible Interpolation for Frege
Proof Systems and Other Weaker Systems
5:45 - 6:15: J. Toran and J. Messner: Optimal Proof Systems and
Complete Sets
July 25, 1997
Friday Morning: FMT
8:00 - 8:30: Continental breakfast
8:30 - 9:30: M. Grohe: Finite-variable logics and polynomial time
9:30 - 10:00: J. Baldwin: $k$-variable Theories of Finite Models
10:00 - 10:30: Coffee Break
10:30 - 11:30: M. Otto: Decision problems for two-variable logics
11:30 - 12:00: A. Blass: Choiceless polynomial time
12:00 - 1:30: Lunch
Friday Afternoon: CAV
1:30 - 2:30: O. Kupferman: Reduction Hierarchies
2:30 - 3:00: A. Puri: Data Structures for Storing States
3:00 - 3:30: Coffee Break
3:30 - 4:00: D. Peled: Software Design Tools
4:00 - 4:30: H. Yenigun: Verifying SDL at a Hardware Interface
4:30 - 5:00: Mahesh Vishwanathan: NEXP-completeness and OBDDs
5:00 - 5:15: Coffee Break
5:15 - 5:45: R. Alur: TBA
5:45 - 6:15: A. Emerson: TBA
-------------------------------------------------------------------------------
The dbworld alias reaches many people, and should only be used for
messages of general interest to the database community.
Requests to get on or off dbworld should go to listproc@cs.wisc.edu.
to subscribe send
subscribe dbworld Your Full Name
to unsubscribe send
unsubscribe dbworld
to change your address
send an unsubscribe request from the old address
send a subscribe request from the new address
to find out more options send
help
------------------------------------------------------------------------FOOTER-