--------------------------------------------------------------------------
| DIMACS: Center for Discrete Mathematics & Theoretical Computer Science |
| A National Science Foundation Science and Technology Center            |
--------------------------------------------------------------------------



            DIMACS Summer School on Applied Logic and Algorithms
                         General Announcement

Introduction

The 1995--96 DIMACS Special Year topic is Logic and Algorithms.
To launch this Special Year, DIMACS will hold a Summer School on
Applied Logic and Algorithms during August 1995.  The Summer School
is intended to expose industry, graduate students, postdocs, and
experienced researchers from other fields to the three focus areas
of the Special Year --- Finite-Model Theory, Proof Complexity, and
Computer-Aided Verification.  The courses will provide students with
a deep understanding of these research areas and will point out
connections with applications.

* Finite-Model Theory is the study of the finite mathematical
  structures that satisfy particular axioms.  It already has
  yielded elegant connections with theoretical computer science,
  including model-theoretic characterizations of complexity classes.
  Further, when a class of finite mathematical structures such as
  graphs is equipped with probability measures, one often can
  develop powerful meta-theorems called zero-one laws, which give
  conditions under which probabilities must approach zero or one as
  the structure size goes to infinity.  Much recent interest in
  this area has concentrated on questions that have no infinite
  counterparts.

* Proof complexity studies the lengths of proofs and the strength
  and computational content of inferences in logical formalisms.
  A recent focus is on lower bounds for the length and syntactic
  complexity of propositional proofs, with connections to the
  "P vs. NP" question, to circuit complexity, and to cryptographic
  security.  Another focus involves bounded fragments of Peano
  Arithmetic, restricted so that they define exactly the predicates
  and functions in complexity classes such as the polynomial
  hierarchy.  Exciting recent work has shown that if certain such
  theories of bounded arithmetic can prove lower bounds in
  complexity theory, then corresponding cryptographic systems
  cannot be secure.

* Computer-Aided Verification studies algorithms and structures
  for formally verifying properties of programs.  It draws upon
  techniques from graph theory, combinatorics, automata theory,
  complexity theory, Boolean functions and algebras, logic, Ramsey
  theory and linear programming.  It also is linked to Finite-Model
  Theory through the study of finite-state programs, which often
  arise in real-world software and hardware protocols.  Since the
  DIMACS CAV workshop in 1990, worldwide interest in CAV has grown
  enormously, not only in academia but in companies like Intel, DEC, 
  SGI, Motorola, Sun, IBM, and AT\&T.  This creates an unusual and rewarding
  opportunity to see theory put directly into practice.



The Summer School will consist of three successive one-week tutorial
courses, one for each topic.  Each week, 3-5 experts will lecture for
a total of approximately 20 hours, and time and space will be provided
for informal discussion as well.

We are seeking funding to support attendance by graduate and
postdoctoral students, emphasizing participation by members of
underrepresented groups.

The DIMACS Conference Center at Rutgers can accommodate about 80
participants.  Subject to this capacity constraint, courses are open to
all researchers; there is no registration fee.  Although registration
at the door is permitted, we ask that you register by June 30, 1995,
to give us some idea of attendance.  Pre-registrants will be given
priority in case of capacity constraints.  In addition, information on
local housing will be sent to people who pre-register.  

DIMACS is a Science and Technology Center funded by the NSF, with
institutional participation by Rutgers University, Princeton 
University, AT&T Bell Laboratories, and Bellcore.  Research and 
education activities at DIMACS focus on such areas as analysis of 
algorithms, combinatorics, complexity, computational algebra, discrete 
and computational geometry, discrete optimization and graph theory.  
A primary activity of the Center is to sponsor Special Years, year-
long research programs on topics of current interest.  The last three
Special Year topics have been Computational Biology, Parallel
Computing, and Combinatorial Optimization.

