From kropf@ira.uka.de Thu Feb 10 21:09:21 EST 1994 Article: 5639 of news.announce.conferences Xref: glinda.oz.cs.cmu.edu news.announce.conferences:5639 Newsgroups: news.announce.conferences Path: honeydew.srv.cs.cmu.edu!bb3.andrew.cmu.edu!news.sei.cmu.edu!cis.ohio-state.edu!magnus.acs.ohio-state.edu!math.ohio-state.edu!cs.utexas.edu!uunet!sparky!rick From: kropf@ira.uka.de (Thomas Kropf, Univ. Karlsruhe) Subject: CFP: Theorem Provers in Circuit Design (TPCD94) Message-ID: <1994Feb9.231102.11936@sparky.sterling.com> Sender: rick@sparky.sterling.com (Richard Ohnemus) Organization: Sterling Software Date: Wed, 9 Feb 1994 23:11:02 GMT Approved: rick@sparky.sterling.com Expires: Sat, 26 Mar 1994 08:00:00 GMT Lines: 189 X-Md4-Signature: e37dd349807a96d0c0a8bf7d9411800a +-------------------------------------------------------+ | | | CALL FOR PAPERS | | | | Second International Conference on | | | | THEOREM PROVERS IN CIRCUIT DESIGN: | | Theory, Practice and Experience | | | | Bad Herrenalb (Blackforest), Germany | | 26. - 29. September 1994 | | | | In cooperation with IFIP WG 10.2 | | | +-------------------------------------------------------+ FOCUS AND OBJECTIVES The use of formal methods in the design of digital systems is steadily gaining popularity. The practicability of such techniques, however, depends on the support of appropriate mechanized verification tools. 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 experi- ments with new or established theorem proving tools, including tau- tology and model checkers. The primary focus will be on the ways in which formal methods can be incorporated into hardware design tools and hardware design me- thodologies, rather than the theory underlying the theorem provers. Topics of interest include the philosophy behind the incorporation of formal techniques in design tools, hardware specification languages, the design and development and evaluation of formally-based tools, and the integration of formally based design and verification with exi- sting tools and methodologies. The intended audience includes workers in the field of hardware ve- rification as well as practising digital designers with little or no prior knowledge in formal methods. SUBMITTING A PAPER Five copies of a complete paper (in English) should be sent to the Con- ference Chair at the address given below to arrive no later than 25 March 1994. Electronic mail submissions in a postscript format are also acceptable. Papers must not exceed 6000 words in length, with full-page figures counted as 300 words. Each paper should include a 300 word abstract. All papers will be refereed and the final choice will be made by the programme committee on the grounds of relevance, significance, originality, correctness, clarity and the use of given benchmark circuits (see below). The conference proceedings will be published by a major publisher. BENCHMARK CIRCUITS A set of benchmarks has been provided by anonymous ftp at goethe.ira.uka.de (129.13.18.22). The circuits as well as detailed instructions on how to use them can be found in the directory /pub/tpcd94/benchmarks. All authors submitting a regular paper or a proposal for a tutorial are strongly encouraged to make use of these circuits. IMPORTANT DATES The important dates are as follows: 25 March 1994: Final deadline for the submission of papers. 20 June 1994: Date for notification of acceptance. 8 July 1994: Final camera-ready copy due. 26-29 September 1994: Conference at Bad Herrenalb. PROPOSALS FOR TUTORIALS Proposals are solicited for tutorial presentations on relevant verifica- tion tools and provers. The intention is that a tutorial will provide an overview of the basic ideas behind the tool using a completely worked out example, rather than a detailed instruction on how to use it, hence the use of benchmark circuits is also suggested. The tutorials should include an assessment of strengths and weaknesses of the tools and should concentrate on general issues such as security, robustness, the degree of interaction required, the user interface, and the mathemati- cal skill required of the user. Proposals for tutorials should not exceed 6000 words in length and should give a clear indication of the topic and structure of the presen- tation. The proposals for tutorials will also undergo a review process and it is proposed to have no more than 6 tutorials during the confe- rence. Also welcome are proposals for demonstrations of working sy- stems. Proposals for both tutorials and demonstrations should be sent to the Tutorials Chair to arrive no later than 25 March 1994. The tuto- rial papers will also be included in the proceedings. PROGRAMME The conference programme will start with a day of tutorials and is fol- lowed by three days of presentations by contributing authors. The late afternoon sessions will be reserved for demonstrations. The program- me will also include invited lectures by prominent researchers in the field of machine-assisted verification. The names of the invited spea- kers will be announced in due course. ORGANIZATION The conference is organized jointly by the Forschungszentrum Infor- matik (FZI), Karlsruhe and the Institute of Computer Design and Fault Tolerance at the University of Karlsruhe, Germany. The conference organizers are: Conference Chair: Ramayya Kumar, FZI Karlsruhe Programme Chair: Mike Fourman, Edinburgh University Tutorials Chair and Benchmarks: Thomas Kropf, University of Karlsruhe Local Arrangements: Hilke Kloss, FZI Karlsruhe PROGRAMME COMMITTEE Dominique Borrione (IMAG, France) Holger Busch (Siemens AG, Germany) Luc Claesen (IMEC, Belgium) David Dill (Stanford University, USA) Hans Eveking (Univ. of Frankfurt, Germany) Simon Finn (AHL, UK) Mike Gordon (University of Cambridge, UK) Keith Hanna (University of Kent, UK) Warren A. Hunt Jr. (CL Inc. USA) Paul Loewenstein (SUN, USA) Miriam Leeser (Cornell Univ., USA) Tom Melham (University of Cambridge, UK) Tobias Nipkow (TU M|nchen, Germany) David Shepherd (Inmos, UK) Jxrgen Staunstrup (Lyngby Univ., Denmark) Victoria Stavridou (Univ. of London, UK) Pasupati Subrahmanyam (ATT Bell Labs, USA) ADDRESSES FOR CORRESPONDENCE The papers and all general correspondence should, in the first in- stance, be sent to the Conference Chair: Ramayya Kumar TPCD Conference Chair Forschungszentrum Informatik Department - ACID Haid-und-Neu Strasse 10-14 76131 Karlsruhe, Germany Tel: (+49) 721 9654-419 Fax: (+49) 721 9654-459 Email: kumar@fzi.de Proposals for tutorials, demonstrations and everything related to the benchmark circuits should be sent to the Tutorials Chair: Thomas Kropf TPCD Tutorials Chair Universitaet Karlsruhe Inst. f. Rechnerentwurf u. Fehlertoleranz P.O. Box 6980 76128 Karlsruhe, Germany Tel: (+49) 721 608-4220 Fax: (+49) 721 370 455 Email: kropf@ira.uka.de All correspondence should include a return postal address and, if possible, Fax and email address. -- Thomas Kropf Institut fuer Rechnerentwurf und Fehlertoleranz Universitaet Karlsruhe, Kaiserstr. 12, D-76128 Karlsruhe, Germany email: kropf@informatik@uni-karlsruhe.de FAX: +49 721 370 455 Tel.: +49 721 608 4220