Conference ricks::formal_verification

                             Workshop on

               Automated Theorem Proving and Mathematics.
               =========================================

                          in Connection with

                  Conference on Automated Deduction
                              (CADE-14)

                         Townsville, Australia
                         Sunday, July 13,  1997

      http://www-theory.dcs.st-and.ac.uk/~um/cade14-workshop.html
      http://www.cs.jcu.edu.au/~cade-14/



The aim of this workshop is to draw together the community working on
applying techniques of automated reasoning to mathematical problems.
McCune's recent solution of the Robbins Algebra problem, and earlier work
of Slaney and others,  has highlighted the success that automated reasoning
tools can have tackling unsolved problems in certain areas of mathematics:
the Mizar achievement has shown what can be achieved with sustained long
term development: new hybrid approaches combining theorem provers with, for
example, computer algebra systems, show promise.

Invited participants include Jacques Calmet, John Harrison, Bill McCune, R.
Padmanabhan and John Slaney.

The workshop will be a mix of  presentations and discussion panels to
encourage lively informal debate on matters of interest and possible future
directions.

Intending participants are invited to send a one page position paper BEFORE
1 JUNE by email to Duncan Shand, [email protected], for distribution
at the meeting. We will use these abstracts to plan the composition of the
panels. No other publication is planned.

Participants should register via the CADE conference: see
http://www.cs.jcu.edu.au/~cade-14/
or contact [email protected]


Organisers
----------

Ursula Martin ([email protected])
University of St Andrews

John Slaney ([email protected])
Australian National University

Call for Papers
User Interfaces for Theorem Provers 1997

INRIA Sophia-Antipolis, Monday and Tuesday, 1-2nd September 1997

This page: http://www.inria.fr/croap/events/uitp97.html

The Workshop

This international workshop provides a forum for the exchange of ideas and
research on the analysis and design of user interfaces for theorem proving
assistants. In particular it facilitates cross-fertilisation between the
fields of human-computer interaction (HCI) and mechanised theorem proving.

The series was started in recognition of the fact that the difficulty in
using powerful theorem proving software frequently lies with a poor user
interface. There are gaps between the knowledge required by designers of
such interfaces and present state of the art in general interface design
technology. Effective solutions require the collaboration of HCI
practitioners and the authors and users of existing theorem proving
software.

In 1995 the first workshop in this series was hosted at the Department of
Computer Science at the University of Glasgow. A brief report was published
in FACS Europe.

In 1996 the second workshop was hosted at the University of York.
Electronic proceedings for this workshop are now available at the following
address: http://www.cs.york.ac.uk/~nam/uitp/proceedings.html

There is a mailing list for disseminating information about the workshop
series and discussion relevant to user interfaces for theorem provers. To
subscribe, email a request to [email protected]. Messages can be
posted to the list at [email protected]. All information about the 1997
workshop will be posted there.

Topics of Interest

The theme of the workshop is the study of interfaces for theorem proving
assistants and all pertinent submissions will be considered. Papers on the
following topics are especially welcome.

   * Analysis of interfaces
   * Case studies of tools
   * Interaction for proof planning
   * Reading and representation of mathematics/logic
   * Interaction for reuse (of theorems, etc.)
   * Studies of reasoning
   * Interface useability studies

Submissions

Papers may be up to 8 pages in length. In addition, system demonstrations
are invited. A cover sheet displaying the author's name, email and postal
addresses, the title and abstract of the paper and whether or not a
demonstration will be on offer, should be included.

Submissions should either be sent electronically, with the cover sheet as
the body of an email and the paper as a postscript enclosure, to

     [email protected]

or as four paper copies to

     Yves Bertot
     UITP '97
     INRIA Sophia Antipolis,
     2004, Route des Lucioles, B.P. 93,
     06902 Sophia Antipolis Cedex,
     FRANCE

The call for papers is also available as postscript.

Dates

 Submissions deadline        7th April 1997
 Notification of acceptance  16th June 1997
 Finished papers             15th July 1997
 Intention to register       15th July 1997
 Workshop                    1-2 September 1997

Programme Committee

   * Stuart Aitken
   * Roland Backhouse
   * David Benion
   * Yves Bertot
   * Richard Bornat
   * Masami Hagiya
   * Xiaorong Huang
   * Gilles Kahn
   * Helen Lowe
   * Tom Melham
   * Nick Merriam
   * Laurent Th=E9ry

Location

The workshop will be held at INRIA Sophia Antipolis in the south of France.
This research center is located near Antibes, very close to the Nice
airport.

Organiser

Yves Bertot

          CALL FOR PARTICIPATION
          CADE-14 WORKSHOP ON 
          STRATEGIES IN AUTOMATED DEDUCTION
          =================================

          July 13, 1997
          Townsville, Australia
          http://www.loria.fr/~gramlich/cade14-ws-strategies.html



MOTIVATIONS

The concept of strategy allows describing and guiding 
computations and deductions in automated theorem provers, 
proof checkers, logical frameworks.

Strategies are used for various purposes, e.g.:
- proof search in  theorem proving,
- combination of different proof techniques and computation paradigms, 
- program transformation,
- development of heuristics for playing games and finding proofs.

Deterministic computations or inference rule based deductions are not
sufficient to capture every computation or proof development.  A
mechanism is needed for instance to formalise the search for different
solutions, the check of context conditions, the request for user input
to instantiate variables, the processing of subgoals in a particular
order.  Strategies are used to guide application of rules, but may
also involve iteration, case analysis, deterministic and
non-deterministic choices. One may want to program strategies, to
transform them, to prove some property on the computations or the
proofs that they describe.