The following form may be used either to pre-register for courses or to
apply for financial support.  The deadline for applying for financial
support is May 30, 1995.  In either case, please email it (ASCII or
PostScript) to center@dimacs.rutgers.edu, or mail it to
 
    Rutgers University
    DIMACS Center
    95 Frelinghuysen Road
    Piscataway, NJ 08854-8018

DIMACS Center; Rutgers University; 96 Frelinghuysen Rd.; Piscataway, NJ 08854-8018 
 TEL: 732-445-5928 FAX: 732-445-5932  **  EMAIL:  center@dimacs.rutgers.edu
                    WWW:  http://dimacs.rutgers.edu


           DIMACS Summer School 1995: Registration Form

Name: ____________________________________________________________

Affiliation: _____________________________________________________

Current position: ________________________________________________

Mailing Address: _________________________________________________
                 _________________________________________________
                 _________________________________________________
                 _________________________________________________

Email address: ___________________________________________________

Daytime telephone number: ________________________________________

Fax number: ______________________________________________________

I plan to attend the following course(s) (check all that apply):

Finite-Model Theory                          14--18 Aug       ____ 
Bounded Arithmetic and Proof Complexity      21--25 Aug       ____
Computer-Aided Verification                28 Aug -- 1 Sept   ____

..................................................................

The remaining questions are for people applying for financial support.
If you are only pre-registering, not applying for support, STOP HERE.

Citizenship: _____________________________________________________

Sex (optional): _____

Major disability (optional): Yes _____         No _____

Primary racial or ethnic background (optional):
American Indian or Alaskan Native ___              Asian        ___
Black, not of Hispanic origin     ___            Hispanic       ___
White, not of Hispanic origin     ___          Pacific Islander ___

Names, affiliations, and phone numbers or email addresses of two
people familiar with your research and education who have agreed to
serve as references:
___________________________________________________________________
___________________________________________________________________
___________________________________________________________________
___________________________________________________________________
Please ask these people to send letters of recommendation to DIMACS 
(address above).  If you're a graduate student
or a new Ph.D., please send an unofficial copy of your graduate
transcript to the same address.

Please attach a current CV, a bibliography, and a personal statement
of at most one page, outlining what you hope to gain from, and
contribute to, the Summer School.  Discuss related research you've
done in the past, your research plans for the near future, and how
the Summer School will help you further them.


Course in Finite-Model Theory
Dates: August 14-18, 1995
Organizer: James Lynch 

The continuous interaction between logic and computer science during
the past twenty five years has  brought about a change in the focus
of traditional mathematical logic. For almost a century mathematical
logic centered around the study  of first-order logic on the class
of all structures (both finite and infinite) or over fixed infinite
structures of mathematical significance, such as the integers, the
real numbers, or more abstract spaces and algebraic structures.
While exploring the connections between logic and computer science,  
researchers realized the importance of focusing on the logical
properties of finite structures. As a result, in recent years first-
order logic and various extensions of first-order logic have been
investigated in depth with regard to their finite models.  This area
of research, which became known as  finite-model theory, brings
together mathematical logic, combinatorics, computational complexity
theory, and database theory.

The finite-model theory course will consist of three parallel, but
interconnected, series of lectures.

Descriptive Complexity: The main aim of descriptive complexity is
  to classify algorithmic problems according to the resources
  needed to express such problems in various logics on finite
  models.  Research in descriptive complexity has amplified the
  close relationship between logic and computation, as evidenced
  by natural characterizations of virtually all major complexity
  classes in terms of logical expressibility on finite models.
  In turn, this provides an opportunity to analyze complexity
  classes by studying the expressive power of of logics on finite
  structures.
Expressive Power of Logics: The lectures on expressive power will
  present methods for investigating both the strengths and the
  limitations of logics on finite structures. In particular, the
  method of combinatorial games has been used extensively to obtain
  upper and lower bounds for expressibility, and to delineate the
  relative expressive power of logics.  This area interacts directly
  with database theory, since a relational database is essentially a
  finite model, and many database query languages correspond to
  logics on finite structures. 
