## CADE-19 in Miami28 July - 2 August 2003## In the sunshine ... On the beach |

Tony Cohn | |
---|---|

Dr Tony Cohn
is Professor of Automated Reasoning and Head of the
School of Computing at the University of Leeds. Tony's research
interests have always centred on knowledge representation and the
control of reasoning. For a number of years he worked on expressive
many sorted logics. His current major focus is on ontologies and
logics for reasoning about physical systems and calculi for
qualitative spatial and spatio-temporal reasoning in particular. The
RCC calculus is perhaps the best known example of the work of his
group at Leeds. Applications of this work include Geographical
Information Systems and Cognitive Vision. The work has received
support from a variety of sources including the UK funding council
EPSRC, the EU and industrial partners.
## Invited Talk: Reasoning about Qualitative Representations of Space and Time
In this talk I survey Qualitative Representations of Space and Time
which have formed an increasingly active area of Knowledge
Representation recently. Although most of the work has concerned
topology and mereology (theories of parthood), known collectively as
I will report on some of the complexity results known, and I will discuss some of the approaches to the usual tradeoff between expressiveness and tractability, including the use of special purpose logics and reasoning procedures, including composition tables, constraint based reasoning, and the use of intuititionistic and modal zero-order logics.
Spatial change is of great applicability in a variety of possible
application domains, for example in reasoning about high level
computer vision, or in geographic information systems. I will present
the notion of a | |

| |

Edmund Clarke | |

Dr Edmund Clarke
is a Professor of Electrical and Computer Engineering
and the FORE Systems Professor of Computer Science in the School of
Computer Science at Carnegie Mellon University. Dr. Clarke's
interests include software and hardware verification and automatic
theorem proving. In his Ph.D. thesis he proved that certain
programming language control structures did not have good Hoare
style proof systems. In 1981 he and his Ph.D. student Allen Emerson
first proposed the use of Model Checking as a verification technique
for finite state concurrent systems. His research group pioneered
the use of Model Checking for hardware verification. Symbolic Model
Checking using BDDs was also developed by his group. This important
technique was the subject of Kenneth McMillan's Ph.D. thesis, which
received an ACM Doctoral Dissertation Award. In addition, his
resarch group developed the first parallel resolution theorem prover
(Parthenon) and the first theorem prover to be based on a symbolic
computation system (Analytica).
## Invited Talk: SAT-based Counterexample Guided Abstraction Refinement in Model CheckingWe introduce a SAT based automatic abstraction refinement framework for model checking systems with several thousand state variables in the cone of influence of the specification. The abstract model is constructed by designating a large number of state variables as "invisible". In contrast to previous work where invisible variables were treated as free inputs we describe a computationally more advantageous approach in which the abstract transition relation is approximated by "pre-quantifying" invisible variables during image computation. The abstract counterexamples obtained from model-checking the abstract model are symbolically simulated on the concrete system using a state-of-the-art SAT checker. If no concrete counterexample is found, a subset of the invisible variables is reintroduced into the system and the process is repeated. The main contribution of this paper are two new algorithms for identifying the relevant variables to be reintroduced. These algorithms monitor the SAT checking phase in order to analyze the impact of individual variables. Our method is complete for safety properties AG p in the sense that - performance permitting - a property is either verified or disproved by a concrete counterexample. Experimental results are given to demonstrate the power of our method on real-world designs. | |

| |

Hélène Kirchner | |

Dr Hélène
Kirchner is a permanent researcher (Directeur de
Recherche) at CNRS. Since January 2001 she has been the Director of
LORIA and INRIA-Lorraine, a joint research center between CNRS,
INRIA, and Nancy Universities. In her Habilitation Thesis she
studied completion procedures for term rewriting systems modulo sets
of equations, and applications to automated deduction. As
post-doctoral fellow at Stanford University she contributed to the
design and implementation of the algebraic programming language
OBJ-3. Back in France her research interests then turned to
constraint solving, combinations of solvers, and theorem proving
with constraints, where she made several theoretical contributions.
The project team Protheo, which she led 1997-2000, has developed the
ELAN software, an environment for specifying and prototyping
deduction systems in a language based on rewrite rules controlled by
strategies, backed up by rewriting logic and rewriting calculus. Her
current research interests are the study of non-deterministic
rewriting and strategies, termination proof under strategies,
modelisation with rule-based languages, and the combination of proof
assistants with rewrite based systems.
## Invited Talk: Proof Search and Proof Check for Equational and Inductive TheoremsThis talk presents an on-going research project on theoretical and practical issues of combining rewriting based automated theorem proving and user-guided proof development, with the strong constraint of safe cooperation of both. In practice, we instantiate the theoretical study on the COQ proof assistant and the ELAN rewriting based system. A first approach of cooperation between COQ and ELAN is described, where COQ delegates equational proofs by rewriting to ELAN, builds a proof term while doing the proof. This proof term is then returned to COQ and checked. In the context of proof by structural induction performed by COQ, this technique is currently used in experiments for proving both the base case and the induction case by rewriting. However proofs by noetherian induction performed by rewriting are much more powerful than structural induction. A second approach, which is yet on-going work, is then presented. Based on the description at the proof theoretical level of proof by noetherian induction provided by the deduction modulo framework, we show how to use narrowing in order to perform proof search for an inductive proof by rewriting, and how to build a proof term that can be checked by COQ. In order to check the proof, additional proof obligations to justify the noetherian induction principle in COQ are also needed. The talks thus presents different ingredients (especially rewriting and inductive proof techniques, proof term construction in rewriting calculus, and deduction modulo) that can contribute to the design of a development framework for certified and modular software. | |

| |

Greg Nelson | |

Dr Greg Nelson received his Ph.D. in Computer Science from Stanford
University in 1980, where he worked under the supervision of Bob
Tarjan on program verification and algorithms for automatic theorem
proving. He received his B.A degree in Mathematics from Harvard
College in 1976. As an undergraduate at Harvard, he invented a
method of combining decision procedures for different logical
theories into a decision procedure for the combination of the
theories (often called the "Nelson-Oppen method") that has become
influential in the automatic theorem-proving community. He was a
member of the committee that designed the programming language
Modula-3, and was the author of the Juno constraint-based graphics
system at the Computer Science Laboratory of the Xerox Palo Alto
Research Center and one of the authors of its successor Juno-2. He
has taught computing at Princeton University, and is currently a
Principal Member of the Technical Staff at Hewlett-Packard Company's
Systems Research Center.
## Invited Talk: Reasoning About Quantifiers by Matching in the E-graphThe talk will describe the method used for reasoning about quantifiers in the Simplify theorem-prover, which is the reasoning engine inside the Extended Static Checkers built for Java and for Modula-3 at the DEC/Compaq/HP Systems Research Center. The essence of the method is pattern-based heuristic instantiation. The two main novelties are (1) because matching is performed in the E-graph instead of in an ordinary term DAG, the prover makes better use of equality information, and (2) two E-graph specific performance optimizations will be described, the "mod-time optimization" and the "pattern-elements optimization". |