AIMS

The workshop aims at gathering different experiences on 
the use of strategies, under various terminology
(tactic, tactical, method, heuristic, proof planning...),
and in various application domains
(first-order, higher-order, inductive theorem proving,
program transformation, operational semantics...).
Based on these experiments, we will address and discuss 
several points:

- Strategy languages:
Which basic constructs are needed? 
Expressiveness versus efficiency?
Meta-language versus reflexivity?
Higher-order versus first-order syntax?

- Computational models for proof systems with strategies:
Architecture, modularity of such systems?
How to deal with user-interaction, input-output?

- Verification of strategies:
Which properties are required for strategies?
Fairness, (partial) completeness, termination, etc.?
How to ensure and/or check them?


SUBMISSIONS

Participants interested in presenting their work are invited to send 
an extended abstract (5-10 pages) by e-mail
submission of a postscript file to the organizers
([email protected]) before April 21, 1997.

Participants interested in attending the workshop without giving 
a presentation should send a position paper (1-2 pages) 
mentioning interest in one or several aspects of the topics.

Additional information will be available through
http://www.loria.fr/~gramlich/cade14-ws-strategies.html

Attendance is by invitation only. Workshop registration is to be done
as part of registration of CADE-14. The early registration deadline
for CADE-14 is May 12, 1997.


IMPORTANT DATES 

Deadline for submissions: April 21, 1997 
                          position paper or abstract
                          by e-mail 
Notification of acceptance: May 5,1997
Postcript version for proceedings: June 6,1997
Workshop: July 13, 1997


ORGANIZERS          

Bernhard Gramlich
Helene Kirchner
CRIN & INRIA-Lorraine (France)
e-mail: [email protected]
Fax:  33 3 83 27 83 19

*********************************************************************
               COMPUTER - AIDED VERIFICATION (CAV 97)
                          June 22-25, 1997

                          Dan Carmel Hotel
                            Haifa, Israel
                        
                           FINAL PROGRAM
                               
                                and

           REGISTRATION, ACCOMMODATION and TOUR RESERVATION
*********************************************************************


CAV '97 is the ninth in a series dedicated to the advancement of the
theory and practice of computer-assisted formal analysis methods for 
software and hardware systems.
The conference covers the spectrum from theoretical results to
concrete applications, with an emphasis on verification tools and 
the algorithms and techniques that are needed for their implementation. 

The contributed presentations of CAV '97 include 34 regular papers and
12 short presentations on tools. The program also includes 3 invited
lectures and a dinner speech in honor of the recipient of the 
Turing award, Professor Amir Pnueli.

Half a day is dedicated to invited talks by representatives from
industry. The industrial part concludes with a panel on 
"Future Trends in Industrial Computer-Aided Verification".

The conference will be opened on Saturday night, June 21, 1997
with a get together reception at the Dan Carmel Hotel.
The technical program will start on Sunday morning and will
proceed until Wednesday, June 25, late afternoon.

For updated information see the CAV'97 home page at:
http://www.cs.technion.ac.il/~cav97/cav97.html


CONFERENCE PROGRAM
------------------
This is a preliminary version of the program. Changes may be made.

Saturday 21.6.97       
----------------

18:00 - 21:00		Registration 
21:00 - 23:00		Reception

Sunday	 22.6.97
----------------

09:00 - 09:30
FE Marschner,		Practical challenges for industrial
COMPASS Design		formal verification tools
Automation

09:30 - 10:00
RB Hughes,		Formal verification of digital systems, from
Abstract Hardware	ASICs to HW/SW codesign - a pragmatic approach

10:00 - 10:30		
A Boralv,		The Industrial Success of Verification Tools 
Logikkonsult NP		Based on Stalmarck's Method

10:30 - 11:00		Coffee Break

11:00 - 11:30
M Rowe,			Formal Verification - Applications 
Chrysalis Symbolic	& Case Studies
Design

11:30 - 12:45		Panel on 
"Future Trends in Industrial Computer-Aided Verification"
EA Emerson, UT at Austin - moderator, B Brennan, Intel, 
T Henzinger, UC Berkeley, RP Kurshan, Bell Labs, C Logan, IBM, 
N Shankar, SRI, Y Wolfstal, IBM


12:45 - 14:00		Lunch

14:00 - 14:25	
A Pardo,		Automatic abstraction techniques for
GD Hachtel,		propositional mu-calculus model checking
Uni. Colorado

14:25 - 14:50	
KL McMillan,		A compositional rule for hardware design 
Cadence Berkeley Labs.	refinement

14:50 - 15:15
O Kupferman, UC Berkeley
MY Vardi, Rice Uni.	Module checking revisited

15:15 - 15:40
R Kaivola,		Using compositional preorders in the
Uni. Helsinki		verification of sliding window protocol

15:40 - 16:05		Coffee Break

16:05 - 16:30		
D Cyrluk, SRI Internat.	An efficient decision procedure for the theory
O Moller, H Reuss,	of fixed-sized bit-vectors
Uni. Ulm

16:30 - 16:55
S Graf, H Saidi		Construction of abstract state graphs with
Verimag			PVS

16:55 - 17:10	
H Saidi, Verimag        The Invariant Checker: Automated deductive
                        verification of reactive systems