Random Finite Models: The third area, random finite models, explores
  the connections between asymptotic combinatorics and logics on
  finite structures.  Sets of finite models definable by formulas
  in various logics are considered, and probability measures are
  assigned to the sets of finite models of a given size. In many
  cases, the probability that a formula holds for a random model
  has a simple asymptotic behavior.  Random finite-model theory
  seeks to determine which classes of random finite models and
  logics exhibit such behavior, as well as to identify in each case 
  the computational complexity of the asymptotic behavior.

Lecturers

* Neil Immerman (Ph.D. Cornell University) is an Associate
  Professor of Computer Science at the University of Massachusetts,
  Amherst.  He has also taught at Tufts University and Yale
  University.  His research interests include descriptive
  complexity, complexity theory, database theory and logic.

* Phokion G. Kolaitis (Ph.D. University of California, Los Angeles)
  is a Professor of Computer and Information Sciences at the
  University of California, Santa Cruz.  He has held visiting
  appointments at Stanford University and the IBM Almaden Research
  Center.  His research interests include finite-model theory,
  computational complexity, and database theory. In recent years,
  he has served on the program committees of several international
  conferences and on the editorial boards of two journals.  In 1993
  he was awarded a John Simon Guggenheim Memorial Foundation
  Fellowship.

* James F. Lynch (Ph.D. University of Colorado) is an Associate
  Professor in the Department of Mathematics and Computer Science
  at Clarkson University. He has held visiting appointments at the
  University of Florida, the Courant Institute of Mathematical
  Sciences, New York University, and the University of Western
  Australia. Most of his work in finite-model theory has involved
  random finite models. He has also done research in combinatorics,
  mathematical biology, and complex systems.

Course in Bounded Arithmetic and Complexity of Proofs
Dates: August 21-25, 1995
Organizer: Toniann Pitassi 

The study of the complexity of proofs is fundamental to logic,
and has rich connections to complexity theory as well. First, the
complexity of propositional proof systems is intimately connected to
whether NP equals co-NP. Secondly, provability of certain statements
in feasible arithmetic (theories whose inferences have feasible
computational content) gives rise to feasible algorithms. These two
areas, propositional proof complexity and feasible arithmetic, are
closely related to one another, and also to other fundamental problems
in circuit complexity. In this workshop, we shall first cover the
basics of propositional proof complexity and feasible (bounded)
arithmetic, then introduce more advanced topics toward the end of
the week.

Complexity of Propositional Proof Systems: In propositional logic,
  we are concerned with the basic question "How long must a proof
  of a propositional tautology be, as a function of the size of
  the tautology?"  The best known upper bound for all known proof
  systems is exponential in the size of the tautology, and it is
  conjectured that a similar lower bound holds.  The (non-)existence
  of a superpolynomial lower bound for all proof systems is
  equivalent to whether or not NP equals co-NP, a question still
  unsolved after 25 years of study.  An approach toward proving that
  NP is not equal to co-NP is to establish superpolynomial lower
  bounds for specific proof systems of greater and greater strength.
  The last ten years have shown substantial progress in proving such
  lower bounds, often using connections and techniques from
  complexity theory. We shall discuss Resolution, Frege, Bounded-
  Depth Frege, Extended Frege, and Cutting Planes systems.  We shall
  also cover recent lower bounds for Resolution, bounded-depth Frege,
  and Cutting Planes systems.

Bounded arithmetic: The concept of a feasible proof --- a proof whose
  inferences correspond to computationally feasible operations ---
  has attracted much research in the last ten years. It has emerged
  as a robust and natural concept with several elegant formalizations,
  including "bounded arithmetic", a hierarchy of bounded subsystems of
  Peano arithmetic.  The subsystem known as S^1_2, introduced by S.
  Buss in 1986, is widely believed to capture the intuitive notion of
  "feasibly provable": a fundamental theorem due to Buss states that
  proofs of certain types of statements in S^1_2 give rise to
  polynomial-time algorithms with feasible correctness proofs.  This
  theorem was the first of several "witnessing theorems" for bounded
  arithmetic.  We shall thoroughly discuss and prove Buss's witnessing
  theorem, then state and prove another witnessing theorem for bounded
  arithmetic, showing that the provable collapse of the bounded
  arithmetic hierarchy is equivalent to the collapse of the
  polynomial-time hierarchy.

