DIMACS Special Year on Logic and Algorithms: 1995 - 1996

Schedule of Events

Tutorial on Computer-Aided Verification

Date: August, 1995
Organizer: Ken McMillan
Speakers: Rajeev Alur, Bob Kurshan, Ken McMillan, J. Moore, Pierre Wolper
Email: mcmillan@cadence.com
Tutorial on Finite-Model Theory Date: August, 1995
Organizer: Jim Lynch
Speakers: Neil Immerman, Phokion Kolaitis, Jim Lynch
Email: jlynch@sun.mcs.clarkson.edu
Schedule: Press here
Tutorial on Proof Complexity
Date: August, 1995
Organizer: Toni Pitassi
Speakers: Sam Buss, Toni Pitassi, Alasdair Urquhart
Email: toni@cs.pitt.edu
Schedule: Press here
Workshop on Verification and Control of Hybrid Systems
Date: October 22-25, 1995 -- DATE CHANGE
Organizers: Rajeev Alur, Tom Henzinger
Email: alur@research.att.com, tah@cs.cornell.edu
Description: A hybrid system contains both discrete and continuous compo- nents. A typical example is a digital controller of an analog process. As embedded controllers become ubiquitous in life-critical applications, formal design support for hybrid systems becomes increasingly important.

The emerging theory of hybrid systems combines both semantic aspects, such as system modeling and specification, and algorithmic aspects, such as the algorithmic solution and complexity of verification and control problems. The analysis of hybrid systems requires, moreover, both combinatorial and analytical techniques and lies at the intersection of computer science and control theory. It is therefore the purpose of the workshop to bring together researchers from both communities.

Workshop on Logic and Random Structures
Date: November 5-7, 1995
Organizers: Ravi Boppana, James Lynchand Kevin Compton
boppana@cs.nyu.edu, jlynch@sun.mcs.clarkson.edu kjc@eecs.umich.edu
Description: The central theme will be the relationship between logic and probabilistic techniques in the study of finite structures. In one direction, this topic includes recent research on limit laws and zero-one laws. A limit law holds in a class of finite structures if all properties decribable in some logical language have limiting probabilities as structure size grows; a zero-one law holds (as in the classic work of Glebskii et. al. and Fagin) if the limiting probabilities are always 0 or 1. This work has been applied to areas such as analysis of algorithms for database query optimization and polynomial time approximation of NP optimization problems. In the other direction, this topic covers use of probabilistic methods to establish lower bounds in circuit complexity. Particular emphasis will be placed on the connections between first-order logic and constant depth circuits with unbounded fan-in. While there will be natural connections to the workshop on "Descriptive complexity and finite models", here calculation of probabilities has center stage.
Workshop on Finite Models and Descriptive Complexity
Date: January 14 - 17, 1996
Organizers: Neil Immerman and Phokion Kolaitis
Email: immerman@cs.umass.edu, kolaitis@cs.ucsc.edu
Description: Descriptive Complexity studies the resources needed to describe properties concerning finite logical structures. This area has been developing through a continuous interaction between computational complexity, finite model theory, database theory, and combinatorics. Research in descriptive complexity has amplified the close relationship between logic and computation, as evidenced by natural characterizations of all major complexity classes in terms of logical expressibility on finite models. Significant new advances in all the above areas have resulted from this approach.

The goal of this workshop is to provide a forum for communicating recent advances in descriptive complexity and to bring together researchers from all areas involved in the development of descriptive complexity.

Workshop on the Satisfiability Problem: Theory and Applications
Date: March 11-13, 1996
Organizers: Ding-Zhu Du, Jun Gu, Panos Pardalos
Email: dzd@cs.umn.edu, gu@enel.ucalgary.ca, pardalos@ufl.edu
Advisory Committee: Bob Johnson, David Johnson, Christos Papadimitriou, Paul Purdom, Benjamin Wah
Description: The satisfiability (SAT) problem is central in mathematical logic, computing theory, and many industrial application problems. There has been a strong relationship between the theory, algorithms, and the applications of the SAT problem. The main focus of this workshop is to bring together the best theorists, algorithmists, and practitioners working on the SAT problem and on the industrial applications involving the SAT problem, enhancing the interaction between the three research groups. This workshop will feature the application of theoretical/algorithmic results to practical problems as well as the presentation of practical problems for theoretical/algorithmic study. Major topics to be covered in the workshop include practical and industrial SAT problems and benchmarks, significant case studies and practical applications of SAT problem and SAT algorithms, new algorithms and improved techniques for satisfiability testing, specific data structures and implementation details of the SAT algorithms, and the theoretical study of the SAT problem and SAT algorithms.