17:10 - 17:25
B Grahlmann		The PEP tool
Hildesheim Uni.


		-------------------------------


Monday 23.6.97
--------------

08:30 - 09:30		Invited Lecture
GJ Powers, CMU		Verification of a chemical process leak test
              		procedure                 

09:30 - 09:55	
G Kamhi, O Weissberg, 	Automatic datapath extraction for efficient 
L Fix, Z Binyamini,	usage of HDD
Z Shtadler, Intel 

09:55 - 10:20
N Klarlund, AT&T Labs.	An n log n algorithm for online BDD refinement

10:20 - 10:45		Coffee Break

10:45 - 11:10
C Baier, Uni Mannheim	Weak bisimulation for fully probabilistic 
H Hermanns, 		processes
Uni Erlangen

11:10 - 11:35
D Bolignano		Towards a mechanization of cryptographic
GIE, Dyade		protocol verification

11:35 - 12:00
YS Ramakrishna, 	Efficient model checking using tabled
CR Ramakrishnan,	resolution
IV Ramakrishnan, 
SA Smolka, T Swift, 
DS Warren, SUNY Brook    

12:00 - 12:15		
N Lindenstrauss, 	TermiLog: A system for checking termination
Y Sagiv, A Serebrenik,	of queries to logic programs
Hebrew Uni

12:15  - 12:30	
P Kelb, T Margaria,     MOSEL: A sound and efficient tool for M2L(Str)
M Mendler, C Gsottberger,
Passau Uni.

12:30 - 14:00		Lunch

14:00 - 14:25		
K Fisler, Rice Uni.	Containment of regular languages in
			non-regular timing diagram languages is
			decidable

14:25 - 14:50
B Boigelot, L Bronne,	An improved reachability analysis method for 
S Rassart, Uni. Liege	strongly linear hybrid systems

14:50 - 15:15
M Bozga, O Maler, 	Some progress in the symbolic verification
S Yovine, Verimag 	of timed automata
A Pnueli, Weizmann Inst.

15:15 - 15:40
S Tasiran, RK Brayton,	STARI: A case study in compositional and 
UC Berkeley   		hierarchical timing verification

15:40 - 16:05		Coffee Break

16:05 - 16:30
A Cimatti,		A provably correct embedded verifier for the 
F Giunchiglia,		certification of safety critical software
P Pecchiari, IRST,
B Pietra, J Profeta,
D Romano, Ansalso 
Trasporti Spa,
P Traverso, IRST
B Yu, Ansalso Trasporti Spa,

16:30 - 16:55
G Barrett, A McIssac,	Model checking in a microprocessor design
SGS-Thomson		project
Microelectronics

16:55 - 17:10
S Campos, E Clarke,	The Verus Tool: A quantitative approach to
M Minea, CMU		the formal verification of real-time systems

17:10 - 17:25
KG Larsen, Aalborg Uni.	UPPAAL - Status & developments              
P Pettersson, W Yi,	
Uppsala Uni.

17:25 - 17:40	
TA Henzinger,		HYTECH: A model checker for hybrid systems
UC Berkeley,   
P-H Ho, Intel,
H Wong-Toi, 
Cadence Berkeley Labs.

		-----------------------------


Tuesday 24.6.97
---------------

08:30 - 09:30		Invited Lecture
D Harel, Weizmann Inst.	Some thoughts on statecharts, 13 years later

09:30 - 09:55	
V Gyuris, AP Sistla, 	On-the-fly model checking under fairness that
Uni. Illinois at	exploits symmetry
Chicago

09:55 - 10:20
M Pandey, RE Bryant,	Exploiting symmetry when verifying transistor-
CMU			level circuits by symbolic trajectory
			evaluation

10:20 - 10:45		Coffee Break

10:45 : 11:10
U Stern, DL Dill,	Parallelizing the Murphi verifier
Stanford Uni.

11:10 - 11:35
RH Hardin, RP Kurshan,	A new heuristic for bad cycle detection 
Bell Labs.,		using BDDs
SK Shukla, Uni. NY,
MY Vardi, Rice Uni.

11:35 - 12:00
I Beer, S Ben-David,	Efficient detection of vacuity in ACTL
C Eisner, Y Rodeh, IBM	formulas

12:00 - 12:25
N Immerman,		Model checking and transitive closure logic
Uni Massachusetts
MY Vardi, Rice Uni.

12:25 - 12:40
AP Sistla, L Miliades,	SMC: A symmetry based model checker for
V Gyuris, Uni.         	verification of liveness properties
Illinois at Chicago

12:40 - 12:55
A Biere,                mucke - efficient mu-calculus model checking
Uni Karlsruhe

12:55 - 14:15 		Lunch

14:30 - 		Excursion and Banquet	
Dinner speech in honor of  Amir Pnueli, the Turing Award recipient,
by
David Harel, 		Amir Pnueli: A Man for all (the Right) Reasons
Weizmann Inst.

		-------------------------------

Wednesday 25.6.97
-----------------

08:30 - 09:30		Invited Lecture
G Berry, Ecole de 	Boolean and 2-adic numbers based techniques
Mines de Paris     	for verifying synchronous designs

09:30 - 09:55
G Cece, A Finkel,	Programs with quasi-stable channels are 
LSV, ENS		effectively recognizable

09:55 - 10:20
W Chan, R Anderson, 	Combining constraint solving and symbolic
P Beame, D Notkin, 	model checking for a class of systems with
Uni. Washington		non-linear constraints