Connecting Feasible Arithmetic and Propositional Logic: We shall then
  explain the connections between systems of bounded arithmetic and
  propositional proofs. In particular, S^1_2 can be viewed as a
  uniform version of polynomial-sized Extended Frege proofs, and
  S_2(f) as a uniform version of polynomial-sized bounded-depth Frege
  proofs.  Lastly, we discuss what can and cannot be proven within
  bounded arithmetic.  It turns out that a large portion of
  mathematics can be carried out within S^1_2, including almost all
  known explicit circuit lower bounds. This not only shows the
  surprising power of S^1_2, but has also led to simpler proofs of
  known lower bounds. We also discuss consequences of the provability
  or unprovability of certain complexity-theoretic statements in
  bounded arithmetic.

Advanced Topics: Time permitting, we shall also cover several
  advanced topics:
  * The work of Razborov and Rudich on Natural Proofs, and 
    Razborov's work on the unprovability of P vs. NP in S^1_2;
  * A new, algebraic proof system based on Hilbert's
    Nullstellensatz, and new results in this area; and
  * Interpolation theorems.

Lecturers
* Samuel R. Buss (Ph.D. Princeton University) is Professor of
  Mathematics and Adjunct Professor of Computer Science at the
  University of California, San Diego.  He has also held visiting
  positions at the Mathematical Sciences Research Institute and at
  the University of California, Berkeley.  His research interests
  are in mathematical logic and computer science, specializing in
  bounded arithmetic, proof complexity, circuit and computational
  complexity, and pattern matching.

* Paul Beame (Ph.D. Toronto) is an Associate Professor in the
  Department of Computer Science and Engineering at the University
  of Washington.  He was a postdoctoral fellow at M.I.T. and in
  1988 he received an NSF Presidential Young Investigator Award.
  His research interests include computational complexity, parallel
  computation, and logic, with a particular emphasis on lower bounds.

* Alasdair Urquhart (Ph.D. Pittsburgh) is Professor of Philosophy
  and Adjunct Professor of Computer Science at the University of
  Toronto.  His research interests include non-classical logics,
  algebraic logic, lattice theory, the history of logic and
  complexity theory.  He is the editor of Volume 4 of the Collected
  Papers of Bertrand Russell.  He has served as a consulting editor
  of the Journal of Symbolic Logic, and is currently an editor of
  the Springer Lecture Notes in Logic series.

Course in Computer-Aided Verification
Dates: August 28 -- September 1, 1995
Organizer: Kenneth McMillan 

The problem of verifying computer programs and computer systems dates
back to the invention of the bug. Almost since that time, computer
scientists have dreamt of computer-aided techniques that could verify
the correctness of these complex systems. Recently, the need for such
techniques has become increasingly urgent, as systems with the
complexity of the last decade's ``mainframes'', now are fabricated on
a single silicon chip.

This course will cover a variety of methods in computer-aided formal
verification, ranging from general and powerful theorem-proving
methods, that require significant user guidance, to more specialized,
highly automated tools, especially model-checkers. 

Overview

The most general approach to verification is to state the correctness
condition for a system, as a theorem in a mathematical logic, and to
generate a mechanically checked proof of this theorem using a general-
purpose theorem-prover.  This approach has attained significant
successes in verifying microprocessor designs, for example.  Theorem-
provers generally provide decision procedures or heuristic algorithms
to automate some steps of the proof, but require the user to provide
at least the broad outline of the proof.

