-------------------------------------------------------------------------- | 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 LynchThe 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.