10:20 - 10:45		Coffee Break

10:45 - 11:10
I Kokkarinen, 		Relaxed visibility enhances partial order
Tampere Uni,		reduction
D Peled, Bell Labs., 
A Valmari, Tampere Uni.

11:10 - 11:35
R Alur, RK Brayton, 	Partial order reduction in symbolic state
TA Henzinger,          	space exploration
S Qadeer, SK Rajamani, 
UC Berkeley   

11:35 - 12:00
S Melzer, S. Roemer,	Deadlock checking using net unfoldings 
Technical Uni. Munich

12:00 - 12:15
K Varpaaniemi, 		prod 3.2 - An advanced tool for efficient
K Heljanko, J Lilius	reachability analysis
Helsinki Uni.

12:15 - 12:30
P Godefroid,           	VeriSoft: A tool for the automatic analysis of
Bell Labs.		concurrent reactive software

12:30 - 14:00           Lunch

14:00 - 14:25
J Sawada, Uni Texas,	Trace table based approach for pipelined
WA Hunt,		microprocessor verification    
Computational Logic Inc.

14:25 - 14:50
J Yuan, Motorola Inc.	On combining formal and informal verification
J Shen, J Abraham, 
A Aziz, Uni. Texas

14:50 - 15:15
M Velev, RE Bryant,	Efficient modeling of memory arrays in  
A Jain, CMU		symbolic simulation

15:15 - 15:30
I Beer, S Ben-David,	RuleBase: Model checking at IBM
C Eisner, D Geist,
L Gluhovsky,
T Heyman, A Landver, 
P Paanah, Y Rodeh, G Ronin,
Y Wolfstahl, IBM 

15:30 - 15:55           Coffee Break

15:55 - 16:20
T Bultan, R Gerber,	Symbolic model checking of infinite state
W Pugh, Uni. Maryland	systems using Presburger arithmetic

16:20 - 16:45
AP Sistla,		Parametrized verification of linear 
Uni. Illinois at 	networks using automata as invariants
Chicago

16:45 - 17:10
Y Kesten, Intel		Symbolic model checking with rich 
O Maler, Verimag	assertional languages
M Marcus, A Pnueli, 
E Shahar, Weizmann Inst.

               -------------------------




LOCATION:
- --------
The conference will take place in the Dan Carmel Hotel, Haifa, Israel.

GETTING THERE:
- --------------
You will arrive at the Ben-Gurion International Airport which is
situated near Tel-Aviv.
 
As you leave the terminal building you will see a taxi stand with the
sign "AMAL". You may share a taxi with about six other people and this
will cost approximately $15. 
The driver will take you to your hotel. This trip may take
approximately one and a half hours.

If you wish to take a taxi by yourself, it may cost between $50-$60. 

Special transportation from Ben Gurion Airport to your hotel can be 
reserved on the attached  Registration & Reservation Form. Participants 
will be met upon arrival and assisted through baggage claim and customs.
Price per person: $ 57.



WEATHER:
- --------
The weather in Haifa in June is sunny and warm. Temperatures range
between 19C - 26C  (69F - 78F). Humidity is moderate and there 
is no rain. Light clothing, informal dress  and swimming suit
are recommended.

VISA:
- ----
Please note that citizens of most countries require a visa to enter
Israel. Please make your arrangements early.

CURRENCY:
- ---------
Israel's currency is the New Israeli Shekel (NIS).
The average exchange rate (as of March 7, 1997) is
1 US dollar = 3.37 NIS.
 
