Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 20 Jul 1994 17:27:31 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA07852; Wed, 20 Jul 1994 09:53:40 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA07847; Wed, 20 Jul 1994 09:52:52 -0600 Received: from irafs1.ira.uka.de ([129.13.10.100]) by dworshak.cs.uidaho.edu (8.6.9/1.0) with SMTP id IAA19638 for ; Wed, 20 Jul 1994 08:48:24 -0700 Received: from irafs2.ira.uka.de (actually irafs2) by irafs1 with SMTP (PP); Wed, 20 Jul 1994 16:23:14 +0200 Received: from i80s37.ira.uka.de by irafs2.ira.uka.de with SMTP (PP) id <12668-0@irafs2.ira.uka.de>; Wed, 20 Jul 1994 16:27:42 +0200 To: info-hol@cs.uidaho.edu, lambda-usergroup@dcs.ed.ac.uk, theorem-provers@mc.lcs.mit.edu, isabelle-users@cl.cam.ac.uk Subject: TPCD94 Programme and Registration From: Thomas Kropf Organization: Universitaet Karlsruhe Postal-Address: IRF, Kaiserstrasse 12, D-76128 Karlsruhe, Germany Telecom: phone +49-721-608 4220, fax +49 721 370 455 Location: Karlsruhe (Germany) Date: Wed, 20 Jul 1994 16:24:40 +0200 Message-Id: <"irafs2.ira.670:20.06.94.14.27.55"@ira.uka.de> ************************************************ * Second International Conference on * * THEOREM PROVERS IN CIRCUIT DESIGN * * Theory, Practice and Experience * * Bad Herrenalb (Black Forest), Germany * * 26. - 28. September 1994 * ************************************************ In cooperation with IFIP WG 10.2 Detailed information about the conference can be found at the WWW page http://goethe.ira.uka.de/tpcd94/ Introduction ------------- This conference is a sequel to the one held at Nijmegen in June 1992 and provides a forum for discussing the role of theorem provers in the design of digital systems. The objective is to cover all relevant aspects of work in the field, i.e. verification, synthesis and testing, including original research as well as case studies and other practical experiments with new or established theorem proving tools, including tautology and model checkers. The intended audience includes workers in the field of hardware verification as well as practising digital designers with little or no prior knowledge in formal methods. For those who are not experts in the field of formal methods and who want to use this conference as a opportunity to get an idea on the underlying ideas and algorithms as well as to get an overview over the state-of-the-art in this area, we have included two excellent tutorials and three invited talks. The tutorials cover relevant aspects on how to perform design verification and implementation verification. The invited talks lighten the use of formal methods in circuit design from an academic and industrial viewpoint, the latter also judging how far the practical use of these approaches has already got on in real world applications. Moreover, the conference has also practical demonstrations of relevant verification systems, giving participants the possibility to see formal methods in practical use. There is an excellent opportunity to combine TPCD94 with other conferences on related topics. The week before TPCD94, there will be the following conferences: - International Conference on Higher-Order Logic Theorem Proving and its Applications (September 19 -22, 1994) in Malta - European Design Automation Conference with EURO_VHDL (September 19-23, 1994), Grenoble, France - Third International School and Symposium Formal Techniques in Real Time and Fault Tolerant Systems (September 19-23, 1994) in L|beck, Germany Programme --------- Sunday, September 25, 1994 18:30-22:30 Registration & Reception at the Hotel ___________________________________________________________________________ Monday, September 26, 1994 8:30-9:00 Registration 9:00-9:15 Introduction and Welcome Thomas Kropf and Ramayya Kumar Invited Talk & Benchmarks Presentation -------------------------------------- 9:15-10:15 Designing Chips That Work Geoff Barrett (INMOS Ltd., UK) 10:15-10:45 Benchmark Circuits for Hardware-Verification Thomas Kropf (University of Karlsruhe, Germany) 10:45-11:05 Coffee Break Session 1: Verification of Pipeline Structures ---------------------------------------------- Chair: Warren Hunt (Computational Logic Inc., USA) 11:05-11:45 Reasoning About Pipelines with Structural Hazards Mark Aagard and Miriam Leeser (Cornell University, USA) 11:45-12:25 A Correctness Model for Pipelined Microprocessors Phillip J. Windley (Brigham Young University, USA) and Michael L. Coe (University of Idaho, USA) 12:25-14:00 Lunch Tutorial 1 ---------- 14:00-15:30 Tutorial on Design Verification ("Synchronized Transitions") Jxrgen Staunstrup and Niels Mellergaard (Tech. Univ. of Denmark, Denmark) 15:30-15:50 Coffee Break Short Paper Session 1: Industrial Applications of Verification Techniques --------------------------------------------------------------------------- Chair: Ramayya Kumar (FZI, Germany) 15:50-16:10 A Reduced Instruction Set Proof Environment Holger Busch (Siemens AG, Germany) 16:10-16:30 Quantitative Evaluation of Formal Based Synthesis in ASIC Design Massimo Bombana, G. Bezzi, P. Cavalloro, S. Conigliaro and G. Zara (ITALTEL SIT Italy) 16:30 System Demonstrations --------------------------- The HOL documentation system in Mosaic Brigham Young University, USA The MEPHISTO Verification System FZI and University of Karlsruhe, Germany 18:00 Dinner 19:30 Bowling Tournament ___________________________________________________________________________ Tuesday, September 27, 1994 Invited Talk ------------ 8:30-9:30: Inductive Reasoning about Circuit Design Tom Melham (Glasgow University., UK) Session 2: Verification of Arithmetic and Regular Structures ------------------------------------------------------------- Chair: Jxrgen Staunstrup (Tech. Univ. of Denmark, Denmark) 9:30- 10:10 Non-Restoring Integer Square Root: A Case Study in Design by Principled Optimization John O'Leary, Miriam Leeser, Jason Hickey and Mark Aargard (Cornell University, USA) 10:10-10:50 An Automatic Generalization Method for the Inductive Proof of Replicated and Parallel Architectures Laurence Pierre (Universiti de Provence, France) 10:50-11:10 Coffee Break Session 3: Propositional Logics and Finite-State Machine based Approaches --------------------------------------------------------------------------- Chair: Paul Loewenstein, SUN Inc., USA 11:10-11:50 A Compositional Circuit Model and Verification by Composition Zheng Zhu (University of British Columbia, Canada) 11:50-12:30 Exploiting Structural Similarities in a BDD-based Verification Method Koen van Eijk and G.L.J.M. Janssen (Eindhoven University of Technology, The Netherlands) 12:30-14:00 Lunch Tutorial 2 ---------- 14:00-15:30 A Tutorial on Using PVS for Hardware Verification S. Owre, J.M. Rushby, N. Shankar and M.K. Srivas (SRI International, USA) 15:30-15:50 Coffee Break Short Paper Session 2 --------------------- Chair: Holger Busch (Siemens, Germany) 15:50-16:10 Formal Verification of Characteristic Properties of Circuits with the Larch Prover Michel Allemand (Universiti de Provence, France) 16:10-16:30 Extending Formal Reasoning with Support for Hardware Diagrams Kathi Fisler (Indiana University USA) 16:30 System Demonstrations --------------------------- PVS Verification System SRI International, USA Synchronized Transitions Tech. Univ. of Denmark, Denmark 18:00 Special Conference Dinner ___________________________________________________________________________ Wednesday, September 28, 1994 Invited Talk ------------ 8:30-9:30 Compositionality, Hierarchical Verification and the Principle of Transparency Pasupati Subrahmanyam (AT&T Bell Labs, USA) Session 4: Case Studies ----------------------- Chair: Pasupati Subrahmanyam (AT&T Bell Labs, USA) 9:30-10:10 Studies of the Single-Pulser in Various Reasoning Systems Steve D. Johnson, Paul S. Miner and Shyam Pullela (Indiana University, USA) 10:10-10:50 Checking Speed-Independence. A Case Study in Verifying Safety Properties with a Theorem Prover Michael Kishinevsky and Jxrgen Staunstrup (Tech. Univ. of Denmark, Denmark) 10:50-11:10 Coffee Break Session 5: Refinement Approaches -------------------------------- Chair: Tom Melham (University of Glasgow, UK) 11:10-11:50 Automatic Correctness Proof of Implementations of Synchronous Sequential Circuits Using an Algebraic Approach Junji Kitamichi, Sumio Morioka, Tero Higashino and Kenichi Taniguchi (Osaka University, Japan) 11:50-12:30 Mechanized Verification of Refinement Niels Maretti (Technical University of Denmark, Denmark) 12:30-14:00 Lunch Sess. 6: Comb. Higher-Order Logics and First-Order Logics Proof Techniques ---------------------------------------------------------------------- Chair: Miriam Leeser (Cornell University, USA) 14:00-14:40 Effective Theorem Proving for Hardware Verification D. Cyrluk, S. Rajan, N. Shankar and M.K.Srivas (SRI International, USA) 14:40-15:30 A Methodology for Designing Guaranteed Correct Circuits Thomas Kropf, Klaus Schneider and Ramayya Kumar (Universitdt Karlsruhe, Germany) 15:30-16:00 Tea and "Auf Wiedersehen" ___________________________________________________________________________ Due to the cosiness of the atmosphere offered by the Hotel, it is recommended that all participants stay at the Hotel. The registration fee therefore includes basically everything, i.e.: - registration fee - accommodation for 3 nights (25th Sept. - 27th Sept.) - preliminary participants proceedings - final LNCS, Springer conference proceedings which would be sent in January/February `95 - all breakfasts, lunches, coffee breaks and dinners, including the gala conference dinner - reception on Sunday, 25th Sept. - Transfer from the Bad Herrenalb Tram station to the Hotel and back Registration Deadline ---------------------- The deadline for registration and hotel reservation is the 9th of September 1994. After that date, we cannot guarantee hotel rooms. The registration/accommodation form is to be sent directly ***to the hotel***. Treff Hotel Bad Herrenalb Dobler Strasse 26 76332 Bad Herrenalb Germany Tel.: +49 7083 7420 Fax: +49 7083 4071 We would be grateful, if you could also send us a short email giving the basic details. All those who register after this date will not be guaranteed rooms in Treff Hotel. email: kumar@fzi.de _________________________________________________________________________ Registration and Accommodation form ----------------------------------- ___ Single Occupancy + Registration (DM 850) ___ Double Room Sharing + Registration (DM 790) ___ Registration without Accommodation (DM 600) ___ Accompanying Person (DM 500) Name: __________________________________________ Address: ________________________________________ ________________________________________________ ________________________________________________ ________________________________________________ Country: __________________________________________ Postcode: __________________________________________ Tel.: _________________________ Fax: _________________________ email: _______________________ Name of the sharing person: _________________________ Number of Accompanying Persons: ____________________ Dietary Requirements: ___ Vegetarian ___Diabetic Enclosed a cheque/Bank Draft for DM ________ Made a Bank Transfer for DM __________ to Deutsche Bank AG Ettlingen BLZ 660 700 04 Account Number 0732180 (Copy of the Receipt of Bank Transfer is enclosed) Please charge my credit card: __ American Express/ __ Diners/ __ Visa/ __ Mastercard Card Number __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ Expiry Date: __ __ / __ __ / __ __ Signature of the Cardholder _________________________ If you need any further informations, do not hesitate to contact me or (concerning registration details) the Conference Chair Ramayya Kumar (kumar@fzi.de). -- Thomas Kropf Institut fuer Rechnerentwurf und Fehlertoleranz Universitaet Karlsruhe, Kaiserstr. 12, D-76128 Karlsruhe, Germany email: kropf@ira.uka.de FAX: +49 721 370 455 Tel.: +49 721 608 4220