As an important activity of the workshop, a set of SAT problem benchmarks derived from the practical industrial engineering applications will be provided for SAT algorithm benchmarking.

Workshop on Computational and Complexity Issues in Automated Verification
Date: March 25-29, 1996
Organizers: Bob Brayton, Allen Emerson, Joan Feigenbaum
Email: brayton@ic.eecs.berkeley.edu, emerson@cs.utexas.edu, jf@research.att.com
Description: The correctness of computer hardware and software is an area of growing theoretical interest as well as practical importance. It is now widely acknowledged that the best way to reason about program correctness hinges on two criteria: (i) the use of appropriate formalisms, such as temporal logic or automata, for rigorously specifying correct behavior; (ii) the use of mechanical reasoning algorithms, such as model checkers, to permit proofs of correctness to be constructed automatically that could not reasonably be constructed by hand owing to the intractable amount of tedious detail.

A principal limiting factor to automated verification is the computational complexity of various associated mechanical reasoning problems, which might be prohibitively high due to the combinatorial state explosion problem in various guises. The workshop will focus on such topics as the theoretical complexity as well as the practical efficiency of model checking algorithms and of testing satisfiability of logics, both in general and in applications-oriented special cases. Other methods for overcoming state explosion such as abstraction through the use of simulations and bisimulation relations are also important. Still other topics include the use of compositionality and modularity to simplify the construction of a correct program from correct constituent subprograms, program checking, testing and correcting, and program synthesis.

A portion of the workshop will be devoted to tools for verification and testing, evaluation of their strengths versus weaknesses, and reports on real experiences with industrial applications.

Workshop on Feasible Arithmetics and Length of Proofs
Date: April 21-23, 1996
Organizers: Paul Beame and Sam Buss
Email: beame@cs.washington.edu, sbuss@cs.ucsd.edu
Description: This workshop will cover two complementary approaches to the complexity of proving a mathematical fact, with emphasis on their connections to circuit complexity and computational complexity. Feasible theories of arithmetic are weak first- or second-order systems whose theorems correspond to problems in computational classes such as the levels of the polynomial time hierarchy or the NC hierarchy. The ``length of proofs'' approach, on the other hand, studies the growth rate (in number of symbols, number of lines, logical depth, etc.) of proofs of instances of some theorem within a fixed, quantifier-free proof system.

Proof complexity and feasible arithmetics are closely related to each other and to fundamental problems from circuit complexity and computa- tional complexity, such as the NP versus coNP problem. Over the last decade there has been significant progress in the study of these areas and many deep connections between them have been discovered. One example is the application of methods from circuit complexity lower bound proofs to obtain new lower bounds on proof complexity. Another example is the recent work on natural proofs, which has shown that if certain theories of bounded arithmetic can prove lower bounds in complexity theory, then certain levels of cryptographic security cannot be achieved.

The workshop will emphasize the interconnections among proof complexity, arithmetic complexity and computational complexity. This encompasses a broad range of topics of current interest, including Frege systems, bounded depth proof systems, cutting plane and Nullstellensatz proof systems, switching lemmas, recursion theoretic characterizations of complexity classes, bounded arithmetic and other feasible formal systems, cryptographic conjectures, interpolation theorems, independence results, interpretability and conservativity.

Workshop on Controllers for Manufacturing and Automation: Specification, Synthesis, and Verification Issues
Date: May 13-15, 1996
Organizers: Mohsen A. Jafari and Bud Mishra
Email: jafari@gandalf.rutgers.edu, mishra@anihccam.cs.nyu.edu
Description: This workshop focuses on the specification, synthesis, and verification of supervisory control of manufacturing and automation systems. Thus, it is intended to be a forum for discussion of the current state of the theory and practice as well as the future research directions surrounding the above issues. Because of the multi-disciplinary nature of the subject, the workshop includes talks from various disciplines and research communities (e.g., control theory, computer science, manufacturing, robotics, transportation and communication), where these issues have featured prominently. In addition to regular talks, we also plan to organize panel discussions, expository survey talks, and software demonstrations.

Regardless of the formal or informal methodology used for its specification and synthesis, the supervisory control of any manufacturing or automation system is eventually a computer software requiring a real (or almost real) time response for many of its functions. Thus, in principle, many of the issues to be discussed in the workshop are also applicable to more general software systems, including real time process control.

