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

- Organizer: Jim Lynch
- Speakers: Neil Immerman, Phokion Kolaitis, Jim Lynch
- Email: jlynch@sun.mcs.clarkson.edu
- Schedule: Press here

- Date: August, 1995
- Organizer: Toni Pitassi
- Speakers: Sam Buss, Toni Pitassi, Alasdair Urquhart
- Email: toni@cs.pitt.edu
- Schedule: Press here

- Date: October 22-25, 1995 -- DATE CHANGE
- Organizers: Rajeev Alur, Tom Henzinger
- Email: alur@research.att.com, tah@cs.cornell.edu

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.

- 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

- Date: January 14 - 17, 1996
- Organizers: Neil Immerman and Phokion Kolaitis
- Email: immerman@cs.umass.edu, kolaitis@cs.ucsc.edu

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.

- 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

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.

- 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

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.

- Date: April 21-23, 1996
- Organizers: Paul Beame and Sam Buss
- Email: beame@cs.washington.edu, sbuss@cs.ucsd.edu

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.

- Date: May 13-15, 1996
- Organizers: Mohsen A. Jafari and Bud Mishra
- Email: jafari@gandalf.rutgers.edu, mishra@anihccam.cs.nyu.edu

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.

- Date: July 24-26, 1996
- Doron Peled, Gerard Holzmann, Vaughan Pratt
- Email: doron@research.att.com, gerard@research.att.com, pratt@cs.stanford.edu

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:

- Experience with the application of verification methods and tools based on partial order semantics and partial order reduction techniques.
- Formal description techniques, logics and algebras, based on partial orders.
- Formal specification methods where partial order semantics are more natural than interleaving semantics.

- 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

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

- Date: July 27 - August 3, 1996 (tentative)
- FLOC'96 Conference Chair: Jon Riecke
- Email: riecke@research.att.com

- 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

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/

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

Index of Special Year on Logic and Algorithms

DIMACS Homepage

Contacting the Center

Document last modified on October 19, 1998.