From mboxrd@z Thu Jan 1 00:00:00 1970 X-Sympa-To: caml-list@inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q1RN1PBR010944 for ; Tue, 28 Feb 2012 00:01:25 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: As8AAJMKTE/dx9kLkWdsb2JhbABDs2oiAQEBAQkLCwcUBSKBdSJLgU8ch3wMmCWgOIl0BYMGEQ4HBgIEAgMDAQEBBAUBAQILCQMHGwuFAA0DDAMOFg4DBAkUglBjBIgcjSGLE4dvgUAJ X-IronPort-AV: E=Sophos;i="4.73,493,1325458800"; d="scan'208";a="133249385" Received: from ajax.nicta.com.au ([221.199.217.11]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/AES256-SHA; 28 Feb 2012 00:01:18 +0100 Received: from atp-mbx1.it.nicta.com.au ([221.199.216.123] helo=atp-mbx1.in.nicta.com.au) by ajax.nicta.com.au with esmtp (Exim 4.72) (envelope-from ) id 1S29ZD-0004t6-2J; Tue, 28 Feb 2012 10:01:15 +1100 Received: from peterhoefner.dynhost.nicta.com.au (221.199.216.124) by atp-mbx1.in.nicta.com.au (221.199.216.123) with Microsoft SMTP Server (TLS) id 8.3.192.1; Tue, 28 Feb 2012 09:55:16 +1100 From: =?iso-8859-1?Q?Peter_H=F6fner?= Content-Type: text/plain; charset="iso-8859-1" Date: Tue, 28 Feb 2012 09:55:15 +1100 To: =?iso-8859-1?Q?Peter_H=F6fner?= Message-ID: MIME-Version: 1.0 (Apple Message framework v1257) X-Mailer: Apple Mail (2.1257) X-TM-AS-Product-Ver: SMEX-8.0.0.4125-6.500.1024-18740.002 X-TM-AS-Result: No--14.976200-0.000000-31 X-TM-AS-User-Approved-Sender: Yes X-TM-AS-User-Blocked-Sender: No X-SA-Exim-Connect-IP: 221.199.216.123 X-SA-Exim-Mail-From: Peter.Hoefner@nicta.com.au X-SA-Exim-Scanned: No (on ajax.nicta.com.au); SAEximRunCond expanded to false Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id q1RN1PBR010944 X-Validation-by: peter.hoefner@nicta.com.au Subject: [Caml-list] CfP: IJCAR Workshop on Automated Theory Exploration [Apologies if you receive multiple copies of this announcement] %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% CALL FOR PAPERS: ATX-2012 IJCAR Workshop on Automated Theory Exploration (June 30-July 1) http://dream.inf.ed.ac.uk/events/atx2012 GENERAL INFORMATION This Workshop on Automated Theory Exploration will be held in June/July in Manchester, UK. It is associated with the 6th International Conference on Automated Reasoning (IJCAR) and follows on from two series of workshops: Automated Theory Engineering and Automatheo. SCOPE Theory exploration means the development of mathematical axioms, definitions, conjectures, theorems, examples and inference procedures as needed to cover the essential concepts and analysis tasks of mathematical and other application domains. The automation and mechanisation of these capabilities are much sought after in areas such as software verification, the analysis of computer systems, formalised mathematics and indeed mathematical research. The aim of the workshop is to bring together researchers with interests in any aspects of this area, including domain-specific formalisations, tool and theory development, and general-purpose frameworks for the structuring of theories and their maintenance. TOPICS Theory exploration is relevant to the design of systems, programs, APIs, protocols, algorithms, design patterns, specification languages, programming languages and beyond. It involves technology such as ITP systems, ATP systems, SAT/SMT solvers, model checkers and decision procedures. Specific topics of the workshop include, but are not limited to: o mechanised reasoning for modelling and analysis o automation applied to formal specification and verification o domain specific models, languages and solvers o theorem proving technology for theory exploration o integration of theories and tools o the formalisation and automation of mathematics o case studies/experiences o automated identification of key concepts and results o supporting collaborative theory exploration INVITED SPEAKERS o Robert L. Constable, Cornell University. o TBA SUBMISSIONS We invite submissions in 3 forms: o Research papers, up to 10 pages; o System/tool descriptions, up to 5 pages; o Extended abstracts, up to 3 pages. Research and tool papers must be unpublished and not submitted for publication elsewhere. Extended abstracts are intended to discuss ideas and work in progress. All papers will be reviewed by the programme committee. Submissions must be in PDF using the LaTeX EasyChair-format http://www.easychair.org/easychair.zip . One author of each accepted submission is expected to present the paper at the workshop. Associated systems demos are encouraged, where appropriate. Accepted research and tool papers will be published as CEUR Workshop Proceedings. If quality and quantity of the submissions warrants this, we plan to publish a special issue of a recognized journal on the topic of the workshop. IMPORTANT DATES: Submission: 3 April 2012 Notification: 8 May, 2012 Final version: 5 June, 2012 Workshop: 30 June & 1 July, 2012 PROGRAM COMMITTEE o Jacques Fleuriot (University of Edinburgh, UK) o Timothy Griffin (University of Cambridge, UK) o Peter Höfner (NICTA, Australia) o Joe Hurd (Galois, USA) o Temur Kutsia (RISC, Austria) o Roy McCasland (University of Edinburgh, UK) o Annabelle McIver (Macquarie University, Australia) o Stephan Merz (INRIA, France) o Petros Papapanagiotou (University of Edinburgh, UK) o Alan Smaill (University of Edinburgh, UK) o David Stanovsky (Charles University, Czech Republic) o Georg Struth (University of Sheffield, UK) o Josef Urban (Radboud University, Netherlands) WORKSHOP ORGANISERS o Alan Smaill o Annabelle McIver o Peter Höfner o Jacques Fleuriot The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.