Workshop on Partial Order Methods in Verification (POMIV)
Date: July 24-26, 1996
Doron Peled, Gerard Holzmann, Vaughan Pratt
Email: doron@research.att.com, gerard@research.att.com, pratt@cs.stanford.edu
Description: Research in the last few decades on the connection between partial order semantics and interleaving semantics has resulted in a class of new verification techniques for distributed systems that may prove themselves to be of great practical value in routine industrial applications of formal verification techniques. Much of the new work in this area is being pursued by people from quite distinct fields, who rarely have an opportunity to meet and exchange ideas directly. These groups include, for instance, verification tool builders, logicians, semantic researchers, and process algebra specialists.

This workshop aims to bring the people from these different disciplines together. The discussion at the workshop will be focused on the following three main topics:

Workshop on Teaching Logic and Reasoning in an Illogical World
Date: July 25-26, 1996
Organizers: Susanna Epp, David Gries, Peter Henderson and Ann Yasuhara
Email: epp@condor.depaul.edu, gries@cs.cornell.edu, pbh@cs.sunysb.edu, yasuhara@cs.rutgers.edu
Description:

Logic and logical thinking are central to all disciplines and are critical in the mathematical and computer sciences. This symposium will explore the teaching of introductory logic and logical thinking, with a primary focus on the college level and a secondary focus on the high school level. The symposium will be interdisciplinary, emphasizing and contrasting approaches used in mathematics, computer science, natural sciences, and engineering.

The symposium seeks a sharing of ideas, rather than consensus, on how to teach logic, so that all participants gain an appreciation for the fundamental issues and ultimately are better able to motivate the importance of logic and to convey the foundations of logical reasoning to students. Topics of interest include, but are not limited to:

Pedagogical Approaches
Cognitive Models of Logical Reasoning
Empirical Studies
Exemplary Course Material
Innovative Approaches
Courseware for Teaching Logic
Federated Logic Conference - FLOC'96
Date: July 27 - August 3, 1996 (tentative)
FLOC'96 Conference Chair: Jon Riecke
Email: riecke@research.att.com
Description: As part of this Special year, DIMACS will host a Federated Logic Conference (FLOC'96). FLOC'96 will be modeled after the successful Federated Computer Research Conference (FCRC). The goal is to battle fragmentation of the technical community by bringing together synergetic conferences that apply logic to computer science. Participating in FLOC'96 are CADE (Conference on Automated Deduction), CAV (Conference on Computer-Aided Verification), LICS (IEEE Symp. on Logic in Computer Science), and RTA (Conference on Rewriting Techniques and Applications). The four conferences will span eight days, with only two-way parallelism at any given time. We will make special efforts to bring about interaction between the various conferences. The meeting will take place in late July, 1996, at Rutgers.
Workshop on SPIN96 -- 2nd Internatonal SPIN Verification Workshop Algorithms, Applications, Tool Use, Theory
Date: August 5, 1996
Organizers: Jean-Charles Gre'goire, Gerard J. Holzmann and Doron Peled
Email: gregoire@inrs-telecom.uquebec.ca, gerard@research.att.com, doron@research.att.com
Description: SPIN is a powerful reachability analysis tool designed for the verification of distributed systems. The tool was first made available publicly in 1991, and has quickly become a standard in both academia and in industry. In academia the tool is used for both teaching verification techniques, and to support research in, e.g., search algorithms, reduction methods, and tool construction. In industry the tool is used routinely on large scale verification problems. There are well over 2,000 installations of SPIN today, with active users in 30 different countries. For more info, see http://netlib.att.com/netlib/spin/whatispin.html

The first SPIN workshop was held in Montreal, Canada. The SPIN96 workshop will take place in New Jersey as part of the DIMACS Special Year on Logic and Algorithms. The new workshop will be part of a series of workshops on formal methods and verification. More information can be found at: http://dimacs.rutgers.edu/archive/

SPIN96 takes place following the LICS (logic in computer science), CADE (conf. on automated deduction) and CAV (computer aided verification) conferences, which will all be held at the same location in New Jersey this year. (See http://www.research.att.com/lics/floc/)

Demo sessions of extensions, restrictions, and variations of SPIN will be organized (or of any comparable tool that is suggested).

Keynote speaker: Moshe Y. Vardi, Rice University

IndexIndex of Special Year on Logic and Algorithms
DIMACS Homepage
Contacting the Center
Document last modified on October 19, 1998.