At the other extreme of the spectrum lies the finite-state technique
of model-checking.  A model-checker works on a finite-state model of
the system to be verified, and a logical specification of a desired
behavior of the system model. It checks that the model adheres to the
specification by effectively searching the entire state space of the
model. Model-checking has been used to verify automatically (or find
errors in) systems of significant complexity, such as the cache
coherence protocols of multiprocessors.  Such results are achieved by
using specification languages (such as temporal logics) that are
expressive enough to state the required properties of concurrent
systems, and yet can be checked with feasible computational complexity.
In most cases heuristics are required, in order to circumvent the
exponential explosion of states that occurs as a function of the number
of components, in concurrent systems.  These heuristics include using
the compressed representations of sets of states afforded by binary
decision diagrams, as well as using reduction techniques.  The
reduction techniques are heuristics which often can reduce the
computational complexity of model-checking through a combination of
abstraction (eliminating irrelevant detail) and decomposition (breaking
large verification problems into small verification problems). Other
reduction techniques exploit symmetries, and the partial ordering of
events in concurrent systems.

Emphasis of the course

The course will provide a grounding in the basic models, theories and
methods of computer-aided formal verification.  This material will be
introduced using realistic examples, which also will provide exposure
to a variety of languages and tools currently used in formal verification. 

Emphasis will be placed on comparing different methods, in terms of
expressiveness, complexity, degree of automation, and the tradeoff
between the expressiveness of a language and the complexity of its
decision procedure. Some of the leading edge research problems will
be introduced, such as the automatic generation of abstractions.

Course outline
* Verification using general-purpose theorem-provers
* Concurrency, temporal logic and automata theory
* Abstraction and compositional methods
* Methods based on binary decision diagrams
* Partial-order based methods
* Real-time and hybrid systems

Lecturers
* Rajeev Alur (PhD, Stanford University, 1991) has been a member of
  the technical staff at AT&T Bell Laboratories in Murray Hill, NJ
  since 1991. His reasearch interests include verification of
  reactive systems,  particularly real-time and embedded systems,
  temporal logics, and distributed computing. 

* David L. Dill (Ph.D., Carnegie Mellon University, 1987) is an
  Associate Professor of Computer Science at Stanford University
  and a member of the Computer Systems Laboratory.  Professor Dill's
  research area is the modeling, analysis, and verification of
  finite-state concurrent systems, particularly hardware designs.

* Robert Kurshan (Ph.D., Univ. of Washington, 1968) has been a
  member of the Mathematics Research Center at Bell Labs in Murray
  Hill, NJ since 1969. His areas of research include: ring theory,
  analytical number theory, coding theory, digital signal processing,
  approximation theory and computer-aided verification.

* Kenneth McMillan (Ph.D., Carnegie Mellon, 1992) was previously a
  member of the technical staff at AT\&T Bell Laboratories in Murray
  Hill, NJ, and is now with Cadence Berkeley Labs in Berkeley, CA.
  His primary research area is the formal verification of hardware
  systems.

* J. Strother Moore (Ph.D., University of Edinburgh, 1973) spent
  three years at Xerox Palo Alto Research Center, and five years
  at the Computer Science Laboratory of SRI International before
  joining the faculty of the Department of Computer Sciences at the
  University of Texas at Austin in 1981. Along with Robert S. Boyer,
  he created the Boyer-Moore automatic theorem-prover and is a
  founder of Computational Logic, Inc., where he has worked since
  1987, primarily on mechanized theorem-proving and its application
  to establish properties of hardware and software systems.

* Pierre Wolper (Ph.D., Stanford University, 1982) was a member of
  the technical staff of Bell Laboratories in Murray Hill, NJ, from
  1982 to 1986, where he pursued research on program specification
  and verification, temporal and modal logics, and distributed
  computing.  He is now a full professor at the University of Liege.
  His current research interests include algorithms and data
  structures for the verification of reactive systems, temporal
  logics, and temporal databases.