TOURS:
--------
`Unitours' is the official travel agent for CAV 97 and will be offering 
reduced rates especially for conference participants. They will extend 
their services for special hotel arrangements, tours and car
rentals as well as pre- and post- conference requests.
               
Pre- and Post- Conference Tours:
---------------------------------- 
 * Tour A -  Acre, Safed, Golan Heights, one day tour, June 21
   Price per person: $ 58

 * Tour B - Jerusalem 2 days/2 nights, June 26-28
   Day 1: Caesarea, Tel Aviv, Jaffa. Dinner and Overnight: Jerusalem
   Day 2: Jerusalem Old and New. Dinner and Overnight: Jerusalem
   Day 3: Check out of hotel or departure for tour C.
   Prices:  Per person in a double room: $ 258. Single room: $ 339
   Rates include: 2 days of guided tours, 2 nights accommodation on 
   breakfast and dinner basis in a first class hotel in Jerusalem

 * Tour C - Massada and Dead Sea, 1 day/1 night, June 28-29
   Day 1: Tour of Massada and Dead Sea. Dinner and Overnight: Jerusalem
   Day 2: Check out of hotel
   Prices:  Per person in a double room: $ 113. Single room: $ 159.

All tours will operate with a minimum of 15 participants.



*********************************************************************
               
                 CAV'97 - REGISTRATION and ACCOMMODATION
                               
*********************************************************************


Dear Participant!!

Below are the Registration and Accommodation Forms for CAV '97.

Please fill out the forms in BLOCK LETTERS and return them 
by e-mail or by airmail to:

The Secretariat - CAV 97
P.O. Box 3190, Tel Aviv 61031, Israel
Tel: 972-3-5209999   Fax: 972-3-5239099  
E-mail: [email protected]


- ----------------------------CUT  HERE -----------------------------
 
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
CONFERENCE REGISTRATION FORM                          CAV '97
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++


PARTICIPANTS:
 
Name : ........................................................
       (Surname)                        (First Name)
 
Title: .......................................................
 
Institution: ..................................................
 
Mailing Address: [  ]Institution [  ]Residence ................
 
...............................................................
 
        City: ................
 
        State: .....................Country: ..................
 
        Zip Code: ............
 
        e-mail:...........................
 
 
	Telephone: .......................
 
        Fax: .............................
 
 
ACCOMPANYING PERSONS:
 
        ....................................................
       (Surname)                         (First Name)
 
        ....................................................
       (Surname)                         (First Name)
 
REGISTRATION FEE: (in US Dollars)

                           till may 21, 1997     after May 22, 1997

[  ] Participant                  350                    390
[  ] Student                      130                    150
[  ] Accompanying Person          120                    120


Fees for participants include:
reception, lunches and coffee breaks, banquet and book of
proceedings.

Fees for students include:
reception, coffee breaks and book of proceedings.

Fees for accompanying persons include:
all social events as listed above and a one day tour.

 
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
ACCOMMODATION FORM                                     CAV '97
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 
 
Name : ........................................................
       (Surname)                        (First Name)
 
Mailing Address: ..............................................
 
...............................................................
 
City ................. Code ............. Country .............
 
Telephone ..................... Fax ...........................
 
Please reserve my hotel accommodation:
 
Single occupancy                Double occupancy

Dan Carmel* [  ] US$ 118         [  ] US$ 146 sharing with ...........
Shulamit ** [  ] US$  61         [  ] US$ 76 sharing with ............

The above prices are per night. The prices include:
an Israeli buffet breakfast and service charges.

*  Conference venue
** The hotel is located 15 min. drive from the conference venue.
   The number of rooms is limited. Rooms are on a  first come first
   serve basis.

Check in on  .................  Check out on ...................

No. of nights ................

Must be accompanied by a deposit of US$ 150  per room.
 
     ----------------------------------------------------------

CANCELATION POLICY OF ACCOMMODATION
Notification must be:
Postmarked 45 days or more prior to arrival - refund of deposit
less US$ 30 bank charges.
Postmarked 45 days or less prior to arrival - refund of deposit
less one night accommodation.

CANCELATION POLICY OF REGISTRATION
Postmarked 21 days prior to conference: refund less US$ 30 bank charges.
Thereafter - no refund will be made.

          -----------------------------------------

TOURS  - 
Please reserve the following tour/s: (must be accompanied by a 
deposit of US$ 58  per tour, per person)
    Tour A (Galilee)   No. of Seats_____ 

    Tour B (Jerusalem)   No. of Seats_____

    Tour C (Massada)    No. of Seats_____

TRANSFER
Please reserve a sharing transfer airport/hotel at US$ 57 per person.
No. of seats _________

PAYMENT
- -------
I enclose herewith payment of US$_________________ as follows:

US$ ______________________ for registration

US$ ______________________ for hotel/tours/transfer

MODE OF PAYMENT

(1) I enclose herewith US$_______________(or equivalent) payable to: 

    CAV/UNITOURS.
    Check  No. ________________________Bank_______________

(2) Enclosed is a copy of my bank transfer
 of US$_______________     payable to 

CAV/UNITOURS, 
Acc. No. 893/403575/60
Bank Leumi Le Israel, 
Trumpeldor Branch  (807), 
Tel Aviv, Israel    

(3) Credit Card Payment:
Please charge the amount of US$____________________to my credit card:

[  ] American Express    
[  ] Visa   
[  ] Master Card 
[  ] Diners Club

Credit card number___________________________Expiration date_________

Signature____________________________       Date____________________

                                   CADE-14

          The 14th International Conference on Automated Deduction
                  July 13-17, 1997, Townsville, Australia

 *******************  EARLY REGISTRATION CLOSES ON 12 MAY  ********************

                                          CALL FOR ATTENDANCE

 Program Committee           CADE  is  the  major  forum  for  presentation  of
 L. Bachmair (Stony Brook)   research  in all aspects  of automated  deduction.
 H. Comon (Orsay)            Logics of interest  include  propositional,  first
 W. Farmer (Bedford)         order,   equational,  higher   order,   classical,
 M. Fujita (Tokyo)           intuitionistic,    constructive,   type    theory,
 H. Ganzinger (Saarbruecken) nonstandard, and meta-logics.  Methods of interest
 F. Giunchiglia (Trento)     include resolution,  paramodulation,  unification,
 J. Harrison (Turku)         term rewriting,  tableaux,  constraints,  decision
 R. Hasegawa (Kyushu)        procedures, induction,  interactive  systems,  and
 S. Hoelldobler (Dresden)    frameworks.   Applications  of  interest   include
 J. Hsiang (Taipei)          hardware   and   software   development,   systems
 D. Kapur (Albany)           verification,  artificial intelligence, logic, set
 C. Kirchner (Nancy)         theory, mathematics, applicative programming,  and
 C. Kreitz (Cornell)         logic  programming.  Special  topics  of  interest
 A. Leitsch (Vienna)         include    proof    translation,    human-computer
 R. Letz (Munich)            interfaces,  distributed   deduction,  and  search
 E. Lusk (Argonne)           heuristics.
 U. Martin (St. Andrews)
 D. McAllester (Murray Hill) CADE-14 will  be held from 13th to 17th July 1997,
 W. McCune (Argonne)         at the Sheraton Breakwater  Hotel,  in Townsville,
 L. Paulson (Cambridge)      North   Queensland,   Australia    (i.e.,  in  the
 F. Pfenning (Pittsburgh)    sunshine,  near  the   Great  Barrier  Reef).  The
 M. Rusinowitch (Nancy)      conference  will  be hosted  by the Department  of
 J. Schumann (Munich)        Computer  Science  at  James  Cook  University  of
 N. Shankar (Menlo Park)     North Queensland. CADE-14 features:
 J. Slaney (Canberra)
 M. Stickel (Menlo Park)       + Six full day workshops (13th July)
 G. Sutcliffe (Townsville)     + Four half day tutorials (13th July)
 T. Tammet (Goeteborg)         + Twenty five research papers (14th-17th July)
 A. Voronkov (Uppsala)         + Seventeen system descriptions (14th-17th July)
 L. Wallen (Oxford)            + An ATP system competition (16th July)
 C. Walther (Darmstadt)        + A banquet on Magnetic Island (16th July)
 D. Wang (Grenoble)            + An   excursion  to  the  Great   Barrier  Reef
 H. Zhang (Iowa City)            (18th July)

                             You are invited to attend CADE-14,  to participate
                             in  the  high quality  technical program,  and  to
                             enjoy some great social events.

                       Information and Registration

 Full details about CADE-14 and an electronic registration form are on the WWW:

                    http://www.cs.jcu.edu.au/~cade-14/

 Alternatively, send us email ([email protected]) or a FAX (+61 77 215515),
 and all the information will be sent to you.  Note: No hardcopy information or
 registration forms will be distributed unless explicitly requested.

                Early registration deadline: May 12, 1997

      Program Chair:                    Local Arrangements Chair:

      William McCune                    Geoff Sutcliffe
      Argonne National Laboratory       James Cook University
      Phone: +1 630 252 3065            Phone: +61 77 815085
      FAX: +1 630 252 5986              FAX: +61 77 814029
      E-mail: [email protected]  E-mail: [email protected]

-------------------------------------------------------------------------------

                      CADE-14 Advance Program Summary

Workshops
+ Automated Induction Theorem Proving
+ Strategies in Automated Deduction
+ Automated Theorem Proving in Software Engineering
+ Automated Theorem Proving and Mathematics
+ Connectionist Systems for Knowledge Representation and Deduction
+ AI Methods in Theorem Proving

Tutorials
+ Learning from Previous Proof Experience
+ Deduction Methods Based on Boolean Rings
+ Term Indexing in Automated Reasoning,  Databases and  Declarative Programming
  Languages
+ Higher Order Equational Logic

Invited Lectures
+ Professor Wu Wen-Tsun, Academia Sinica, Beijing, China
+ Professor Moshe Vardi, Rice University, Houston, USA

Research Papers
+ Decidable Call by Need Computations in Term Rewriting.
  Irene Durand, Aart Middeldorp
+ A New Approach for  Combining Decision Procedures for the  Word Problem,  and
  Its Connection to the Nelson-Oppen Combination Method.
  Franz Baader, Cesare Tinelli
+ On Equality Up-to Constraints over Finite Trees, Context Unification and One-
  Step Rewriting.
  Joachim Niehren, Manfred Pinkal, Peter Ruhrberg
+ A Practical Symbolic  Algorithm for the Inverse Kinematics of 6R Manipulators
  with Simple Geometry.
  Lu Yang, Hongguang Fu, Zhenbing Zeng
+ Automatic Verification of Cryptographic Protocols with SETHEO.
  Johann Schumann
+ A Practical Integration of First-Order Reasoning and Decision Procedures.
  Nikolaj S. Bjorner, Mark E. Stickel and Tomas E. Uribe
+ Some Pitfalls of LK-to-LJ Transformations and How to Avoid Them.
  Uwe Egly
+ Deciding Intuitionistic Propositional  Logic via  Translation into  Classical
  Logic.
  Daniel Korn, Christoph Kreitz
+ Lemma Matching for a PTTP-based Top-down Theorem Prover.
  Koji Iwanuma
+ Exact  Knowledge Compilation in  Predicate Calculus:  the Partial Achievement
  Case.
  Olivier Roussel, Philippe Mathieu
+ Non-Horn Magic Sets to  Incorporate Top-down Inference into Bottom-up Theorem
  Proving.
  Ryuzo Hasegawa, Katsumi Inoue, Yoshihiko Ohta and Miyuki Koshimura
+ Connection-Based Proof Construction in Linear Logic.
  Christoph Kreitz, Heiko Mantel, Jens Otten, Stephan Schmitt
+ Resource-distribution via Boolean Constraints.
  James Harland, David Pym
+ Constructing a Normal Form for Property Theory.
  Mary Cryan, Allan Ramsay
+ Using a Generalisation Critic to Find Bisimulations for Coinductive Proofs.
  Louise Dennis, Alan Bundy, Ian Green
+ A Colored Version of the lambda-Calculus.
  Dieter Hutter, Michael Kohlhase
+ A Practical  Implementation of  Simple Consequence Relations  Using Inductive
  Definitions.
  Sean Matthews
+ Soft Typing for Ordered Resolution.
  Harald Ganzinger, Christoph Meyer, Christoph Weidenbach
+ A Classification of Non-Liftable Orders for Resolution.
  Hans de Nivelle
+ Hybrid Interactive Theorem Proving using Nuprl and HOL.
  Amy P. Felty, Douglas J. Howe
+ Proof Tactics for a Theory of State Machines in a Graphical Environment.
  Katherine A. Eastaughffe, Maris A. Ozols, Tony Cant
+ RALL: Machine-supported Proofs for Relation Algebra.
  David von Oheimb and Thomas F. Gritzner
+ Evolving Combinators.
  Matthias Fuchs
+ Partial Matching for Analogy Discovery in Proofs and Counter-examples.
  Gilles Defourneaux, Nicolas Peltier
+ DiaLog: A System for Dialogue Logic.
  Jurgen Ehrensberger, Claus Zinn

System Descriptions
+ Peers-mcd,  CODE, SETHEO, KIV,  SATO, Dedam,  ILF, ILF-SETHEO, 3CNF,  MINLOG, 
  PLAGIATOR, Nuprl-Light, OMEGA, XIsabelle, Snarks, XBarnacle, Jape.

		 The 1997 International Conference on
		Theorem Proving in Higher Order Logics

			Call for Participation


        ************************************************************
        *                                                          *
        *  If you have Web access, all the following information   *
        *     and more is available in a nicer format from:        *
        *                                                          *
        *   http://cm.bell-labs.com/who/elsa/tphol/tphol97.html    *
        *                                                          *
        ************************************************************

The 1997 International Conference on Theorem Proving in Higher Order
Logics will be the tenth conference in a series dating back to
1988. The conference will be held on 19-22 August 1997 (Tuesday to
Friday) at Bell Labs in Murray Hill, NJ, USA. The conference will be a
venue for presentations on the following topics, among others:
advances in interactive theorem proving, proof automation and decision
procedures, applications of mechanized theorem proving, comparison
between different theorem proving approaches, exploiting external
tools within theorem provers and incorporating theorem provers into
larger systems.

Previous conferences have been at Cambridge (UK), Arhus, Davis,
Leuven, Vancouver, Malta, Salt Lake City, and Turku. This conference
is being jointly organized by Bell Labs, and the Department of
Computer and Information Science at the University of Pennsylvania.

If you require any further information, please contact the organizing
committee chair via email at

		     [email protected]

or via physical mail at


                     Elsa L. Gunter
                     600 Mountain Ave, Rm # 2A432
                     Bell Laboratories
                     Lucent Technologies
                     Murray Hill, NJ 07974-0636
                     U.S.A.




  ============================================================================
			Conference Information
REGISTRATION

The fee for early registration, on or before Friday 20 June is
US$250.00 for regular participants, and US$125.00 for students.  After
that date, the registration will be US$300.00 for regular
participants, and US$165.00 for students.  All payments must be in US
currency and must accompany the registration form.  Registration
includes the conference participation, a copy of the proceedings,
coffee breaks, reception, conference excursion and banquet.  Hotel
accommodations and meals are separate.  You can register via the
Web; see:

  http://cm.bell-labs.com/who/elsa/tphol/webform.html

Alternatively, fill in the form at the end, and either:

 * Email it to "[email protected]"

 * Fax it to Elsa Gunter at +908 582 5857

 * Send it by mail to Elsa Gunter (see the address above).



ACCOMMODATIONS

A block of rooms has been booked at two hotels in the area near Bell
Labs: the Murray Hill Inn and the Grand Summit Hotel.  The Murray Hill
Inn is cheaper and closer (a 15 minute walk uphill to Bell Labs), but
the number of rooms is limited to 35 (possibly more will be available
later).  The Grand Summit Hotel includes breakfast, a shuttle from and
to Newark International Airport, and a shuttle to and from Bell Labs.
Breakfast may also be had in the cafeteria at Bell Labs.  There is a
public bus that stops at the train stations near each of the hotels
which will take you to Bell Labs.  Other hotels in the area include
the Hilton at Short Hills (800-445-8667, +908-379-0100), the Holiday
Inn of Springfield (+201-376-9400).  The latter is cheaper, but both
would require you to have a car.

With the exception of the conference dinner, meals are at the
participant's own expense.  There is a cafeteria at Bell Labs where
the participants will be able to purchase breakfast and lunch.


LOCATION

The conference is being held at Lucent Technologies, Bell Labs in
Murray Hill, NJ.  Bell Labs is located a short distance from the
Murray Hill train station which offers direct train to New York City.
The closest airport to Bell Labs is Newark International, which is
about 20 minutes away by taxi.  Cab fair from Newark International is
about $25 and a cab will hold up to four people.  The temperature in
New Jersey in August is usually 80 - 95 degrees F during the day and
in the 70's at night.


RECEPTION, BANQUET and EXCURSION

A welcoming reception will be held in the Oak Room at Bell Labs on the
evening of Tuesday 18 August (5:30pm - 6:30pm).  The banquet will be
held at the Grand Summit Hotel in the evening of Thursday 21 August.
There will be an excursion to the Statue of Liberty and Ellis Island,
or Liberty Science Center in Liberty State Park in the afternoon of
Thursday 21 August.  These arrangements may be subject to change.



  ============================================================================
                                   Program

  The 1997 International Conference on Theorem Proving in Higher Order Logics

-------------------------------------------------------------------------------

Tuesday August 19

9:00  Welcome

9:15 - 10:15   Invited Talk -- Bob Constable (Cornell Univ.)

10:15 - 10:45  Coffee Break

10:45   Derivation and Use of Induction Schemes in Higher-Order Logic
        Konrad Slind (Univ. of Cambridge)

11:20   Possibly Infinite Sequences in Theorem Provers: A Comparative Study
        M. Devillers (Univ. of Nijmegen), D. Griffioen (CWI) and
        O. Mueller (Technische Universitat Munchen)

11:55   Verifying the accuracy of polynomial approximations in HOL
        John Harrison (Univ. of Cambridge)


12:30 - 2:00 Lunch


2:00    A Hybrid Approach to Verifying Liveness in a Symmetric Multi-Processor
        Albert J. Camilleri (Hewlett-Packard)

2:35    An Isabelle-based Theorem Prover for VDM-SL
        Sten Agerholm (IFAD) and Jacob Frost (Technical University of Denmark)


3:10 - 3:40 Coffee Break

3:40 - 5:15  Category B poster session


5:30 Reception - Oak Room

-------------------------------------------------------------------------------

Wednesday August 20

9:00 - 10:00 Invited Talk -- Doron Peled (Bell Labs)

10:00 - 10:30 Coffee Break

10:30   Embedding CSP in PVS.  An Application to Authentication Protocols
        Bruno Dutertre and Steve Schneider (Univ. of London)

11:05   A full formalisation of pi-calculus theory in the Calculus of
        Constructions
        Daniel Hirschkoff (ENPC/INRIA)

11:40   Refining Reactive Systems in HOL using Action Systems
        Thomas Langbacka (Univ. of Helsinki) and
        Joakim von Wright (Abo Akademi Univ.)

12:15 - 1:45 Lunch

1:45    Human-Style Theorem Proving Using PVS
        Myla Archer and Constance Heitmeyer (NRL)

2:20    Proof Presentation for Isabelle
        Martin Simons (Technische Universitat Berlin)

2:55 - 3:25 Coffee Break

3:25 - 5:00 Category B poster session

-------------------------------------------------------------------------------

Thursday August 21

9:00    Formal Verification of Concurrent Programs in Lp and in Coq :
        A Comparative Analysis
        Boutheina Chetali and Barbara Heyd (CRIN-CNRS and INRIA-Lorraine)

9:35    A Comparative Study of Coq and HOL
        Vincent Zammit (Univ. of Kent)

10:10 - 10:40 Coffee Break

10:40   Cut elimination for a first-order formulation of higher-order logic
        Gilles Dowek (INRIA-Rocquencourt)

11:15   On Formalization of Bicategory Theory
        Takahisa Mohri (Univ. of Tokyo)

11:50 - 1:00 Lunch

1:15 Excursion

7:00 Dinner

-------------------------------------------------------------------------------

Friday August 22

9:00 - 10:00 Invited talk Deepak Kapur (SUNY-Albany)

10:00 - 10:30 Coffee Break

10:30   Towards an Object-oriented Progification Language
        Wolfgang Naraschewski (Technische Universitat Munchen)

11:05   A Theory of Structured Model-Based Specifications in Isabelle/HOL
        Thomas Santen (GMD FIRST)

11:40   Executing Formal Specifications by Translation to Higher Order
        Logic Programming
        James Andrews (Univ. of British Columbia)

12:15 - 1:15 Lunch

1:15    Higher Order Quotients and their Implementation in Isabelle HOL
        Oscar Slotosch (Technische Universitat Munchen)

1:50    Type Classes and Overloading in Higher-Order Logic
        Markus Wenzel (Technische Universitat Munchen)

2:25 - 3:30 Coffee Break (shared with 1127)

3:30 - 5:00 Business Meeting

-------------------------------------------------------------------------------


This programme is provisional, and it is possible, though not likely, that it
will be changed.

Elsa Gunter,
[email protected]

  ============================================================================

		      TPHOLs97 REGISTRATION FORM


 Name: ___________________________________________________________
    (as you would like it to appear on your name tag)

 Affiliation:

    ______________________________________________________________

    ______________________________________________________________

 Address:

    ______________________________________________________________

    ______________________________________________________________

    ______________________________________________________________

 Email: __________________________________________________________

 Fax: +___________________________________________________________

 Phone: +_________________________________________________________


 Registration fees:
             Early (before 20 June 97)  /  Late (after 20 June 97)

  Regular:   [ ] US$250.00                 [ ] US$300.00
  Student:   [ ] US$125.00                 [ ] US$165.00

  Additional Excursion tickets: US$30.00  ___________

  Additional Banquet tickets: US$65.00    ___________


  Dietary restrictions:_________________________________________


  Total Fee:_____________

  Method of payment:

  [ ] Check made payable to: University of Pennsylvania/TPHOL
      in US dollars for the total fee.

  [ ] Credit card

      Name: ______________________________________________________
           (as appears on credit card)

      Type: ______________________________________________________
           (e.g VISA, Mastercard)

      Card Number: _______________________________________________

      Expiration Date: ___________________________________________

Accommodations:

  Please mark your choice of room:

                         Cost     First Choice   Second Choice

  Murray Hill Inn      $92/night      [ ]             [ ]
  Grand Summit Hotel  $145/night      [ ]             [ ]

  To hold the reservation:

  Name: __________________________________________________________
        (as appears on credit card)

  Type: __________________________________________________________
        (e.g VISA, Mastercard)

  Card Number: ___________________________________________________


  Expiration Date: _______________________________________________


  Arrival date: __________________________________________________


  Departure date: ________________________________________________

  I will make my own reservations:    [ ]


  Double room occupancy is possible for an extra $10/night.  If you
  would like to share a room, please indicate with whom you would share
  (both must indicate the other):


  Roommate:_________________________________________________________


  Special requests:___________________________________________________